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