Motivation

The Graph Minor Theorem of Robertson and Seymour states that finite graphs are well-quasi-ordered by the minor relation: in every infinite sequence of finite graphs, some graph is a minor of a later one. It is one of the deepest results of combinatorics, and it implies that every minor-closed class of graphs is characterised by finitely many excluded minors. Nash-Williams introduced the stronger notion of better-quasi-ordering (BQO) in the 1960s, precisely because well-quasi-ordering is not preserved under the natural infinitary constructions (Rado's example): BQO is preserved under taking subsets, sequences and transfinite iterations of these. Whether finite graphs are better-quasi-ordered under minors is a folklore conjecture that has resisted every attempt; the only known route, the Graph Minor Theorem, gives well-quasi-ordering and nothing more (Georgakopoulos 2025).

Timeline.

• 1954 — Rado exhibits a well-quasi-order whose power set is not well-quasi-ordered (Rado 1954).
• 1965/1968 — Nash-Williams introduces better-quasi-orders and proves that they are closed under the operations that break well-quasi-orders; infinite trees are BQO under topological minors (Nash-Williams 1965).
• 1983–2004 — Robertson and Seymour prove the Graph Minor Theorem (Robertson–Seymour 2004).
• 1988 — Thomas shows that infinite graphs are not well-quasi-ordered under minors and conjectures that countable graphs are (Thomas 1988).
• 2025 — Georgakopoulos proves that the BQO conjecture for finite graphs is equivalent to Thomas's conjecture restricted to rayless countable graphs (Georgakopoulos 2025).

Setting

A quasi-order is a reflexive, transitive relation $\le$ on a set $Q$. It is a well-quasi-order (WQO) if for every sequence $q_0,q_1,\dots$ in $Q$ there are $i<j$ with $q_i\le q_j$.

For a set $Q$ and an ordinal $\alpha$ define the cumulative hierarchy $V^*_\alpha(Q)$ by $V^*_0(Q)=Q$, $V^*_{\beta+1}(Q)=\mathcal P^*(V^*_\beta(Q))$ (the nonempty subsets), and $V^*_\lambda(Q)=\dot\bigcup_{\beta<\lambda}V^*_\beta(Q)$ (disjoint union) for limit $\lambda$. Extend $\le$ to a relation $\le^*$ on the hierarchy by a two-player game from a position $(X,Y)$: if both $X$ and $Y$ lie in $Q$, Player II wins if $X\le Y$; otherwise Player I names $X'$, which is $X$ itself if $X\in Q$ and an element of $X$ otherwise, then Player II names $Y'$ in the same way from $Y$, and play continues from $(X',Y')$; an element of a limit level is identified with its underlying element of a lower level. Then $X\le^* Y$ means that Player II has a winning strategy from $(X,Y)$. The quasi-order $(Q,\le)$ is $\alpha$-well-quasi-ordered if $(V^*_\alpha(Q),\le^*)$ is well-quasi-ordered. Thus $0$-WQO is WQO, and $(Q,\le)$ is BQO exactly when it is $\omega_1$-WQO, equivalently $\alpha$-WQO for every ordinal $\alpha$.

Finite graphs are ordered by $G\preceq H$ if $G$ is a minor of $H$: $H$ contains pairwise disjoint connected branch sets $B_v$, one for each vertex $v$ of $G$, with an edge of $H$ between $B_u$ and $B_v$ for every edge $uv$ of $G$. A finite graph is planar if it has neither $K_5$ nor $K_{3,3}$ as a minor (Wagner's criterion). The challenge interleaves planar graphs and all graphs: for an ordinal $r$, write $r=2\cdot\alpha+k$ with $k\in\{0,1\}$ and let

$$\mathrm{WQO}(r):\quad\begin{cases}\text{finite planar graphs are } \alpha\text{-WQO under minors} & k=0,\\ \text{finite graphs are } \alpha\text{-WQO under minors} & k=1.\end{cases}$$

Formalization targets

Goal

$$\forall r\in\mathrm{Ord}:\quad \mathrm{WQO}(r),$$

i.e. finite graphs (and finite planar graphs) are $\alpha$-well-quasi-ordered under minors for every ordinal $\alpha$: the BQO conjecture for graph minors.

Rungs

$\mathrm{WQO}(0)$ (planar graphs are WQO) and $\mathrm{WQO}(1)$ (the Graph Minor Theorem) are proved, by the same theorem. $\mathrm{WQO}(2)$, that nonempty sets of planar graphs are well-quasi-ordered under the lifted relation, is the first rung beyond the Graph Minor Theorem; the literature cited here records no proof of it.

Significance

Better-quasi-ordering is the property that makes well-quasi-order theory robust: the BQO conjecture would imply that countable rayless graphs are BQO and would give the strongest form of the structure theory of graph minors. It is equivalent to Thomas's conjecture on rayless graphs and would settle Seymour's self-minor conjecture for them. Even the rung $\mathrm{WQO}(1)$ is the Graph Minor Theorem.

No part of this landscape is formalized: Mathlib has well-quasi-orders in the form of WellQuasiOrderedLE-style notions but neither the minor relation, nor Nash-Williams's hierarchy, nor any piece of the Graph Minor Theorem. Formalizing the definitions alone already contributes a reusable theory of $\alpha$-WQO and better-quasi-orders, and the planar rung $\mathrm{WQO}(0)$ is a long-term formalization target of independent interest.

Difficulty

Well-quasi-ordering of planar graphs rests on the Grid Theorem and tree-decompositions; the full Graph Minor Theorem on the structure theorem for graphs excluding a minor, hundreds of pages of proof. Beyond well-quasi-ordering, the Graph Minor Theorem gives no information: BQO cannot be obtained from WQO by any general principle (Rado), and the only known BQO results for graphs concern trees and bounded tree-width-like classes, proved by Nash-Williams's minimal bad sequence method in its transfinite form. The naive idea, that WQO of a class implies WQO of its power set, is exactly what Rado's example refutes.

Formalization scope

Quasi-orders are arbitrary binary relations le : Q → Q → Prop; IsWQO le says every sequence $f\colon\mathbb N\to Q$ has $i<j$ with le (f i) (f j). VStar Q o is defined by Mathlib's ordinal recursion Ordinal.limitRecOn: level $0$ is $Q$, a successor level is the type of nonempty subsets ({S : Set _ // S.Nonempty}) of the previous level, and a limit level is the sigma type over the smaller ordinals (represented by o.ToType) of the lower levels. leStar le a X b Y is the game relation between $X$ at level $a$ and $Y$ at level $b$, defined by recursion on $a$ and $b$ with casts along the three level equations; limit-level elements are unwrapped to their underlying lower-level element. IsAlphaWQO le a is IsWQO of leStar le a · a · on VStar Q a. Finite graphs are FiniteGraph := Σ n, SimpleGraph (Fin n), with MinorLE G H := Nonempty (Minor G.2 H.2) (a Minor structure records branch sets, their disjointness and connectedness, and the edge witnesses); PlanarGraph is the subtype of FiniteGraph satisfying IsWagnerPlanar, no K5 and no K33 minor. Ordinals are Ordinal.{0}, and statement_06 r branches on Mathlib's ordinal remainder r % 2 and uses the ordinal quotient r / 2 as the level. The goal is ∀ r, statement_06 r.

No trivialising reading: $\alpha$-WQO at level $0$ is well-quasi-ordering, the relations are the minor relation on the nose, and the universe of graphs is all finite simple graphs on Fin n. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: basic lemmas about VStar and leStar (monotonicity, the characterisation of $1$-WQO as the Hoare lift), reflexivity and transitivity of MinorLE, the equivalence of $\omega_1$-WQO with Nash-Williams's definition of BQO, and decompositions of $\mathrm{WQO}(0)$.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 6).
• R. Rado, Partial well-ordering of sets of vectors, Mathematika 1 (1954), 89–95. https://doi.org/10.1112/S0025579300000565
• C. St. J. A. Nash-Williams, On well-quasi-ordering infinite trees, Proc. Cambridge Philos. Soc. 61 (1965), 697–720. https://doi.org/10.1017/S0305004100039062
• N. Robertson, P. D. Seymour, Graph minors. XX. Wagner's conjecture, J. Combin. Theory Ser. B 92 (2004), 325–357. https://doi.org/10.1016/j.jctb.2004.08.001
• R. Thomas, A counter-example to "Wagner's conjecture" for infinite graphs, Math. Proc. Cambridge Philos. Soc. 103 (1988), 55–57. https://doi.org/10.1017/S0305004100064616
• A. Georgakopoulos, On better-quasi-ordering under graph minors, 2025. https://arxiv.org/abs/2510.19285
• R. Diestel, Graph Theory, 5th ed., Springer, 2017, Chapter 12. https://doi.org/10.1007/978-3-662-53622-3