Finite planar graphs are well-quasi-ordered by the minor relation

Open

TenChallenges.challenge_06_r0

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-minorsten-challengeswell-quasi-ordering

The rung $r=0$ of Challenge 6: finite planar graphs are well-quasi-ordered under minors. For every sequence $G_0,G_1,\dots$ of finite graphs without $K_5$ or $K_{3,3}$ minor there are indices $i<j$ such that $G_i$ is a minor of $G_j$ :

\forall (G_n)_{n\in\mathbb N}\ \text{planar}:\quad \exists i<j:\ G_i\preceq G_j .

Preamble

import Definitions.Def_TenChallenges_Challenge_06

Formal statement

namespace TenChallenges
theorem challenge_06_r0 : statement_06 0 := by sorry
end TenChallenges

Source

N. Robertson, P. D. Seymour, Graph minors. XX. Wagner's conjecture, JCTB 92 (2004), 325–357, https://doi.org/10.1016/j.jctb.2004.08.001 (the planar case is a special case of the Graph Minor Theorem)

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph