Finite graphs are well-quasi-ordered by the minor relation (Graph Minor Theorem)

Open

TenChallenges.challenge_06_r1

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

graph-minorsten-challengeswell-quasi-ordering

The rung $r=1$ of Challenge 6: the Graph Minor Theorem. For every sequence $G_0,G_1,\dots$ of finite graphs there are indices $i<j$ such that $G_i$ is a minor of $G_j$ :

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

Preamble

import Definitions.Def_TenChallenges_Challenge_06

Formal statement

namespace TenChallenges
theorem challenge_06_r1 : statement_06 1 := 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, Theorem 1.1 (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