Ten Challenges

Motivation

Hadwiger's conjecture (1943) asserts that for every integer $t\ge 0$, every graph with no $K_{t+1}$ minor is $t$-colourable. It is a far-reaching strengthening of the four-colour theorem, and it is widely described as one of the central open problems of graph theory (Bollobás, Catlin and Erdős called it "one of the deepest unsolved problems in graph theory"). The interest is structural: the four-colour theorem concerns planar graphs, and Hadwiger's conjecture proposes that the only obstruction to $t$-colourability that matters is the presence of a complete graph $K_{t+1}$ as a minor.

Timeline.

• 1937 — Wagner shows that the case $t=4$ is equivalent to the four-colour theorem, via a clique-sum decomposition of graphs with no $K_5$ minor.
• 1943 — Hadwiger poses the conjecture and proves it for $t\le 3$ (graphs with no $K_4$ minor have a vertex of degree at most two).
• 1964 — Wagner proves that graphs with no $K_{t+1}$ minor are $2^t$-colourable.
• 1967 — Mader proves that excluding any fixed minor forces a linear number of edges, and determines the exact extremal function for $K_t$ minors when $t\le 7$.
• 1976 — Appel and Haken prove the four-colour theorem, hence the case $t=4$.
• 1982 — Duchet and Meyniel prove that every $n$-vertex graph has a $K_t$ minor with $t\ge n/(2\alpha(G)-1)$.
• 1984 — Kostochka and Thomason independently show that graphs with no $K_t$ minor have average degree $O(t\sqrt{\log t})$, hence are $O(t\sqrt{\log t})$-colourable.
• 1993 — Robertson, Seymour and Thomas prove the case $t=5$ (using the four-colour theorem).
• 2023–2024 — Norin, Postle and Song, then Delcourt and Postle, improve the general bound to $O(t\log\log t)$ colours.
• (Date not recorded in the survey) Albar and Gonçalves prove that graphs with no $K_7$ minor are $8$-colourable and graphs with no $K_8$ minor are $10$-colourable.

The case $t=6$ (graphs with no $K_7$ minor are $6$-colourable) is the first open case.

Setting

All graphs are finite and simple. A minor of a graph $G$ is any graph obtained from a subgraph of $G$ by contracting edges. Equivalently, a graph $H$ on vertex set $W$ is a minor of $G$ if there are branch sets $B_w\subseteq V(G)$, $w\in W$, which are pairwise disjoint, each inducing a connected (nonempty) subgraph of $G$, and such that for every edge $w_1w_2$ of $H$ some vertex of $B_{w_1}$ is adjacent to some vertex of $B_{w_2}$. $G$ has a $K_t$ minor if the complete graph $K_t$ is a minor of $G$, i.e. $G$ contains $t$ pairwise disjoint connected vertex sets, every two joined by an edge.

A graph is $t$-colourable if its vertices can be coloured with $t$ colours so that adjacent vertices receive different colours; $\chi(G)$ is the least such $t$. Write $\mathrm{HC}(t)$ for the statement "every graph with no $K_{t+1}$ minor is $t$-colourable". A graph is $k$-degenerate if every nonempty set of vertices contains a vertex with at most $k$ neighbours inside the set. The stability number $\alpha(G)$ is the largest size of a set of pairwise non-adjacent vertices.

Formalization targets

Goal

$$\forall t\ge 0:\qquad K_{t+1}\not\preceq G\ \Longrightarrow\ \chi(G)\le t\qquad\text{for every finite graph } G.$$

Proved special cases

$$\mathrm{HC}(t)\ \text{for } t\le 3,\qquad \mathrm{HC}(4),\qquad \mathrm{HC}(5).$$

Weaker colouring bounds

• no $K_{t+1}$ minor $\Rightarrow$ $\chi(G)\le 2^t$ (Wagner);
• no $K_t$ minor $\Rightarrow$ $\chi(G)=O(t\sqrt{\log t})$ (Kostochka, Thomason) and $\chi(G)=O(t\log\log t)$ (Delcourt–Postle);
• no $K_7$ minor $\Rightarrow$ $\chi\le 8$; no $K_8$ minor $\Rightarrow$ $\chi\le 10$ (Albar–Gonçalves).

Supporting extremal and structural results

• non-null graphs with no $K_4$ minor have a vertex of degree $\le 2$;
• $k$-degenerate graphs are $(k+1)$-colourable;
• for every $H$ there is $c$ with $|E(G)|\le c|V(G)|$ whenever $H\not\preceq G$ (Mader);
• the exact edge bounds $n-1$, $2n-3$, $3n-6$ for no $K_3$, $K_4$, $K_5$ minor, and $(t-2)n-\binom{t-1}{2}$ for no $K_t$ minor, $t\le 7$ (Mader);
• every $n$-vertex graph has a $K_t$ minor with $t\ge n/(2\alpha(G)-1)$ (Duchet–Meyniel);
• a graph with no $K_{t+1}$ minor has a $t$-colourable induced subgraph on at least half of its vertices.

Significance

A proof of the conjecture would give a structural explanation of the four-colour theorem that does not depend on planarity, and would settle the chromatic number of every minor-closed class defined by excluding a single complete graph. Partial results already drive the theory of graph minors: bounds on the average degree of $K_t$-minor-free graphs are the standard input to colouring, and linear Hadwiger-type bounds are used in structural and algorithmic graph theory.

On the formal side, only the smallest cases have Lean proofs: the platform already contains proofs of the cases $t\le 2$ under a different encoding of minors (namespace Hadwiger), which may be reused after bridging the definitions. The cases $t\le 3$, Wagner's $2^t$ bound, the degeneracy lemma, the small extremal bounds and the Duchet–Meyniel theorem have elementary proofs and are realistic targets. The cases $t=4,5$ depend on the four-colour theorem, whose formal proof exists in Coq but not in Lean; formalizing them here requires either porting that proof or proving the reduction to it. The general conjecture is open.

Difficulty

The natural approach — contracting the colour classes of an optimal colouring — does not produce a minor, because colour classes are independent sets and contraction is only allowed along edges. Degeneracy arguments only give bounds of order $t\sqrt{\log t}$, since dense random graphs with no large clique minor have average degree of that order; closing the gap to $t$ requires using large chromatic number itself, not just density. Already for $t=4$ the statement is equivalent to the four-colour theorem, so no short proof is expected for any $t\ge 4$.

Formalization scope

Graphs are SimpleGraph V on a finite vertex type V : Type. Minors are encoded by branch sets (IsMinor), complete minors by HasCompleteMinor G t (the complete graph on Fin t is a minor of G), colourability by Mathlib's SimpleGraph.Colorable, and edge counts by the cardinality of the edge set. $\mathrm{HC}(t)$ is the definition HC t. Logarithms are natural logarithms; asymptotic bounds are stated with an explicit existential constant and a ceiling. The case $t=0$ is included; HasCompleteMinor G 0 holds for every graph, so no statement becomes vacuous through a degenerate minor definition.

Useful reusable infrastructure: minor models and their composition, contraction of connected sets, greedy colouring of degenerate graphs, and edge-counting for minor-free graphs. Contributions of intermediate lemmas along the milestones are welcome.

Selected references

• P. Seymour, Hadwiger's conjecture, in: Open Problems in Mathematics, Springer, 2016 (survey; source of the milestone numbering).
• Wikipedia, Hadwiger conjecture (graph theory). https://en.wikipedia.org/wiki/Hadwiger_conjecture_(graph_theory)
• H. Hadwiger, Über eine Klassifikation der Streckenkomplexe, Vierteljschr. Naturforsch. Ges. Zürich 88 (1943).
• K. Wagner, Über eine Eigenschaft der ebenen Komplexe, Math. Ann. 114 (1937).
• N. Robertson, P. Seymour, R. Thomas, Hadwiger's conjecture for $K_6$-free graphs, Combinatorica 13 (1993).
• A. Kostochka, Lower bound of the Hadwiger number of graphs by their average degree, Combinatorica 4 (1984).
• A. Thomason, An extremal function for contractions of graphs, Math. Proc. Cambridge Philos. Soc. 95 (1984).
• M. Delcourt, L. Postle, Reducing linear Hadwiger's conjecture to coloring small graphs (2024).

Motivation

How many copies of a fixed graph $H$ must a graph $G$ of given edge density contain? For bipartite $H$, Sidorenko's conjecture gives the cleanest possible answer: the random graph of the same density contains the fewest, so the homomorphism density of $H$ in $G$ is at least the edge density of $G$ raised to the number of edges of $H$. The statement was conjectured independently by Erdős and Simonovits and by Sidorenko; it is equivalent to a family of integral inequalities for graphons and is a benchmark problem of extremal graph theory, with consequences for quasirandomness, graph norms and the counting of subgraphs in dense graphs (Conlon–Fox–Sudakov 2010, Szegedy 2015).

Timeline.

• 1984/1991 — Erdős and Simonovits, and Sidorenko, pose the conjecture; Sidorenko proves it for trees, even cycles, complete bipartite graphs, and bipartite graphs with at most four vertices on one side (Sidorenko 1991, Sidorenko 1993).

• 2010 — Hatami proves it for hypercubes via graph norms (Hatami 2010); Conlon, Fox and Sudakov prove it for every bipartite graph with a vertex adjacent to all vertices on the other side (Conlon–Fox–Sudakov 2010).

• 2011 — Li and Szegedy extend the vertex-complete case to graphs obtained by gluing (Li–Szegedy 2011).

• 2015 — Szegedy's entropy method and the tree-arrangeable graphs of Kim, Lee and Lee enlarge the known classes (Szegedy 2015, Kim–Lee–Lee 2016).

• 2018 — Conlon, Kim, Lee and Lee prove it for strongly tree-decomposable graphs and for the first bipartite graphs without the vertex-complete property (Conlon–Kim–Lee–Lee 2018); Conlon and Lee prove it for all graphs obtained by gluing enough copies of a bipartite graph along one side (Conlon–Lee 2021).

• 2026 — OpenAI releases a manuscript A counterexample to Sidorenko's conjecture (dated 23 September, published 6 October 2026) with a Lean proof: for $H$ the incidence graph of $22$ triples on $13$ points ($35$ vertices, $66$ edges, sides of size $13$ and $22$) there is a finite host $G$ with $t(H,G)<t(K_2,G)^{66}$ (openai/math). The claim has not yet been reviewed by the community; its Lean proof has been checked mechanically by third parties, including the ProofBench harness.

Before this, the smallest bipartite graph for which the conjecture was open was $K_{5,5}$ minus a $10$-cycle, the Möbius ladder on ten vertices, with five vertices on each side.

Setting

All graphs are finite and simple. A homomorphism from $H$ to $G$ is a map $f\colon V(H)\to V(G)$ with $f(u)f(v)\in E(G)$ for every edge $uv\in E(H)$; $\hom(H,G)$ is the number of homomorphisms and the homomorphism density is

$$t(H,G) := \frac{\hom(H,G)}{|V(G)|^{|V(H)|}}.$$

For the single edge $K_2$, $t(K_2,G)=2|E(G)|/|V(G)|^2$ is the edge density. Sidorenko's inequality for $H$ in $G$ is

$$t(H,G)\ \ge\ t(K_2,G)^{|E(H)|}.$$

A graph $H$ is bipartite with sides bounded by $r$ if $V(H)=X\cup Y$ for disjoint sets $X,Y$ with every edge between $X$ and $Y$, $|X|\le r$ and $|Y|\le r$. For $r\in\mathbb N$ let $\mathrm{Sid}(r)$ be the statement

$$\text{for every } H \text{ bipartite with sides bounded by } r \text{ and every nonempty } G:\quad t(H,G)\ \ge\ t(K_2,G)^{|E(H)|}.$$

Formalization targets

Goal

$$\text{for every finite bipartite } H \text{ and every nonempty finite } G:\quad t(H,G)\ \ge\ t(K_2,G)^{|E(H)|},$$

Sidorenko's conjecture itself. It is equivalent to $\mathrm{Sid}(r)$ for all $r$, since every finite bipartite graph has sides bounded by some $r$. If OpenAI's counterexample stands, the goal is false and the mission closes by a disproof: a Lean proof of the negation, which is what the claimed counterexample provides once transported to the definitions here.

Rungs

$\mathrm{Sid}(r)$ for $r\le 4$ follows from Sidorenko's theorem on bipartite graphs with at most four vertices on one side. $\mathrm{Sid}(22)$ is refuted by the counterexample, whose $H$ has sides of size $13$ and $22$; so $\mathrm{Sid}(r)$ is false for all $r\ge 22$, and the open question is the exact threshold, the largest $r$ for which $\mathrm{Sid}(r)$ holds, somewhere between $4$ and $21$. $\mathrm{Sid}(5)$, which contains $K_{5,5}\setminus C_{10}$, is the first rung not covered by Sidorenko's theorem.

Significance

The conjecture determines the minimum number of copies of every bipartite graph in graphs of given density, the bipartite half of the subgraph-counting problem whose non-bipartite half (for which the random graph is not extremal, by Thomason's examples) is far less understood. It is equivalent to the statement that every bipartite graph is "common" in the sense of Erdős and to the positivity of a class of graphon integrals; it would also settle a conjecture of Simonovits on the Turán numbers of bipartite graphs in the degenerate regime. The rungs with $r\le 4$ are proved and the rungs with $r\ge 22$ are refuted, if the counterexample stands; the rungs $5\le r\le 21$ are open.

Formalizing the conjecture builds homomorphism counting on Mathlib's SimpleGraph, which has graph homomorphisms but no density theory: the Cauchy–Schwarz and tensor-power arguments for trees and even cycles, the entropy method, and the vertex-complete theorem would all become reusable. No positive case of Sidorenko's conjecture has a machine-checked proof; the counterexample does, in OpenAI's Lean development, with its own definitions of homomorphism density.

Difficulty

The obvious approach, applying Cauchy–Schwarz edge by edge, proves the inequality only for graphs that can be built by repeated "gluing" along stars, which is why trees, even cycles and complete bipartite graphs are the easy cases. The known proofs for harder graphs replace Cauchy–Schwarz by entropy inequalities on random homomorphisms, and the entropy method is known to fail for some graphs on five plus five vertices. OpenAI's counterexample beats the random graph for a specific $35$-vertex $H$; which smaller graphs, if any, fail the inequality remains unknown, and the known positive methods still say nothing about the rungs between $5$ and $21$.

Formalization scope

Graphs are Mathlib's SimpleGraph on finite types W (for $H$) and V (for $G$), both in Type; the host $G$ has [Nonempty V], so $|V(G)|\ge 1$ and the density is a genuine quotient. homDensity H G : ℝ is Nat.card of the subtype of maps $W\to V$ sending adjacent vertices to adjacent vertices, divided by $|V|^{|W|}$ as real numbers; SidorenkoFor H G is the inequality $t(H,G)\ge t(K_2,G)^{e(H)}$ with $K_2$ = completeGraph (Fin 2) and $e(H)$ = Nat.card H.edgeSet. BipartiteBoundedBy H k asks for sets $X,Y$ with Mathlib's H.IsBipartiteWith X Y (disjoint, every edge between them), $X\cup Y$ the whole vertex set, and X.ncard ≤ k, Y.ncard ≤ k. The rung statement_04 r quantifies over all such $H$ and all nonempty finite $G$. The goal states the conjecture directly: for every finite $H$ admitting sets $X,Y$ with H.IsBipartiteWith X Y and $X\cup Y$ the whole vertex set, and every nonempty finite $G$, SidorenkoFor H G; it is equivalent to ∀ r, statement_04 r, the universal form of the benchmark.

No trivialising reading: both sides are real numbers in $[0,1]$, the exponent counts edges of $H$ exactly, and for $r=0$ the only admissible $H$ is the empty graph, for which both sides equal $1$. 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: a transport of OpenAI's Lean counterexample to the definitions here (a disproof of the goal and of the rung $r=22$), the multiplicativity of $\hom$ over disjoint unions, $t(K_2,G)=2e(G)/n^2$, the tree and even-cycle cases, a reduction of $\mathrm{Sid}(r)$ to a finite list of graphs $H$ for small $r$.

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 4).
• A. F. Sidorenko, Inequalities for functionals generated by bipartite graphs, Diskret. Mat. 3 (1991), 50–65 (Russian); English translation Discrete Math. Appl. 2 (1992), 489–504. https://doi.org/10.1515/dma.1992.2.5.489
• A. F. Sidorenko, A correlation inequality for bipartite graphs, Graphs Combin. 9 (1993), 201–204. https://doi.org/10.1007/BF02988307
• H. Hatami, Graph norms and Sidorenko's conjecture, Israel J. Math. 175 (2010), 125–150. https://doi.org/10.1007/s11856-010-0005-1
• D. Conlon, J. Fox, B. Sudakov, An approximate version of Sidorenko's conjecture, Geom. Funct. Anal. 20 (2010), 1354–1366. https://doi.org/10.1007/s00039-010-0097-0
• J. L. X. Li, B. Szegedy, On the logarithmic calculus and Sidorenko's conjecture, 2011. https://arxiv.org/abs/1107.1153
• B. Szegedy, An information theoretic approach to Sidorenko's conjecture, 2015. https://arxiv.org/abs/1406.6738
• J. H. Kim, C. Lee, J. Lee, Two approaches to Sidorenko's conjecture, Trans. Amer. Math. Soc. 368 (2016), 5057–5074. https://doi.org/10.1090/tran/6487
• D. Conlon, J. H. Kim, C. Lee, J. Lee, Some advances on Sidorenko's conjecture, J. London Math. Soc. 98 (2018), 593–608. https://doi.org/10.1112/jlms.12142
• D. Conlon, J. Lee, Sidorenko's conjecture for blow-ups, Discrete Analysis 2021:2. https://doi.org/10.19086/da.21472

Motivation

A partition of the vertices of a graph into two classes is unfriendly if every vertex has at least as many neighbours in the other class as in its own. Every finite graph has one: a partition with the maximum number of crossing edges. For infinite graphs the question is the unfriendly partition conjecture of Cowan and Emerson: does every countable graph have an unfriendly partition? Shelah and Milner showed that uncountable graphs need not, and the countable case has been open since the 1980s, with positive answers for locally finite graphs, graphs with finitely many vertices of infinite degree, and rayless graphs (Aharoni–Milner–Prikry 1990, Shelah–Milner 1990, Bruhn–Diestel–Georgakopoulos–Sprüssel 2010).

This challenge scales the conjecture through a game. The parameter is an ordinal $r$, the clock: Challenger repeatedly names a vertex and lowers the clock, and Partitioner must extend a finite partial partition so that the named vertex becomes unfriendly. An unfriendly partition of the whole graph gives Partitioner a winning strategy for every clock, so the full conjecture implies every rung, and the rungs with transfinite clocks measure how much of an unfriendly partition can be built on demand.

Timeline.

• 1980s — Cowan and Emerson pose the conjecture.
• 1990 — Aharoni, Milner and Prikry prove it for graphs with only finitely many vertices of infinite degree, in particular for locally finite graphs (Aharoni–Milner–Prikry 1990).
• 1990 — Shelah and Milner construct uncountable graphs without unfriendly partitions (Shelah–Milner 1990).
• 2010 — Bruhn, Diestel, Georgakopoulos and Sprüssel prove it for rayless graphs of any cardinality (Bruhn–Diestel–Georgakopoulos–Sprüssel 2010).
• 2017 — Berger proves it for graphs containing no subdivision of an infinite clique (Berger 2017).

Setting

Let $G$ be a graph with vertex set $V$. A partial partition is a partial function $f\colon V\rightharpoonup\{0,1\}$; it is finite if its domain is finite, and a partition if it is total. Write $N(v)$ for the neighbourhood of $v$. A partial partition $f$ is unfriendly at $v$ if $f(v)$ is defined and

$$\big|N(v)\cap f^{-1}[1-f(v)]\big|\ \ge\ \big|N(v)\cap f^{-1}[f(v)]\big|,$$

as cardinal numbers; neighbours outside the domain of $f$ are not counted. A partition is unfriendly if it is unfriendly at every vertex.

The $r$-partitioning game. For an ordinal $r$, a position is a pair $(f,\alpha)$ of a partial partition and an ordinal, the initial position is $(\emptyset,r)$. In each turn from $(f,\alpha)$, Challenger names a vertex $v$ and an ordinal $\beta<\alpha$; Partitioner must answer with a finite partial partition $g$ extending $f$ (preserving all assignments of $f$) that is unfriendly at $v$; the new position is $(g,\beta)$. A player unable to move loses; since ordinals have no infinite descending sequences, the game ends after finitely many turns, and Partitioner wins if Challenger runs out of moves. For an ordinal $r$ let

$$\mathrm{UP}(r):\quad \text{Partitioner has a winning strategy in the } r\text{-partitioning game on every countable graph.}$$

Formalization targets

Goal

$$\text{every countable graph has an unfriendly partition,}$$

the unfriendly partition conjecture of Cowan and Emerson. A partial partition that is unfriendly at every vertex is total, so the goal is stated with the same notion of unfriendliness as the game.

The scaled form

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

Partitioner wins the $r$-partitioning game on every countable graph for every ordinal clock. An unfriendly partition yields a winning strategy for every clock, so the goal implies the scaled form; the rungs are the scaled form for particular clocks and particular classes of graphs.

Rungs

Any graph with an unfriendly partition yields a winning strategy for every clock: Partitioner reveals the partition on a finite set containing the named vertex and the finitely many coloured neighbours needed. Hence every finite graph, every countable locally finite graph, and every countable rayless graph satisfies all rungs. For finite clocks $r=n$ the statement is an exercise; the rung $r=\omega$ is the first with an infinite clock.

Significance

The unfriendly partition conjecture is the basic open question about majority colourings of infinite graphs, and its scaled form isolates how the difficulty grows with the "transfinite length" of the commitment required: with clock $\omega$, Challenger must announce in advance how many more vertices will be challenged, with clock $\omega\cdot 2$ once more, and so on. The full statement is implied by the conjecture; how much of the conjecture the game recovers in return is part of what the scaled version is designed to probe.

Nothing about unfriendly partitions is formalized; Mathlib has simple graphs on arbitrary types and cardinals, but neither majority conditions nor the compactness argument for locally finite graphs. The finite-clock rungs, the finite-graph case and the locally finite case are reachable formalization projects; the infinite-clock rungs are open.

Difficulty

The max-cut argument of the finite case has no infinite analogue: a vertex of infinite degree can be unfriendly only through a cardinality comparison, and attempts to build a partition by transfinite induction run into vertices whose status is changed by later decisions. The known positive results use a careful ordering of the vertices of infinite degree or a structural decomposition (rayless graphs); none of them gives any information about graphs with infinitely many vertices of infinite degree and infinite paths. In the game, the naive strategy of colouring only the challenged vertex fails because Challenger can later challenge a coloured vertex all of whose finitely many neighbours have already been coloured badly.

Formalization scope

Graphs are Mathlib's SimpleGraph V with V in a universe u and the hypothesis Countable V; partial partitions are functions V → Option Bool, with none for undefined and some b for class $b$. NeighColored G f v b is the type of neighbours of $v$ with value $b$, and UnfriendlyAt G f v requires some b with f v = some b and the cardinal inequality #(neighbours coloured b) ≤ #(neighbours coloured !b) (Mathlib's Cardinal.mk). emptyPartition V is the constant none; HasFiniteDomain, Extends and IsLegalResponse G f g v (extends, finite domain, unfriendly at $v$) are as in the Setting. PartitionerWins G f α is defined by well-founded recursion on the ordinal α : Ordinal.{v}: for every vertex $v$ and every $\beta<\alpha$ there is a legal response $g$ with PartitionerWins G g β. The rung statement_10 r is PartitionerWins G (emptyPartition V) r for every countable V and every G; the scaled form is ∀ r, statement_10 r. The goal is ∃ f : V → Option Bool, ∀ v, UnfriendlyAt G f v for every countable V and every G: since UnfriendlyAt requires f v to be defined, such an f assigns a class to every vertex and is an unfriendly partition in the usual sense.

No trivialising reading: with clock $0$ Partitioner wins vacuously, which is the intended base case; responses must be finite, so Partitioner cannot reveal a whole infinite partition at once; and the cardinal comparison is exactly the majority condition on coloured neighbours. The universes of V and of the ordinal are independent parameters. 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: the lemma that an unfriendly partition yields PartitionerWins for every clock, monotonicity of PartitionerWins in the clock, the finite-graph and locally finite cases, the finite-clock rungs, and the relation between winning for all countable clocks and the existence of an unfriendly partition.

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 10).
• R. Aharoni, E. C. Milner, K. Prikry, Unfriendly partitions of a graph, J. Combin. Theory Ser. B 50 (1990), 1–10. https://doi.org/10.1016/0095-8956(90)90092-E
• S. Shelah, E. C. Milner, Graphs with no unfriendly partitions, in: A Tribute to Paul Erdős, Cambridge University Press, 1990, 373–384.
• H. Bruhn, R. Diestel, A. Georgakopoulos, P. Sprüssel, Every rayless graph has an unfriendly partition, Combinatorica 30 (2010), 521–532. https://doi.org/10.1007/s00493-010-2590-3
• E. Berger, Unfriendly partitions for graphs not containing a subdivision of an infinite clique, Combinatorica 37 (2017), 157–166. https://doi.org/10.1007/s00493-015-3261-1
• R. Diestel, Graph Theory, 5th ed., Springer, 2017, Chapter 8. https://doi.org/10.1007/978-3-662-53622-3

Motivation

The sphere packing problem asks for the largest fraction of $\mathbb R^d$ that can be covered by non-overlapping unit balls. The densest packings known in most dimensions are lattice packings, whose centres form a lattice, and for $d\in\{1,2,3,8,24\}$ a lattice packing is known to be optimal among all packings. But in several dimensions, $d=10$ being the first, the densest packing known is not a lattice packing and is denser than the best lattice packing known (Conway–Sloane 1999). Whether the sphere-packing constant and the lattice-packing constant agree in every dimension is open; the answer may well be negative, and this challenge is a question rather than a conjecture.

Timeline.

• 1611 — Kepler asserts that the face-centred cubic packing is densest in dimension $3$.
• 1773/1831 — Lagrange and Gauss show that the hexagonal and face-centred cubic lattices are the densest lattice packings in dimensions $2$ and $3$.
• 1910/1940 — Thue and Fejes Tóth prove the hexagonal packing optimal among all packings of the plane (Fejes Tóth 1940).
• 1998/2005 — Hales proves the Kepler conjecture; the Flyspeck project completes a formal proof in HOL Light and Isabelle in 2014 (Hales 2005, Hales et al. 2017).
• 2016 — Viazovska proves that the $E_8$ lattice packing is optimal in dimension $8$; Cohn, Kumar, Miller, Radchenko and Viazovska prove that the Leech lattice packing is optimal in dimension $24$ (Viazovska 2017, Cohn–Kumar–Miller–Radchenko–Viazovska 2017).
• 2024–2026 — The Sphere Packing project formalizes Viazovska's theorem in Lean 4, with the final steps completed in 2026 (Sphere Packing in Lean).

Setting

Fix $d\ge 1$ and equip $\mathbb R^d$ with the Euclidean distance and Lebesgue measure $\mathrm{Vol}$; $B(x,\rho)$ is the open ball of radius $\rho$ about $x$. A unit packing is a set $C\subseteq\mathbb R^d$ of centres with $\|x-y\|\ge 2$ for all distinct $x,y\in C$, so the open unit balls about the points of $C$ are pairwise disjoint. Its upper density is

$$\bar\delta(C) := \limsup_{R\to\infty}\ \frac{\mathrm{Vol}\big(\bigcup_{x\in C}B(x,1)\cap B(0,R)\big)}{\mathrm{Vol}(B(0,R))}.$$

The sphere-packing constant $\Delta_d$ is the supremum of $\bar\delta(C)$ over all unit packings $C$ of $\mathbb R^d$. A lattice packing is a unit packing $L$ that is an additive subgroup of $\mathbb R^d$ spanning $\mathbb R^d$; the separation condition forces $L$ to be discrete, hence a full-rank lattice. The lattice-packing constant $\Delta_d^L$ is the supremum of $\bar\delta(L)$ over lattice packings. Trivially $\Delta_d^L\le\Delta_d$. For $r\in\mathbb N$ let

$$\mathrm{SP}(r):\quad \Delta_r=\Delta_r^L .$$

Formalization targets

Goal

$$\forall r\in\mathbb N:\quad \Delta_r=\Delta_r^L .$$

A disproof, exhibiting a dimension in which some non-lattice packing beats every lattice packing, is as welcome as a proof.

Rungs

$\mathrm{SP}(r)$ is known for $r\in\{1,2,3,8,24\}$; $\mathrm{SP}(4)$ is the first open rung. In dimensions $4$ to $7$ the densest lattice packings are known ($D_4$, $D_5$, $E_6$, $E_7$; Korkine–Zolotarev, Blichfeldt), so only the general constant is missing there.

Significance

The equality $\Delta_d=\Delta_d^L$ is the statement that lattices suffice for sphere packing. In dimension $3$ it is the Kepler conjecture (since $\Delta_3^L$ was known from Gauss), in dimensions $8$ and $24$ it is the content of the Fields-medal work of Viazovska and her coauthors. A counterexample would be a dimension in which non-lattice packings are provably better, which is expected in high dimensions but not proved in any.

The rungs $r=8$ and $r=24$ have machine-checked proofs in the Lean Sphere Packing project, in its own definitions; transferring them to the definitions here means proving that the two formalizations of density agree, which is a substantial but well-defined task. The rung $r=3$ has a formal proof in HOL Light and Isabelle (Flyspeck), not in Lean. The rungs $r=1$ and $r=2$ have no machine-checked proof; $r=1$ is an exercise once the density of a packing of the line is computed, while $r=2$ needs the Thue–Fejes Tóth theorem.

Difficulty

Upper bounds on $\Delta_d$ are the hard direction: the known proofs use the linear-programming bound of Cohn and Elkies and a magic modular form (dimensions $8$, $24$), or a computer-assisted analysis of local configurations (dimension $3$). The lattice constant is comparatively tractable, which is why the question stands exactly where the general constant is unknown. The naive approach, that the densest packing must have the symmetry of a lattice, is unfounded: in dimension $10$ Best's packing is denser than any known lattice, and in high dimensions the best known packings are periodic but not lattice.

Formalization scope

Points are EuclideanSpace ℝ (Fin d) with its volume (the Lebesgue measure through Mathlib's Haar measure), and a packing is a set C : Set (EuclideanSpace ℝ (Fin d)). IsUnitPacking C requires $2\le\mathrm{dist}(x,y)$ for distinct $x,y\in C$. upperDensity C : ℝ≥0∞ is limsup over $R\to\infty$ (Filter.atTop on $\mathbb R$) of the quotient of extended nonnegative reals above; spherePackingConstant d is the indexed supremum ⨆ over all sets $C$ satisfying IsUnitPacking C, and latticePackingConstant d the supremum over AddSubgroups $L$ of the space whose carrier is a unit packing and whose real span is the whole space. The rung statement_07 r is the equality of the two constants in ℝ≥0∞, and the goal is ∀ r, statement_07 r.

No trivialising reading: densities are at most $1$, the supremum over the empty family is $0$, and for $d=0$ both constants trivially coincide. Densities are extended nonnegative reals, so no real-valuedness hypotheses are needed; the quotient uses the convention of ℝ≥0∞ division, harmless since $\mathrm{Vol}(B(0,R))>0$ for $R>0$. 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: the inequality $\Delta_d^L\le\Delta_d$, the bound $\Delta_d\le 1$, periodification lemmas, the density of a lattice packing as $\mathrm{Vol}(B(0,1))/\mathrm{covol}(L)$, and the bridge to the Sphere Packing project's definitions.

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 7).
• J. H. Conway, N. J. A. Sloane, Sphere Packings, Lattices and Groups, 3rd ed., Springer, 1999. https://doi.org/10.1007/978-1-4757-6568-7
• L. Fejes Tóth, Über einen geometrischen Satz, Math. Z. 46 (1940), 83–85. https://doi.org/10.1007/BF01181430
• T. C. Hales, A proof of the Kepler conjecture, Ann. of Math. 162 (2005), 1065–1185. https://doi.org/10.4007/annals.2005.162.1065
• T. Hales et al., A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2. https://doi.org/10.1017/fmp.2017.1
• M. S. Viazovska, The sphere packing problem in dimension 8, Ann. of Math. 185 (2017), 991–1015. https://doi.org/10.4007/annals.2017.185.3.7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, The sphere packing problem in dimension 24, Ann. of Math. 185 (2017), 1017–1033. https://doi.org/10.4007/annals.2017.185.3.8
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math. 157 (2003), 689–714. https://doi.org/10.4007/annals.2003.157.689
• The Sphere Packing project, Progress in formalizing sphere packing in dimension 8, 2026. https://arxiv.org/abs/2604.23468 — code: https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean

Motivation

In a finite directed graph in which every vertex has an out-neighbour, following arcs must eventually return to a visited vertex, so a directed cycle exists; but it may be long. The Caccetta–Häggkvist conjecture quantifies how large minimum out-degree forces short directed cycles: out-degree at least $r$ on $n$ vertices should force a directed cycle of length at most $\lceil n/r\rceil$. The circulant digraph on $\mathbb Z/n$ with arcs $v\to v+1,\dots,v+r$ shows that nothing better is possible. The conjecture is a central open problem on digraphs, with connections to the Erdős–Szekeres-type and Ramsey-type questions on tournaments and to the "directed triangle" problem for dense digraphs (Sullivan 2006).

Timeline.

• 1978 — Caccetta and Häggkvist pose the conjecture and prove it for $r=2$ (Caccetta–Häggkvist 1978).
• 1987 — Hamidoune proves the case $r=3$ (Hamidoune 1987).
• 1987 — Hoàng and Reed prove the cases $r=4$ and $r=5$ (Hoàng–Reed 1987).
• 1998 — Shen shows that minimum out-degree at least $(3-\sqrt7)\,n\approx 0.3542\,n$ forces a directed triangle, the first step on the dense case $r=n/3$ (Shen 1998).
• 2000 — Shen proves the conjecture for every $r$ whenever $n\ge 2r^2-3r+1$ (Shen 2000).
• 2017 — Hladký, Král' and Norin lower the triangle threshold to $0.3465\,n$ (Hladký–Král'–Norin 2017).

The cases $r\ge 6$ are open for general $n$.

Setting

A digraph $D$ consists of a finite vertex set $V$ and a set of arcs, ordered pairs $(v,w)$ of distinct vertices; at most one arc from $v$ to $w$, no loops, and arcs in both directions between two vertices are allowed. The out-degree $d^+(v)$ is the number of $w$ with an arc $(v,w)$. A directed cycle of length $\ell\ge 2$ is a sequence $v_0,\dots,v_{\ell-1}$ of distinct vertices with an arc $(v_i,v_{i+1})$ for every $i$, indices modulo $\ell$. For $r\ge 1$ let $\mathrm{CH}(r)$ be the statement

$$\text{every digraph on } n\ge 1 \text{ vertices with } d^+(v)\ge r \text{ for all } v \text{ has a directed cycle of length at most } \lceil n/r\rceil .$$

The condition $\ell\le\lceil n/r\rceil$ is the same as $\ell r<n+r$.

Formalization targets

Goal

$$\forall r\ge 1:\quad \mathrm{CH}(r).$$

Rungs

$$\mathrm{CH}(1),\ \mathrm{CH}(2),\ \mathrm{CH}(3),\ \mathrm{CH}(4),\ \mathrm{CH}(5),$$

and the first open rung $\mathrm{CH}(6)$.

Significance

The conjecture would determine exactly the smallest girth a digraph of given order and minimum out-degree can have, a directed analogue of the Moore-type bounds for undirected graphs; its dense case, that out-degree $n/3$ forces a directed triangle, is itself a well-known open problem and implies results on the number of edges in digraphs without short cycles. Partial results have produced the main tools of extremal digraph theory: Shen's counting arguments, the flag-algebra computations of Hladký, Král' and Norin, and the structural approach of Chudnovsky, Seymour and Sullivan to the triangle case.

Formalizing the known rungs gives Mathlib a working theory of directed cycles and out-degrees, which it does not have. The rung $\mathrm{CH}(1)$ is an exercise; $\mathrm{CH}(2)$ is a two-page argument; $\mathrm{CH}(3)$, $\mathrm{CH}(4)$ and $\mathrm{CH}(5)$ are short papers. None of them has a machine-checked proof. $\mathrm{CH}(6)$ and beyond are open.

Difficulty

The natural induction, removing a vertex of small out-degree or contracting a short cycle, fails because contraction can create parallel arcs or loops and because the minimum out-degree is not preserved; the known proofs for $r\le 5$ are delicate counting arguments on the neighbourhoods of a shortest cycle, and each new value of $r$ has required a new idea. Shen's theorem settles the conjecture only when $n$ is quadratic in $r$, and the dense regime $r\approx n/3$ is open even for triangles.

Formalization scope

Digraphs are Mathlib's Digraph V with [Fintype V] [Nonempty V]; the adjacency relation is arbitrary, so looplessness is an explicit hypothesis ∀ v, ¬ G.Adj v v, while arcs in both directions between two vertices are permitted. The out-degree of $v$ is {w | G.Adj v w}.ncard. A directed cycle of length $\ell$ is an injective map $f\colon\mathrm{Fin}\,\ell\to V$ with an arc from $f(i)$ to $f(i+1)$ for every $i$, the successor taken cyclically (finRotate). CaccettaHaggkvistFor r states: if $0<r$, then every such digraph in which every vertex has out-degree at least $r$ has a directed cycle of some length $\ell$ with $2\le\ell$ and $\ell r<n+r$, where $n$ is the number of vertices. The rung statement_03 r is CaccettaHaggkvistFor r, and the goal quantifies over all $r$; the case $r=0$ is vacuous by the guard $0<r$. Vertex types are in Type (the lowest universe).

No trivialising reading: the length bound $\ell r<n+r$ is exactly $\ell\le\lceil n/r\rceil$, cycles of length $2$ are genuine directed cycles, and the out-degree condition is on every vertex. 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 on HasCycleOfLength (closed walks contain cycles, reversal, blow-ups), the rung $\mathrm{CH}(1)$, and decompositions of $\mathrm{CH}(2)$.

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 3).
• L. Caccetta, R. Häggkvist, On minimal digraphs with given girth, Proc. 9th Southeastern Conf. on Combinatorics, Graph Theory and Computing (1978), Congr. Numer. 21, 181–187.
• Y. O. Hamidoune, A note on minimal directed graphs with given girth, J. Combin. Theory Ser. B 43 (1987), 343–348. https://doi.org/10.1016/0095-8956(87)90009-8
• C. T. Hoàng, B. Reed, A note on short cycles in digraphs, Discrete Math. 66 (1987), 103–107. https://doi.org/10.1016/0012-365X(87)90122-1
• J. Shen, Directed triangles in digraphs, J. Combin. Theory Ser. B 74 (1998), 405–407. https://doi.org/10.1006/jctb.1998.1839
• J. Shen, On the girth of digraphs, Discrete Math. 211 (2000), 167–181. https://doi.org/10.1016/s0012-365x(99)00323-4
• B. D. Sullivan, A summary of results and problems related to the Caccetta–Häggkvist conjecture, 2006. https://arxiv.org/abs/math/0605646
• J. Hladký, D. Král', S. Norin, Counting flags in triangle-free digraphs, Combinatorica 37 (2017), 49–76. https://doi.org/10.1007/s00493-015-2662-5
• J. Bang-Jensen, G. Gutin, Digraphs: Theory, Algorithms and Applications, 2nd ed., Springer, 2009. https://doi.org/10.1007/978-1-84800-998-1

Motivation

Ramsey's theorem guarantees that every graph on $n$ vertices has a clique or an independent set of size about $\tfrac12\log_2 n$, and random graphs show that this is best possible. The Erdős–Hajnal conjecture says that forbidding any single induced subgraph $H$ changes the picture completely: $H$-free graphs should contain cliques or independent sets of polynomial size $n^{c_H}$. The conjecture is a central problem of structural graph theory, linking induced subgraphs, perfect graphs and Ramsey theory (Chudnovsky 2014).

Timeline.

• 1977/1989 — Erdős and Hajnal pose the conjecture and prove that $H$-free graphs contain cliques or independent sets of size $\exp(c\sqrt{\log n})$ (Erdős–Hajnal 1989).
• 2001 — Alon, Pach and Solymosi show that the conjecture is closed under substitution, giving it for a family of graphs built from small cases (Alon–Pach–Solymosi 2001).
• 2008 — Chudnovsky and Safra prove it for the bull (Chudnovsky–Safra 2008).
• 2023 — Chudnovsky, Scott, Seymour and Spirkl prove it for the five-vertex cycle (Chudnovsky–Scott–Seymour–Spirkl 2023).
• 2023 — Bucić, Nguyen, Scott and Seymour improve the general bound to $\exp(c\sqrt{\log n\log\log n})$ (Bucić–Nguyen–Scott–Seymour 2023).
• 2023/2026 — Nguyen, Scott and Seymour prove it for the five-vertex path $P_5$, completing all graphs on five vertices; they also show that for every path $P$ and every $d<1$, $P$-free graphs contain cliques or independent sets of size $2^{(\log n)^d}$ (Nguyen–Scott–Seymour, ISD V, ISD VII).

The conjecture is open for the six-vertex path $P_6$, and for every longer path.

Setting

All graphs are finite and simple. A set of vertices is a clique if its vertices are pairwise adjacent and an independent set (or stable set) if they are pairwise non-adjacent. For graphs $G$ and $H$, $G$ is $H$-free if no induced subgraph of $G$ is isomorphic to $H$. The path $P_r$ has $r$ vertices $v_1,\dots,v_r$ and edges $v_iv_{i+1}$. For $r\in\mathbb N$ let $\mathrm{EH}(r)$ be the statement

$$\exists\, c>0\ \ \forall G\ P_r\text{-free}:\quad G \text{ has a clique or an independent set of size at least } |V(G)|^{c}.$$

The constant $c$ may depend on $r$ but not on $G$.

Formalization targets

Goal

$$\forall r\in\mathbb N:\quad \mathrm{EH}(r).$$

Rungs

$\mathrm{EH}(4)$ ($P_4$-free graphs are cographs, hence perfect, and $c=\tfrac12$ works), $\mathrm{EH}(5)$ (Nguyen, Scott, Seymour), and the first open rung $\mathrm{EH}(6)$. The rungs $r\le 3$ are exercises: $P_2$-free graphs are edgeless, $P_3$-free graphs are disjoint unions of cliques.

Significance

Paths are the test case for the conjecture: a proof for all paths would, by the substitution theorem and the known closure properties, settle it for a large class of graphs, and the methods developed for $P_5$ (sparse–dense dichotomies, "polynomial Rödl" theorems) are the current state of the art. The weaker near-polynomial bound $2^{(\log n)^{1-o(1)}}$ is known for all paths, so the gap to be closed is precisely the exponent.

Formalizing the rungs builds the induced-subgraph vocabulary (induced embeddings of paths, cographs, the clique–independent set dichotomy) on top of Mathlib's SimpleGraph. $\mathrm{EH}(4)$ via perfection of cographs is a realistic first project; $\mathrm{EH}(5)$ is a long paper with no machine-checked proof. The goal and $\mathrm{EH}(6)$ are open.

Difficulty

The Erdős–Hajnal argument gives only $\exp(c\sqrt{\log n})$ because each step of its density increment loses a constant factor; the polynomial regime requires structure specific to the forbidden graph. For $P_5$ the proof needs a new "polynomial" version of Rödl's theorem for $P_5$-free graphs together with a delicate analysis of sparse and dense configurations; none of it is known to extend to $P_6$. The naive idea, induction on $r$ by deleting a vertex, loses the forbidden structure.

Formalization scope

Graphs are Mathlib's SimpleGraph V with [Fintype V] and V : Type (the lowest universe); $H$-freeness is ¬ H ⊴ G with Mathlib's induced-subgraph relation ⊴ (an injective graph homomorphism that reflects adjacency). ErdosHajnalConjectureFor H states: there is a real $c>0$ such that every finite $H$-free graph $G$ has a Finset $s$ which is a clique of $G$ or a clique of the complement $G^{c}$, with $|s|\ge |V|^{c}$ as real numbers (real exponentiation). The rung statement_05 r is ErdosHajnalConjectureFor (pathGraph r), with Mathlib's pathGraph r on Fin r. For $r\le 1$ the path embeds in every graph with enough vertices, so the hypothesis is vacuous or nearly so; the content starts at $r=2$. The goal is ∀ r, statement_05 r.

No trivialising reading: $c$ is chosen before $G$, the empty graph on $0$ vertices satisfies the conclusion with $s=\emptyset$ since $0^c=0$, and the clique-or-independent-set alternative is genuine. 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: an API for $P_r$-freeness (characterisations of $P_3$-free and $P_4$-free graphs), perfection of cographs, the exercises $r\le 3$, decompositions of $\mathrm{EH}(4)$ and $\mathrm{EH}(5)$.

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 5).
• P. Erdős, A. Hajnal, Ramsey-type theorems, Discrete Appl. Math. 25 (1989), 37–52. https://doi.org/10.1016/0166-218X(89)90045-0
• M. Chudnovsky, The Erdős–Hajnal conjecture: a survey, J. Graph Theory 75 (2014), 178–190. https://doi.org/10.1002/jgt.21730
• N. Alon, J. Pach, J. Solymosi, Ramsey-type theorems with forbidden subgraphs, Combinatorica 21 (2001), 155–170. https://doi.org/10.1007/s004930100016
• M. Chudnovsky, S. Safra, The Erdős–Hajnal conjecture for bull-free graphs, J. Combin. Theory Ser. B 98 (2008), 1301–1310. https://doi.org/10.1016/j.jctb.2008.02.005
• M. Chudnovsky, A. Scott, P. Seymour, S. Spirkl, Erdős–Hajnal for graphs with no 5-hole, Proc. London Math. Soc. 126 (2023), 997–1014. https://doi.org/10.1112/plms.12504
• M. Bucić, T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. I. A loglog step towards Erdős–Hajnal, 2023. https://arxiv.org/abs/2301.10147
• T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. V. All paths approach Erdős–Hajnal, 2023. https://arxiv.org/abs/2307.15032
• T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. VII. The five-vertex path, Proc. London Math. Soc. (2026). https://arxiv.org/abs/2312.15333

Motivation

For bipartite graphs, Kőnig's theorem says that the minimum number of vertices needed to meet every edge equals the maximum number of pairwise disjoint edges: $\tau=\nu$. For hypergraphs whose edges have $r$ vertices, the ratio $\tau/\nu$ can be as large as $r$ in general, and the bound $\tau\le r\nu$ is trivial. Ryser's conjecture asserts that for $r$-partite $r$-uniform hypergraphs, the natural generalisation of bipartite graphs, the trivial bound can be improved by one:

$$\tau(\mathcal H)\le (r-1)\,\nu(\mathcal H).$$

For $r=2$ it is Kőnig's theorem. Truncated projective planes show that the factor $r-1$ cannot be lowered when $r-1$ is a prime power. The conjecture is a central problem on matchings and covers in hypergraphs (Aharoni 2001, Haxell–Scott 2012).

Timeline.

• 1931 — Kőnig proves $\tau=\nu$ for bipartite graphs, the case $r=2$.
• 1971 — The conjecture appears in the thesis of Ryser's student Henderson; the case $\nu=1$ is attributed to Lovász.
• 1983 — Tuza proves the intersecting case $\nu=1$ for $r\le 5$ (Tuza 1983).
• 2001 — Aharoni proves the case $r=3$ using the topological Hall theorem of Aharoni and Haxell (Aharoni 2001).
• 2012 — Haxell and Scott prove $\tau\le (r-\varepsilon)\nu$ for $r=4,5$ and some $\varepsilon>0$ (Haxell–Scott 2012).
• 2017–2021 — Francetić, Herke, McKay and Wanless, then Abu-Khazneh, Barát, Pokrovskiy and Szabó, construct families of extremal hypergraphs; Bishnoi, Das, Morris and Szabó settle the $t$-intersecting case (Abu-Khazneh et al. 2019, Bishnoi et al. 2021).

The case $r=4$ is open.

Setting

A hypergraph $\mathcal H$ has a finite vertex set $V(\mathcal H)$ and a set $E(\mathcal H)$ of edges, each a subset of $V(\mathcal H)$. It is $r$-uniform if every edge has exactly $r$ vertices, and $r$-partite if $V(\mathcal H)$ is the disjoint union of parts $P_1,\dots,P_r$ such that every edge meets every part in exactly one vertex. A vertex cover is a set $C\subseteq V(\mathcal H)$ meeting every edge; the cover number $\tau(\mathcal H)$ is the least size of a vertex cover. A matching is a set of pairwise disjoint edges; the matching number $\nu(\mathcal H)$ is the largest size of a matching. For $r\in\mathbb N$ let $\mathrm{Ry}(r)$ be the statement

$$r\ge 2 \implies \text{every } r\text{-partite } r\text{-uniform hypergraph } \mathcal H \text{ satisfies } \tau(\mathcal H)\le (r-1)\,\nu(\mathcal H).$$

Formalization targets

Goal

$$\forall r\in\mathbb N:\quad \mathrm{Ry}(r).$$

Rungs

$\mathrm{Ry}(2)$ is Kőnig's theorem, $\mathrm{Ry}(3)$ is Aharoni's theorem, and $\mathrm{Ry}(4)$ is the first open rung. For $r\le 1$ the statement is vacuous.

Significance

Ryser's conjecture is the hypergraph form of Kőnig's theorem and one of the standard open problems in the matching theory of hypergraphs. Its intersecting case ($\nu=1$) is equivalent to a question about the covering number of Latin-square-like structures and is open for $r\ge 6$; its fractional version, $\tau\le (r-1)\nu^*$, was proved by Füredi. A proof for $r=4$ would be the first progress on the full conjecture since Aharoni's theorem.

Formalizing the known rungs gives a theory of finite hypergraphs, covers and matchings on top of Mathlib's Finset, which currently has Kőnig's theorem only in graph form (Hall's marriage theorem is in Mathlib). Aharoni's proof for $r=3$ goes through the topological Hall theorem, so a formalization would need the connectivity of independence complexes, a sizeable but reusable piece of topological combinatorics. None of the rungs has a machine-checked proof in the hypergraph formulation; $\mathrm{Ry}(4)$ and the goal are open.

Difficulty

The bound $\tau\le r\nu$ comes from taking all vertices of a maximum matching; improving it by a factor $(r-1)/r$ requires exploiting the partition, and no inductive or greedy argument is known to do so beyond $r=3$. Aharoni's proof for $r=3$ is non-constructive and topological, and the topological Hall theorem gives for general $r$ only $\tau\le r\nu$-type bounds; the $\varepsilon$-improvements of Haxell and Scott already require long case analyses. The conjecture is tight for infinitely many $r$, so no slack is available.

Formalization scope

A hypergraph is the structure FinHypergraph α with vertices : Finset α, edges : Set (Finset α) and the axiom that every edge is a subset of vertices; since edges are finite subsets of a finite set, there are finitely many. IsUniform r, IsPartite r (parts indexed by Fin r, covering the vertex set, pairwise disjoint, each meeting each edge in exactly one vertex), IsVertexCover C (a subset of the vertices meeting every edge) and IsMatching M (a Finset of edges, pairwise disjoint) are as in the Setting. coverNumber is the infimum sInf of the sizes of vertex covers, and matchingNumber the supremum sSup of the sizes of matchings; both are natural numbers, with the conventions $\inf\emptyset=0$ and $\sup$ of an unbounded set $=0$, which never arise since the vertex set covers every edge whenever edges are nonempty and matchings are bounded by the number of edges. RyserConjectureFor H r is $\tau\le(r-1)\nu$ under the uniformity and partiteness hypotheses, statement_08 r adds the guard $2\le r$ and quantifies over all vertex types with decidable equality in a universe u, and the goal is ∀ r, statement_08 r.

No trivialising reading: $r=0$ and $r=1$ are excluded by the guard, uniformity with $r\ge 2$ makes edges nonempty, and for an edgeless hypergraph both sides are $0$. 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: the basic inequalities $\nu\le\tau\le r\nu$, finiteness of the edge set, Kőnig's theorem in this formulation, and decompositions of Aharoni's theorem.

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 8).
• R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica 21 (2001), 1–4. https://doi.org/10.1007/s004930170001
• Z. Tuza, Ryser's conjecture on transversals of r-partite hypergraphs, Ars Combin. 16 (1983), 201–209.
• P. E. Haxell, A. D. Scott, On Ryser's conjecture, Electron. J. Combin. 19 (2012), P23. https://doi.org/10.37236/1175
• A. Abu-Khazneh, J. Barát, A. Pokrovskiy, T. Szabó, A family of extremal hypergraphs for Ryser's conjecture, J. Combin. Theory Ser. A 161 (2019), 164–177. https://doi.org/10.1016/j.jcta.2018.07.011
• A. Bishnoi, S. Das, P. Morris, T. Szabó, Ryser's conjecture for t-intersecting hypergraphs, J. Combin. Theory Ser. A 179 (2021), 105366. https://doi.org/10.1016/j.jcta.2020.105366
• N. Francetić, S. Herke, B. D. McKay, I. M. Wanless, On Ryser's conjecture for linear intersecting multipartite hypergraphs, European J. Combin. 61 (2017), 91–105. https://doi.org/10.1016/j.ejc.2016.10.004
• Z. Füredi, Maximum degree and fractional matchings in uniform hypergraphs, Combinatorica 1 (1981), 155–162. https://doi.org/10.1007/BF02579271

Motivation

A matroid records which subsets of a finite set are independent, in the way that sets of columns of a matrix are linearly independent or sets of edges of a graph are acyclic. The matroids that come from matrices over a field $\mathbb F$ are the $\mathbb F$-representable matroids, and deciding which matroids are representable over a given finite field is one of the oldest structural questions of the subject. The class of $\mathrm{GF}(q)$-representable matroids is closed under deletion and contraction, so it is determined by its excluded minors, the minor-minimal matroids outside the class. Listing them is the matroid analogue of Kuratowski's and Wagner's theorems for planar graphs.

Timeline.

• 1958 — Tutte proves that a matroid is binary, i.e. $\mathrm{GF}(2)$-representable, if and only if it has no minor isomorphic to $U_{2,4}$: there is exactly one excluded minor (Tutte 1958).
• 1971 — Rota conjectures that for every finite field the list of excluded minors is finite (Rota 1971).
• 1979 — Bixby and Seymour independently prove that the excluded minors for $\mathrm{GF}(3)$ are $U_{2,5}$, $U_{3,5}$, $F_7$ and $F_7^*$ (Bixby 1979, Seymour 1979).
• 2000 — Geelen, Gerards and Kapoor determine the seven excluded minors for $\mathrm{GF}(4)$ (Geelen–Gerards–Kapoor 2000).
• 2008 — Mayhew and Royle enumerate the matroids on at most nine elements and find hundreds of excluded minors for $\mathrm{GF}(5)$ among them; the complete list for $\mathrm{GF}(5)$ is unknown (Mayhew–Royle 2008).
• 2014 — Geelen, Gerards and Whittle announce a proof of Rota's conjecture built on their matroid minors structure theory. The argument gives no explicit bound on the number of excluded minors, and the full write-up has not appeared (Geelen–Gerards–Whittle 2014).

Setting

A matroid $M$ on a finite ground set $E$ is given by a family $\mathcal I$ of subsets of $E$, the independent sets, such that $\emptyset\in\mathcal I$, every subset of an independent set is independent, and whenever $I,J\in\mathcal I$ with $|I|<|J|$ there is some $x\in J\setminus I$ with $I\cup\{x\}\in\mathcal I$. The maximal independent sets are the bases.

Let $p$ be a prime, $m\ge 1$ an integer, and $\mathrm{GF}(p^m)$ the field with $p^m$ elements. $M$ is $\mathrm{GF}(p^m)$-representable if there are a vector space $W$ over $\mathrm{GF}(p^m)$ and a map $v\colon E\to W$ such that a set $I\subseteq E$ is independent in $M$ exactly when the family $(v(x))_{x\in I}$ is linearly independent.

The deletion $M\backslash D$ has ground set $E\setminus D$ and the independent sets of $M$ contained in $E\setminus D$. The dual $M^*$ has the same ground set, and a set is independent in $M^*$ when its complement contains a base of $M$. The contraction is $M/C := (M^*\backslash C)^*$. A minor of $M$ is a matroid $M/C\backslash D$ with $C,D\subseteq E$ disjoint; it is proper if it differs from $M$. For a class $\mathcal C$ of matroids closed under minors, an excluded minor for $\mathcal C$ is a matroid outside $\mathcal C$ all of whose proper minors lie in $\mathcal C$. Write $\mathrm{EX}(q)$ for the set of excluded minors for $\mathrm{GF}(q)$-representability, counted up to isomorphism.

The challenge is scaled by two natural numbers. For $r,B\in\mathbb N$ let $S(r,B)$ be the statement

$$\text{for every prime power } p^m\le r:\quad |\mathrm{EX}(p^m)|\le B .$$

$S(r,B)$ implies $S(r',B')$ whenever $r'\le r$ and $B'\ge B$; a contestant chooses $r$ and $B$ and proves $S(r,B)$.

Formalization targets

Goal

$$\forall r\in\mathbb N\ \ \exists B\in\mathbb N:\quad S(r,B).$$

This is Rota's conjecture: every finite field has only finitely many excluded minors up to isomorphism. It asserts only the shape of the truth, an unspecified finite bound for each field, and so remains the goal whatever explicit bounds are proved.

Rungs

$$S(2,1),\qquad S(3,4),\qquad S(4,7).$$

These are Tutte's theorem, the Bixby–Seymour theorem and the Geelen–Gerards–Kapoor theorem. An explicit bound $B$ with $S(5,B)$ is the first open rung.

Significance

Excluded-minor characterisations are the standard route to recognition algorithms and to the structure theory of a class; for $\mathrm{GF}(2)$, $\mathrm{GF}(3)$ and $\mathrm{GF}(4)$ they underlie the theory of regular, ternary and quaternary matroids. The lists are complete for exactly these three fields. Rota's conjecture settles finiteness in general, but its announced proof gives no bound: an explicit $B$ for $\mathrm{GF}(5)$ would be the first quantitative information on the size of $\mathrm{EX}(5)$ beyond lower bounds from computer search.

Formalizing the rungs produces the representability theory that Mathlib lacks: matrix representations and their duals, uniform matroids, the Fano plane and its relatives, and the minor-closure of representable classes. None of the three theorems has a machine-checked proof; Tutte's theorem alone is a substantial project, and the $\mathrm{GF}(4)$ case is a long paper. The goal itself is proved in the literature only in announced form and is not formalized anywhere.

Difficulty

The obvious attack, enumerating small matroids and testing representability, cannot work: nothing bounds the size of an excluded minor in advance, and bounding it is precisely the content of the problem. Tutte's theorem requires showing that a non-binary matroid can be reduced by deletions and contractions to $U_{2,4}$, which needs either his homotopy theorem or one of the later shorter arguments; the $\mathrm{GF}(3)$ and $\mathrm{GF}(4)$ cases rest on connectivity and splitter-type reductions that are far longer. Counting excluded minors up to isomorphism also forces one to compare matroids on different ground sets.

Formalization scope

Matroids are Mathlib's Matroid α, with ground set M.E : Set α and independence predicate M.Indep; finiteness is M.Finite. Representability is the predicate IsGFRepresentable p m M: there exist a type W with an additive group structure, a module structure over GaloisField p m, and a map v : α → W such that M.Indep I ↔ LinearIndepOn (GaloisField p m) v I for every set I. Because non-independent sets include every set containing an element outside the ground set, a representation sends such elements to $0$. Minors are Mathlib's strict minor order N <m M; IsExcludedMinorFor P M says that $M$ fails $P$ while every strict minor satisfies $P$. Isomorphism is the explicit Matroid.IsIso: a bijection between the ground sets, as subtypes, carrying independent sets exactly to independent sets. ExcludedMinorsAtMost p m B says that some finite set $S$ of at most $B$ matroids on the ground type $\mathbb N$ contains, up to isomorphism, every finite excluded minor for $\mathrm{GF}(p^m)$-representability on any ground type in Type. The rung statement_02 r B quantifies over all primes $p$ and all $m\ge 1$ with $p^m\le r$; it is vacuous for $r\le 1$, and the goal is ∀ r, ∃ B, statement_02 r B.

There is no trivialising reading: $B=0$ is impossible for $r\ge 2$ since $U_{2,4}$ is not binary, and the representatives in $S$ are unconstrained, so the statement is exactly a bound on the number of isomorphism classes. The Lean definitions are copied verbatim from the Ten Challenges repository, so that a proof accepted here is a proof of the benchmark statement. 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: an API for matrix representations and duality, the standard small matroids ($U_{2,4}$, $U_{2,5}$, $U_{3,5}$, $F_7$, $F_7^*$) and their non-representability, minor-closure of representable classes, decompositions of the rungs.

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 2).
• W. T. Tutte, A homotopy theorem for matroids, I, II, Trans. Amer. Math. Soc. 88 (1958), 144–174. https://doi.org/10.1090/S0002-9947-1958-0101526-0
• R. E. Bixby, On Reid's characterization of the ternary matroids, J. Combin. Theory Ser. B 26 (1979), 174–204. https://doi.org/10.1016/0095-8956(79)90056-X
• P. D. Seymour, Matroid representation over GF(3), J. Combin. Theory Ser. B 26 (1979), 159–173. https://doi.org/10.1016/0095-8956(79)90055-8
• J. F. Geelen, A. M. H. Gerards, A. Kapoor, The excluded minors for GF(4)-representable matroids, J. Combin. Theory Ser. B 79 (2000), 247–299. https://doi.org/10.1006/jctb.2000.1963
• G.-C. Rota, Combinatorial theory, old and new, Actes du Congrès International des Mathématiciens (Nice, 1970), vol. 3, Gauthier-Villars, 1971, 229–233. https://www.mathunion.org/icm/proceedings
• J. Geelen, B. Gerards, G. Whittle, Solving Rota's conjecture, Notices Amer. Math. Soc. 61 (2014), 736–743. https://doi.org/10.1090/noti1139
• D. Mayhew, G. F. Royle, Matroids with nine elements, J. Combin. Theory Ser. B 98 (2008), 415–431. https://doi.org/10.1016/j.jctb.2007.07.005
• J. Oxley, Matroid Theory, 2nd edition, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001

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