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

Open

TenChallenges.challenge_06_r2

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

graph-minorsten-challengeswell-quasi-ordering

The rung $r=2$ of Challenge 6: finite planar graphs are $1$ -well-quasi-ordered under minors. For every sequence $X_0,X_1,\dots$ of nonempty sets of finite planar graphs there are indices $i<j$ such that every graph in $X_i$ is a minor of some graph in $X_j$ :

\forall (X_n)_{n\in\mathbb N}:\quad \exists i<j\ \ \forall G\in X_i\ \ \exists H\in X_j:\ G\preceq H .

Here $2=2\cdot 1+0$ , so the level is $\alpha=1$ and the class is the planar graphs.

Preamble

import Definitions.Def_TenChallenges_Challenge_06

Formal statement

namespace TenChallenges
theorem challenge_06_r2 : statement_06 2 := by sorry
end TenChallenges

Source

Open; context in A. Georgakopoulos, On better-quasi-ordering under graph minors, https://arxiv.org/abs/2510.19285

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

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

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