OpenAI and the finite lattice representation problem

On 6 October 2026 OpenAI published a collection of 722 mathematical manuscripts written by an unreleased internal model. Two of them claim a negative answer to the finite lattice representation problem (FLRP), which asks whether every finite lattice is the congruence lattice of a finite algebra. This post explains what the main paper proves and how, which parts of it a careful reading could check, where the risk sits, what the proof assumes, and how much of it is already formalized in Lean. The short version: in an AI-assisted reading the lattice-theoretic half holds up; the whole weight rests on one unverified theorem about finite groups; the proof builds an explicit family of candidate lattices but certifies none, because a parameter it needs is never bounded; and more of it is formalized than OpenAI's own documentation says, though not the part that matters.

How this post was written

I prepared this post with Claude (Anthropic) as a reading assistant, within a day of the release. Claude Fable 5.1 read the main paper in full and about forty pages of the companion, and checked Sections 2, 8, 9 and 10 of the main paper line by line. Claude Opus 5.5 surveyed OpenAI's Lean library file by file, checked one claim in GAP, and drafted this text and its diagrams. The line-by-line checks reported here are the model's. Where this post calls a part of the proof checked, it means that reading: it is not a referee's verification, and as far as I know no one outside OpenAI has yet checked the group theory of Sections 3 to 7.

The post is written in layers: a one-minute summary, a five-minute overview of the proof, answers to the questions a reader will ask, the assumptions, the mathematics in detail, the state of the formalization, and the companion paper's undecidability claim. Stop wherever you have what you need.

The one-minute version

OpenAI's collection holds 722 manuscripts, and two of them attack the FLRP. The 87-page paper proves, if it is right, that some finite lattice is not an interval in the subgroup lattice of any finite group, and it deduces the FLRP answer from the Pálfy–Pudlák equivalence. In an AI-assisted reading, its lattice-theoretic half (how the lattice is built, how the pieces are glued, and the final contradiction) checks out line by line. Its weight rests on one theorem about finite groups, a uniform bound on the length of certain subgroup chains, proved over fifty pages with the classification of finite simple groups and repeated Ramsey arguments, and that theorem is unverified. The proof is classical at its core: it builds an explicit family of lattices, but the length that makes a member a counterexample is proved to exist and never bounded. OpenAI's Lean library formalizes a few of the paper's lemmas and some estimates used inside the proof of its main theorem, but not the theorem itself.

In one line each, the verdicts are as follows:

• The elementary half survives a careful reading. In an AI-assisted reading, Sections 2, 8, 9 and 10 are correct, given Schreier's theorem.
• The group-theoretic core is unverified. Theorem 3.2, proved in Sections 3 to 7, needs expert refereeing.
• The counterexample is explicit up to one unknown number. The paper builds an explicit family of lattices \(L_N\), and every member with \(N \ge B\) is no subgroup interval; \(B\) is proved to exist and never bounded.
• The formalization is partial. OpenAI's Lean library holds the fence test of Section 2, four of the gluing lemmas of Section 10, some estimates used inside the proof of Theorem 3.2, and the companion's graph criterion; not Theorem 3.2 itself.
• The companion goes further. It claims that representability is undecidable and specifies a "minimum" counterexample through a Busy Beaver constant. Its logic is sound; the structural mathematics behind it was not part of this reading.

The two papers and the shape of the proof

The two manuscripts belong to one "family" of OpenAI's collection, and they take different routes to the same negative answer.

	A negative solution to the FLRP	Finite congruence lattices: characterization and undecidability
Length	87 pages	180 pages
Main claim	A finite lattice that is no subgroup interval of a finite group (Theorem 1.2), hence a finite lattice that is no congruence lattice of a finite algebra (Theorem 1.1)	Representability is undecidable; so is recognizing subgroup intervals; a nonrepresentable family is built directly; a minimum nonrepresentable lattice is "specified"
Route to algebras	The global Pálfy–Pudlák equivalence of two universal statements	Pointwise: a least-carrier reduction, then a diagonal construction in a semidirect power represents the dual lattice as a group interval
Counterexample	An explicit family \(L_N\); every \(N \ge B\) gives a lattice that is no subgroup interval, with \(B\) never bounded	One member of an explicit family, with parameters chosen to give fewer than \(M^*\) elements; and a minimum lattice defined through a Busy Beaver constant
Checkable claims	Sections 2, 8, 9 and 10: checked in this reading	Its representation of L7 is right, by a GAP computation; its graph criterion is standard
In Lean	Definition 2.1, Lemma 2.2, Lemmas 10.1, 10.2, 10.5 and 10.7, and degree bounds used in Proposition 4.1; not Theorem 3.2 itself	The graph criterion, with a comparator challenge; the fixed-size witness test; the coset correspondence
This reading covered	All of it	Sections 1 to 4.4, 15 and 17, about forty pages

How the negative solution is assembled

The proof in one column. Everything except the dashed box is finite lattice theory and elementary group theory, and this reading checked it. The dashed box is a uniform statement about all finite groups whose proof uses the classification of finite simple groups.

Four ideas you need to follow it

Fences. An interval \([a, b]\) is fenced when every interior element \(c\) has two comparable complements \(u < v\): both meet \(c\) at \(a\) and join it to \(b\). In a subgroup interval \([D, X]\), a fence forces every normal subgroup of \(X\) either into \(D\) or to supplement it, by one application of Dedekind's law. From that, \(X\) modulo the core of \(D\) has a unique minimal normal subgroup, a direct power of a nonabelian simple group \(T_X\), which the paper calls the label of \(X\). This is Pálfy's strongly non-modular argument, and the paper cites my 2012 note on interval enforceable properties for the general viewpoint that lattice shapes can force group structure.

Labels move predictably. A section of a group is a quotient of one of its subgroups. For labeled \(X < Y\) over the same bottom, either the labels agree, and \(X\) meets the socle \(T_Y^m\) of \(Y\) in a subdirect product of diagonal strips, or \(T_X\) is a proper section of \(T_Y\), and \(X\) meets the socle in a product of proper subgroups, one in each coordinate. In the second case, the vertices of \([X, Y]\) that also meet the socle in such a product form a sublattice, and one coordinate carries that sublattice onto an honest interval in an almost simple group with socle \(T_Y\), with covers going to covers. So a strict change of label at a cover is a maximal subgroup of an almost simple group.

Tested chains. A tested chain is a chain \(a = x_0 < x_1 < \cdots < x_N = b\) in which every pair \(x_i < x_j\) is joined by a two-cover path through a private middle vertex, with fences on all the pairs, coatom conditions, and an \(M_{16}\) hanging under every upper vertex. Theorem 3.2 says that past an absolute length \(B\) the two ends carry the same label. The intuition: in the almost simple projection, the bottom of the chain is second maximal in every vertex above it at once, while the labels strictly grow. The classification allows only a few ways to be second maximal, each of which moves a numerical invariant (field degree, dimension, rank) in a direction that two-step routes between all pairs cannot sustain.

The simplest case shows the mechanism. Suppose every label is a group of Lie type of one fixed type, \(T_i\) defined over the field with \(p^{f_i}\) elements. Then a strict cover between labels is a subfield step, which multiplies the field exponent by a prime (Lemma 3.11), so a two-step shortcut from \(x_i\) to \(x_j\) makes \(f_j / f_i\) a product of at most two primes. Four vertices are impossible: \(f_4 / f_1 = (f_4 / f_3)(f_3 / f_2)(f_2 / f_1)\) has at least three prime factors, while the shortcut from \(x_1\) to \(x_4\) allows at most two. Theorem 3.2 runs a count of this kind for every way one label can sit inside a larger one, using Ramsey arguments to make the counts uniform.

Gluing on a Boolean lattice. Suppose \([D, G]\) represents the lattice with \(|G|\) as small as possible. The global fence then gives \(G = DS\), where \(S = T^m\) is the unique minimal normal subgroup, \(D \cap S = 1\), and \(D\) permutes the \(m\) simple factors of \(S\) transitively. Let \(A\) be the stabilizer in \(D\) of one factor, and \(\alpha \colon A \to \operatorname{Aut}(T)\) its action on that factor. The forward chains make every proper vertex \(Y\) of a copy of \(B_4\) meet \(S\) subdirectly, and Pálfy's dictionary for subgroups of twisted wreath products describes the whole filter above such a \(Y\) by a pair \((U, \beta)\): a subgroup \(A \le U \le D\) and a homomorphism \(\beta \colon U \to \operatorname{Aut}(T)\) extending \(\alpha\). Smaller vertices give larger domains, and Boolean meets become unions of index sets. For a family of faces whose union is the whole four-element set, the forward groups meet in \(D\), which meets \(S\) trivially; so the homomorphisms attached to those faces cannot all be restrictions of one homomorphism on the subgroup their domains generate. Section 10 shows that they must be.

Who can check what

The work divides by expertise.

• A lattice theorist, in a day or two: Section 8, the construction and its persistence lemmas, and the lattice parts of Section 2.
• A finite group theorist, in a week: Sections 2, 9 and 10, which use Dedekind's law, subdirect products of simple groups, cores, and Schreier's theorem.
• A specialist in maximal subgroups of classical groups and modular representations of algebraic groups, in months: Sections 3 to 7.

Questions a reader will ask

How constructive is the proof?

It is non-constructive at one essential point, and the rest could be made explicit.

• The bound is proved to exist by contradiction. The proof of Theorem 3.2 assumes tested chains of unbounded length with different end labels, extracts uniform structure by Ramsey arguments, and reaches an impossibility. No estimate of \(B\) is given or attempted. The authors say so: "An explicit numerical value of that parameter is unnecessary for the existence conclusion."
• The family is explicit. For each \(N\) the lattice \(L_N\) is a finite lattice built by explicit steps, and Lemma 8.5 bounds each of its components by \(9(q_0 + 27hN^2)\) elements. What is missing is a value of \(N\) known to be large enough.
• The transfer to algebras could name a lattice; the paper does not. The Pálfy–Pudlák theorem is a global equivalence between two universal statements: it does not say that a given congruence lattice is a subgroup interval, and the paper uses it only in that global form, so it names no lattice that fails to be a congruence lattice. The proof of the direction it needs is explicit, though. Lemma 2 of Pálfy and Pudlák places any finite lattice \(L\) as the top interval of a lattice \(L'\) with \(5|L| + 1\) elements, and the proof of their Theorem 2 shows that if \(L'\) is a congruence lattice, then \(L\) is an interval in the subgroup lattice of a finite group. So for every \(N \ge B\) the lattice \(L'_N\) built from \(L_N\) is not a congruence lattice, and the only missing datum is \(B\).
• The classification of finite simple groups is used throughout. It enters through Schreier's theorem, Aschbacher's theorem, and the maximal-subgroup literature; the section on assumptions below lists every channel. No choice principle is needed, since every object is finite or countable.
• The main theorem is not formalized. OpenAI's Lean library formalizes a handful of the paper's lemmas and some estimates used inside the proof of Theorem 3.2, described below, but not the theorem itself.

What undecidability would and would not change

If the companion is right and representability is undecidable, then the lattices that are not congruence lattices do not even form a semidecidable set, so no algorithm can find and certify counterexamples by search; each one needs a proof of its own. That would not stop anyone from bounding \(B\) in this paper by a sharper analysis of Theorem 3.2, and the companion claims an explicit counterexample of its own.

Does either paper name a counterexample?

To name a counterexample is to give a specific finite lattice together with a proof that it is not a congruence lattice. The negative-solution paper comes within one number of doing so: any \(L'_N\) with \(N \ge B\) would do, and no value of \(B\) is known. The companion makes two claims of its own.

• One explicit member. Its Section 16 fixes the parameters of one member of its family of affine test lattices by explicit computable choices, so that the member is nonrepresentable and has fewer than \(M^*\) elements, where \(M^* = x_5\), \(x_0 = 10^9\), and \(x_{j+1} = J^{x_j}(x_j)\) for a fast-growing function \(J\). If its unread Sections 5 to 14 are right, that does name a counterexample, one that is computable in principle and far too large to write down.
• A minimum lattice by Busy Beaver. Its Section 17 defines a nonrepresentable lattice \(L_0\) of minimum cardinality as the first order table, by size and then lexicographically, up to \(M^*\), that has no colored-graph witness smaller than \(\mathcal{B}\), where \(\mathcal{B}\) is the largest output of any terminating register program of a fixed size. That is a definite integer and a definite lattice. A program that prints the integer certainly exists, but there is no way to tell which program it is, since the Busy Beaver function outgrows every computable function. The authors are candid about it: no evaluated cardinality and no diagram.

Were the pieces glued together correctly?

When several lattices are combined to enforce several properties at once, the danger is that one gadget spoils another's covers, fences or meets, or that the properties stop holding in the combined lattice. The paper handles this carefully, and in this reading every mechanism held up.

• Private insertion. Every gadget (a chain, a shortcut vertex, a fence, an \(M_{16}\), a pair of coatom witnesses) is inserted into an interval \([a, b]\) so that a fresh vertex compares with an old one only through \(a\) and \(b\): an old \(x\) lies below a fresh \(w\) exactly when \(x \le a\), and a fresh \(w\) lies below an old \(y\) exactly when \(b \le y\). Lemma 8.2 proves that this yields a lattice, preserves all old meets and joins, and destroys an old cover \(c \prec d\) only when the insertion's endpoints are exactly \(c\) and \(d\).
• Persistence. A fence is witnessed by two comparability components in the proper part of its interval, and private insertions never merge components (Lemma 8.3). Covers, coatom representations and exact \(M_{16}\) intervals survive because later insertions never use their endpoints (Lemmas 8.4 and 8.5).
• Two kinds of test that cannot touch. A fresh vertex of a forward test lies below no proper original vertex; a fresh vertex of a reverse test lies inside a proper original interval. This separation keeps the forward and reverse gadgets apart, and it is proved by induction on the insertions.
• The final batch. After all the shape gadgets are in, fences are added below every vertex of a forward comparison interval and above every vertex of a reverse one, over a frozen vertex set. Lemma 8.5 proves that no further round is needed: the only vertices without a fence from the bottom are the fresh interior vertices of these last fences, and each has a labeled bottleneck below it that is comparable with everything beneath it. That is condition T5 of Definition 3.1, and Corollary 2.4 shows that the bottleneck gives the same normal-subgroup consequences a fence would.
• The horizontal sum. The decorated Boolean lattice, the detector and their duals are summed by identifying only \(0\) and \(1\). Interiors of different components are incomparable, so cross meets are \(0\) and cross joins are \(1\). This threatens no test, and it supplies the fence on \([0, 1]\) itself.
• The semantic gluing. The reverse tests are read not in \([D, G]\) but in the group intervals \([A, U_v]\) produced by the extension dictionary. That is legitimate because every subgroup above a subdirect subgroup is subdirect, so the dictionary is an isomorphism of the entire filter above \(Y_v\), not just of its labeled vertices. The paper flags the point itself: "no representation of the entire dual lattice is assumed."

What is new, and what was already known?

The ingredients are known. The paper uses Pálfy's strongly non-modular argument and his dictionary for subgroups of twisted wreath products, Aschbacher's choice of a representation minimal over both orientations, the reduction of a strict label change to a maximal subgroup of an almost simple group in the spirit of Baddeley and Lucchini, the bound of Burness, Liebeck and Shalev on second maximal subgroups, and Basile's bound for alternating and symmetric groups. The companion's bridge from algebras to groups is classical as well: Pálfy and Pudlák's least-carrier lemma, the observation that simplicity of the lattice forces every nonunit unary polynomial to be constant, Kurzweil's diagonal construction representing the dual of an invariant-equivalence lattice as an interval, and Pálfy and Pudlák's count of complements, which is always a prime power, played against diamonds \(M_q\) with \(q - 1\) not a prime power.

What is new is a change of target. Work on the problem has mostly aimed at small lattices, where the group theory needed is a finite but open-ended classification problem; the reductions of Baddeley and Lucchini and of Aschbacher push a hypothetical representation toward almost simple groups and then face a case analysis. This proof trades a small lattice for an enormous one with a free length parameter, so that the group theory becomes a uniform asymptotic statement, chain rigidity, and Ramsey arguments do the work that case analysis cannot do for a fixed small lattice.

The lattice-theoretic half could have been found with tools that have been in the literature for decades. Theorem 3.2 is another matter. It needs working command of Aschbacher's classes, Liebeck and Seitz on classical subgroups, Larsen and Pink's theorem on finite subgroups of algebraic groups, Lübeck's tables of small modules, Steinberg's tensor product and restriction theorems, and Seitz's classification of irreducible triples with its later corrections, plus the stamina to carry Ramsey thinning across fifty pages of case distinctions. That is a job for specialists in the subgroup structure of classical groups.

How was it produced?

The public record says this much.

• The repository's README is the primary source. An unreleased internal OpenAI model produced the 722 manuscripts, grouped into 372 families. Each result used about three hours of "ChatGPT Pro thinking compute" on average, out of roughly 4,000 problems posed, and there was no human editing except in two noted cases. The README adds: "Some of the unformalized results could have issues."
• The paper's texture is distinctive. It has no acknowledgments, its citations carry page locators into author versions and specific arXiv versions, and it contains dozens of sentences that disclaim an assertion, such as "No assertion that this is the entire projected socle is required." Each of those marks a point where the argument deliberately claims less than a reader might assume, and a referee should read them first.
• The companion's L7 witness was already public. My 2012 thesis left one lattice with at most seven elements, L7, without a known representation. The companion represents it as the interval \([\mathrm{PGL}_2(2), \mathrm{PGL}_2(64)]\), with intermediate groups \(D_{18}\), \(D_{42}\), \(A_5\), \(D_{126}\) and \(\mathrm{PSL}(2, 8)\); in characteristic two, \(\mathrm{PGL}_2(q) = \mathrm{PSL}_2(q) = \mathrm{SL}_2(q)\). A GAP computation confirms it in about twenty seconds: those five intermediate groups, with nine covering pairs, form L7. The same representation appears in Chenxiao Tian's note posted on ResearchGate on 28 August 2026, which the companion does not cite. Whether the model found it or read it cannot be told from the text; the companion's proof is an elementary counting argument, different in style from Tian's.
• The method itself is instructive. It works at scale, uses the classification as a black box, trades explicitness for uniformity, and formalizes the combinatorial pieces that can be formalized.

What the proof assumes

How classical is the result, and how strong? The answer comes in three layers, the logic, the foundations and scope, and the external theorems, followed by a verdict.

Logic

• Classical logic is essential at one point. Theorem 3.2 asserts that a bound \(B\) exists, and its proof shows only that the assumption "for every \(B\) there is a longer chain whose end labels differ" is contradictory. Passing from that to an actual \(B\) is not intuitionistically valid, and nothing in the paper supplies one.
• A second classical step is optional. The paper deduces "not every finite lattice is a congruence lattice" from the global Pálfy–Pudlák equivalence, which is intuitionistically fine, and then passes to "some finite lattice is not one", which is classical. Pálfy and Pudlák's explicit extension, described above, avoids that step: for \(N \ge B\), \(L'_N\) is a specific lattice that is not a congruence lattice.
• Everywhere else the case distinctions are on decidable properties of finite groups. They are harmless for a constructive reading. The finite Ramsey theorems, Chevalley–Warning and the lattice arguments of Sections 8 to 10 are finitary and elementary.
• The result is a \(\Sigma^0_2\) sentence of arithmetic. "Some finite lattice is the congruence lattice of no finite algebra" says that there is a finite lattice such that, for every finite algebra, a decidable test fails. The paper proves its classically equivalent form \(\neg\forall L\,\exists A\), and a classical proof of a \(\Sigma^0_2\) sentence need not carry a witness. Here the witness would be \(L'_N\) for any \(N \ge B\), so the only missing datum is \(B\).

Foundations and scope

• No set theory beyond the ordinary. Every object is finite except the algebraic groups of Sections 3 to 7, which live over algebraic closures of finite fields, countable fields that exist without choice. No choice principle, large cardinal or nonstandard model is used. The proof is plausibly formalizable in second-order arithmetic with the imported theorems as axioms, and those theorems are ordinary classical mathematics.
• No conjecture. The proof assumes no unproved statement. The one conditional statement nearby, Burness, Liebeck and Shalev's bound on the number of generators of a second maximal subgroup, is not the one used; their bound on chief factors, which the paper uses, is unconditional. No computer calculation enters, apart from Lübeck's published tables.
• What the theorem quantifies over. A finite algebra is a nonempty finite set with finitely many total operations of finite arity; nullary operations and the empty signature are allowed, and the signature may depend on the lattice. The paper notes that infinitely many operations would add no finite representations. The congruence lattice is the full one. On the group side, intervals are full intervals \([D, G]\) in finite groups, with no restriction on \(D\). The constructed lattice is finite, nonempty and self-dual.
• What is not claimed. There is no bound on the size of the lattice, on the order of a hypothetical representing group, or on the carrier of a representing algebra; no named counterexample; and no statement about any restricted class of algebras.

Where the classification of finite simple groups enters

The dependence is not incidental. There are four separate routes, and a proof avoiding the classification would have to replace each of the following:

1. Schreier's theorem, that \(\operatorname{Out}(T)\) is solvable for every finite simple \(T\), used in Proposition 2.9, Lemma 3.8, Proposition 3.13, Lemma 9.2 and Lemma 10.3, and inside the lemma of Pálfy that Proposition 9.5 uses.
2. The trichotomy that every nonabelian finite simple group is alternating, of Lie type, or one of finitely many sporadic groups, used in Proposition 3.13 to discard the sporadic groups.
3. Burness, Liebeck and Shalev's bound of five nonabelian chief factors for a second maximal subgroup of an almost simple group, whose proof runs through the known maximal subgroups.
4. Basile's bound on height-two intervals in alternating and symmetric groups, which rests on the Liebeck–Praeger–Saxl classification of their maximal subgroups; in the same spirit, the descriptions of Aschbacher's class \(\mathcal{S}\) in Kleidman and Liebeck.

Larsen–Pink, Steinberg, Seitz, Lübeck, Landazuri–Seitz and the cohomological inputs do not depend on the classification.

The dependency stack. The elementary left branch needs the classification only through Schreier's theorem. The right branch needs it through the maximal-subgroup literature and the trichotomy, and it also imports the representation theory of algebraic groups in positive characteristic.

Every imported theorem

The table collects each citation in the text with the lemma it supports. The column headed "Classification" says whether the imported result itself depends on the classification of finite simple groups. "Checked" in the last column means only that the citation exists and is used for the stated purpose, unless it says more.

Result	Used in	For	Classification	Status of this reading
Classification of finite simple groups	Proposition 3.13, and wherever Schreier's theorem is used	large simple groups are alternating or of Lie type	itself	assumed; the first-generation proof runs to some ten thousand pages
Schreier's theorem	Proposition 2.9, Lemma 3.8, Proposition 3.13, Lemmas 9.2 and 10.3	\(\operatorname{Out}(T)\) is solvable	yes	standard
Pálfy–Pudlák 1980, Theorem 2	Theorem 1.1	the transfer between the two universal statements	no	standard and elementary
Pálfy 2019, Lemmas 2.1, 2.11, 2.12, 2.13, 3.6, Proposition 2.2, Lemma 2.3	Sections 2 and 9	subdirect products of simple groups; the twisted wreath dictionary; the strongly non-modular test; subgroups of \(\operatorname{Aut}(T)\) not containing \(\operatorname{Inn}(T)\)	Lemma 2.11 through Schreier	mostly reproved in the paper; checked
Aschbacher 1984; Kleidman–Liebeck 1990	Propositions 3.3, 3.4 and 4.1	a maximal subgroup of a classical group lies in one of eight geometric classes or is almost simple and irreducible	the statement no; the details of class \(\mathcal{S}\) yes	not checked clause by clause
O'Nan–Scott, in maximal-subgroup form	Propositions 3.3 and 3.4	maximal subgroups of \(A_n\) and \(S_n\): intransitive, imprimitive, affine, diagonal, product action, almost simple	the statement no; maximality yes	not checked
Larsen–Pink 2011	Proposition 3.3, Lemmas 3.10 and 3.11	a finite subgroup of an algebraic group is a subfield group or lies in a bounded envelope	no	not checked
Burness–Liebeck–Shalev 2017, Proposition 8.1	Proposition 3.3, Lemma 3.7	a second maximal subgroup has at most five nonabelian chief factors	yes	the bound confirmed from the published abstract
Basile 2001, Theorem D	Proposition 3.3, Lemma 3.9	a height-two interval in \(A_n\) or \(S_n\) has at most eleven interior points	yes	consistent with the thesis abstract
Landazuri–Seitz 1974; Häsä 2014	Propositions 3.3 and 4.1	lower bounds on cross-characteristic projective degrees	no	not checked
Steinberg 1963, 1967, 1981	Proposition 3.3, Lemmas 5.3, 5.4 and 6.6, Propositions 5.5, 5.8 and 7.4	the tensor product theorem; restriction to finite groups; automorphisms; universal central covers uniformly in the field	no	standard
Lübeck 2001	Proposition 4.1	every nonnatural restricted module in rank above 11 has dimension at least \(r^2/2\)	no	not checked
Liebeck–Seitz 1998	Lemma 4.3, Proposition 5.8	tensor and twisted-tensor subgroups and their fixed points	mostly no	not checked
Bray–Holt–Roney-Dougal 2013	Proposition 4.1	normalizers of symplectic-type subgroups	partly	not checked
Seitz 1987; Cavallin–Testerman 2019; Burness–Testerman 2019	Lemmas 7.1 and 7.2	the classification of irreducible triples	no	the table's rows not checked
Jantzen 2003	Lemma 5.4	simple, costandard and Weyl modules	no	standard
Conrad 2014	Lemmas 3.11 and 5.7, Proposition 5.8	the isogeny theorem; vector stabilizers in characteristic two; lifting through central isogenies	no	not checked
Dowd–Sin 1996	Proposition 5.8, Lemma 6.6, Section 7	the special isogenies between types B and C in characteristic two	no	not checked
Bendel–Nakano–Parshall–Pillen–Scott–Stewart 2015; Bendel–Nakano–Pillen 2004; Cline–Parshall–Scott–van der Kallen 1977; Garibaldi–Nakano 2016	Lemma 5.4, Proposition 5.5	injectivity of restriction in cohomology; first cohomology of the first Frobenius kernel; quadratic refinements of invariant forms	no	not checked
Chevalley 1935; Warning 1935	Lemma 4.10	a nonzero common zero of few low-degree equations, giving an invariant totally singular subspace	no	standard
Taylor 1992	Lemma 5.7	Witt's extension theorem; the Dickson invariant	no	standard
The finite Ramsey theorem	Proposition 3.13, Lemmas 4.5 and 4.14, Proposition 7.4, the end of Section 7	homogeneous subchains for colorings of pairs and triples	no	standard

Some citations carry no logical weight: Aschbacher 2008, whose dual-minimality argument the paper reproves, and Baddeley–Lucchini, Baddeley, Börner, Grätzer–Schmidt, McNulty, Pudlák–Tůma, Repnitskiĭ–Tůma, Schaffer and my 2012 note, which are context.

Standard facts used without citation

These are asserted as known. Each is standard, and a referee would still want them named:

• Dedekind's modular law for subgroups, which the paper calls the subgroup modular identity.
• Schur's lemma, and a matrix form of Hilbert's Theorem 90 used to descend representations to minimal fields.
• The Lang–Steinberg theorem, and the description of the automorphisms of groups of Lie type as inner-diagonal, field and graph automorphisms.
• \(\operatorname{Aut}(A_n) = S_n\) for \(n \ge 7\), and the order formulas for the classical groups.
• That a characteristically simple finite group is a direct power of a simple group, and that the invariant subgroups of an abelian group form a modular lattice.
• The surjectivity of norms of finite fields, Steinberg's root presentations, and the structure of perfect central extensions.

The companion's additional imports

From the parts read here: the companion lists its inputs in its Section 4.1. They are the classification, Schreier's theorem, the classification of finite two-transitive groups, Lang–Steinberg, highest-weight theory, Steinberg's theorems, the algebraic Peter–Weyl filtration, Larsen–Pink, Jordan's prime-cycle theorem, Bochert's bound on the index of primitive groups, Burnside's theorem on groups of prime degree, the fact that a six-transitive group of large degree contains the alternating group, the finite Ramsey, Hales–Jewett and vector-space Ramsey theorems, Maróti's bound on the orders of primitive groups, Dickson's lemma, and the Davis–Putnam–Robinson–Matiyasevich theorem (DPRM).

Verdict on the assumptions

How classical: classical at one essential point, the existence of \(B\), and finitary everywhere else. It needs no axiom beyond ordinary mathematics, no choice and no conjecture, and its conclusion is an arithmetical \(\Sigma^0_2\) sentence whose witness is explicit except for \(B\). How strong: a little more than the negative answer. The lattice is self-dual and belongs to an explicit family, and the paper notes that it is not the lattice of intermediate fields of any finite separable field extension either. But there is no bound on \(B\), so no counterexample is certified, and the proof depends on the classification of finite simple groups through four separate channels; a proof that avoided the classification would be a different proof.

The mathematics in more detail

This section gives the definitions with pictures, then the structure of the fifty-page proof of Theorem 3.2, reduction by reduction, and then the construction and the gluing.

A fence is a pentagon at every interior element

Fenced: every interior c of [a, b] is the odd vertex of a pentagon inside the interval. Put c = DR for a normal subgroup R of X with D < DR < X. Dedekind's law gives (DR ∨ U) ∧ V = U ∨ (DR ∧ V), whose two sides are V and U, so no normal subgroup sits strictly between: that is Lemma 2.2. Fences also exclude modular intervals and intervals in soluble groups.

From Lemma 2.2, Lemma 2.3 extracts the structure that drives everything. If \([D, X]\) is fenced, then \(X\) modulo the core of \(D\) has a unique minimal normal subgroup. That subgroup is nonabelian, hence a direct power \(T_X^m\) of a simple group; it has trivial centralizer; and \(D\) acts transitively on its simple factors. An abelian minimal normal subgroup would make the interval modular, and two minimal normal subgroups would leave it with at most two elements.

Two ways labels can move

Propositions 2.6 to 2.8. Equal labels merge coordinates into strips and strictly lower the multiplicity. A strictly smaller label forces a coordinatewise product, and one coordinate then carries the saturated part of the interval onto a genuine subgroup interval in an almost simple group. All the group theory of Sections 3 to 7 happens in such projections.

A tested chain

Definition 3.1 with N = 4. Because shortcuts exist for all pairs, every subchain keeps its shortcuts, which is what lets the proof thin the chain again and again. Not drawn: the fences below every vertex, the coatom conditions, the sixteen-atom diamond hanging under each upper vertex, and the bottleneck condition at the few vertices that lack a fence.

Why should such chains be short when the end labels differ? Read the projected picture. The image \(H^*\) of the bottom is a second maximal subgroup of the almost simple group with socle \(T_b\), so by Burness, Liebeck and Shalev it has at most five nonabelian chief factors. Each \(x_i\) projects to \(H^* P_i\) with \(P_i \le T_b\), and the growing labels \(T_i\) live inside the \(P_i\) as "active" chief factors. The two-step routes mean that \(T_i\) always sits inside \(T_j\) through one or two maximal-subgroup steps. Aschbacher's theorem lists those steps, and each one changes a numerical invariant (the field exponent, the natural dimension, or the rank) in a way that the arithmetic of two-step routes cannot sustain indefinitely. The proof is the bookkeeping that makes this precise for all finite groups at once.

The proof of Theorem 3.2, reduction by reduction

Sections 3 to 7 as a single descent. Each box removes a class of configurations from the hypothetical unbounded family while keeping the family unbounded, so the next box may assume the configurations that remain. The last line of a box names the external results its step leans on.

The table says what each reduction proves, what it imports, and how far this reading got with it.

Step	What is proved	Main inputs	Status of this reading
Lemma 3.7	The projected bottom has at most five nonabelian chief factors; the stabilizer types used along shortcuts come from one bounded pool; equal-label stretches have bounded length; multiplicity ratios take boundedly many values	Burness–Liebeck–Shalev; the action structure of O'Nan–Scott and Aschbacher; a lemma bounding towers of natural alternating actions	plausible, not verified
Lemma 3.9	No upper label is an alternating group of degree at least 7	the \(M_{16}\) gadget projects to an \(M_{16}\) interval in \(A_n\) or \(S_n\), which Basile's thesis rules out	the logic checked; consistent with Basile's abstract
Lemma 3.12	Only boundedly many labels of Lie rank at most \(R\) occur	Larsen–Pink; the isogeny theorem; counting prime factors of field degrees	the logic checked; the inputs not verified
Proposition 3.13	Reduce to classical labels of growing rank, with equal multiplicities and solvable "killed kernels"	finite Ramsey on multiplicity ratios; the five-chief-factor bound to cut the nonsolvable gaps	the logic checked
Section 4	Along every two-edge shortcut: no purely geometric path, no change of characteristic, a common field, no large unipotent radical, and quadratic growth of dimension	Kleidman–Liebeck; Landazuri–Seitz and Häsä; Lübeck; a Chevalley–Warning construction of invariant totally singular subspaces; "coordinate normal tests" that read the lattice's fences inside the group	not verified; the degree and field-of-definition bounds used for clause (C6) of Proposition 4.1 are formalized in Lean
Section 5	Each retained inclusion of finite components lifts to a homomorphism of simply connected algebraic groups, compatibly along a path	Steinberg's covering and restriction theorems; Lang–Steinberg; Bendel et al.; Garibaldi–Nakano; Dowd–Sin	not verified; the densest run of delicate claims
Section 6	The natural module of a later label has at most \(30b + 62\) composition factors on an earlier component, uniformly, where \(b\) bounds the denominators of certain field ratios; it is not the \(B\) of Theorem 3.2	the normal tests give a solvable centralizer; an \(\mathrm{SL}_3\) in a centralizer bounds multiplicities by 15; packets of Galois-conjugate constituents; a congruence between source and ambient Frobenius shifts	not verified
Section 7	Two more Ramsey steps make natural restrictions irreducible; Seitz's triples then leave at most seven possible ambient ranks, against eight disjoint comparisons	Burness and Testerman's corrected table of irreducible triples; irreducibility on a finite group implies irreducibility on any algebraic group containing its image	the logic checked; the table's rows not verified

How Ramsey theory is used, and how it is not

Every Ramsey step in the paper follows one pattern. Ramsey theory enters only as a compactness device: there is no Ramsey-theoretic property of lattices, no coloring of the lattice, and no partition regularity in the conclusion. Along the chain, some relation between pairs \(i < j\) takes values in a palette of absolutely bounded size. Color each pair by its value and pass to a homogeneous subchain. The chain order supplies a transitivity law for the relation (ratios multiply, valuations add, composition counts add), and on a homogeneous triple that law forces the common value to be trivial, because a constant \(t\) must satisfy \(t \cdot t = t\), or a constant vector must equal twice itself. The chain is then uniform in that respect, and the next relation is attacked.

The one pattern behind every Ramsey step in the paper: a palette of bounded size on pairs, a homogeneous subchain, and a transitivity law along the chain that forces the constant to be trivial.

The pattern is applied five times.

1. Multiplicities (Proposition 3.13). The socle multiplicities \(m_i\) of the chain vertices have ratios from a palette of bounded size, by Lemma 3.7. Homogeneity gives \(t^2 = t\), so all retained multiplicities are equal, and every comparison has exactly one active simple factor per coordinate.
2. Field exponents and dimensions (Lemma 4.5). The relation is \(x_j / x_i = c \cdot u^{\pm 1}\) with \(c\) from a fixed finite set of rationals and \(u\) an integer with at most \(h\) prime factors. Color a pair by the vector of valuations at the finitely many primes of the \(c\)'s, together with the total valuation outside them. On a homogeneous triangle each coordinate equals twice itself, and outside the fixed primes nothing cancels because all signs agree, so every ratio is one. This is applied to field exponents to get a common field (Lemma 4.13 and Proposition 4.7), and to natural dimensions to exclude a subfield step paired with an extension step on every comparison (Lemma 4.6). The authors note that field ratios alone would not suffice: the exact dimension formula is what makes the palette finite.
3. Parabolic multipliers (Lemma 4.14). For a fixed upper vertex the possible inner index multipliers form a list of bounded length, and a pair is colored by its position in that list. Homogeneity equates two multipliers and reduces an index ratio to the order of an outer automorphism group, which is too small against a unipotent radical.
4. Composition counts (Proposition 7.4). A pair is colored by the numbers of nontrivial and trivial composition factors of the later natural module on the earlier component, a pair of integers bounded by the uniform constant of Section 6. On a homogeneous subchain, additivity along \(i < j < k\) forces every nontrivial constituent to restrict irreducibly. A second coloring, of triples, marks those with a non-natural tensor factor; a rank count bounds such chains, leaving chains on which natural modules restrict irreducibly.
5. The last split (the end of Section 7). A pair is marked when its shortcut has a one-digit edge with a non-natural restricted factor. Unmarked chains satisfy polynomial growth along one shortcut but doubly exponential growth along a fixed number of consecutive comparisons, a contradiction. Marked chains give eight comparisons whose source ranks all lie in a set of at most seven ranks, by Seitz's classification, and the eight are distinct because labels strictly increase.

What a quantitative version would cost. The colorings are iterated: a homogeneous subchain for one relation is the input to the next coloring, and the palettes have sizes like \((c + 1)^2\), with \(c\) itself coming from constants that the classification-based lemmas never make explicit. Even with every constant in hand, \(B\) would be an iterated Ramsey number for pairs and triples with dozens of colors, a tower-type quantity. That is why the paper never estimates \(B\), and why the companion's size ceiling \(M^*\) is a five-fold iterate of a fast-growing function. The companion also uses the finite Hales–Jewett theorem and the finite vector-space Ramsey theorem of Graham, Leeb and Rothschild for its affine charts.

If Ramsey theory is to do more than compactness here, the place to look is Lemma 3.7(iii), the bounded length of equal-label stretches, together with Lemma 3.5, which bounds the height of overgroup lattices in towers of natural alternating actions. Those are statements about chains of block systems in permutation groups, and they are the only places where the chain's combinatorics meets the lattice structure rather than numerical invariants.

Section 8 builds the lattice

Left, Lemma 8.2: a fresh vertex of an insertion into [a, b] is above exactly the old vertices below a, and below exactly the old vertices above b. Right, the paper's equation (8.11): the four components share only 0 and 1, which makes the whole lattice self-dual and fenced at the top level.

There are two components before decoration.

• The Boolean component is \(B_4\), the subsets of a four-element set. Its forward requested pairs are \((v, 1)\) for every proper nonzero \(v\), fourteen tests, each a tested chain from \(v\) up to the top. Its reverse requested pairs are all comparable pairs \(v < u\) of proper vertices, thirty-six tests, each read in the dual order inside \([v, u]\).
• The detector has a middle vertex \(X\), below it two chains \(0 < p_i < d_i < q_i < X\) that meet only at their ends, and above it two chains \(X < e_i < z_i < f_i < 1\) of the same kind. Its forward pairs are \((d_1, 1)\), \((d_2, 1)\) and \((X, 1)\), and its one reverse pair is \((z_1, X)\). Its job is that every coatom of \([0, X]\) lies above some \(d_i\), which in the group forces the point stabilizer to induce every inner automorphism of \(T\).

One test on a pair \((a, b)\) is built in five batches.

1. Insert a chain with \(N - 1\) fresh interior vertices from \(a\) to \(b\).
2. For every pair \(i < j\), insert one fresh middle vertex \(v_{ij}\) into \([x_i, x_j]\): the shortcut.
3. Insert fences (two disjoint two-vertex chains) into every \([x_i, x_j]\), and into every \([a, v_{ij}]\) with \(i \ge 1\).
4. Under every upper target \(u\), insert a fresh \(m_u\) and sixteen incomparable vertices between it and \(u\): the exact \(M_{16}\).
5. Insert two coatom witnesses for every \((a, u)\) and every \((c, b)\) with \(c\) a lower principal vertex, so that the principal vertices are meets of coatoms.

A final batch then fences \([0, t]\) for every \(t\) in a forward comparison interval and \([t, 1]\) for every \(t\) in a reverse one. Lemma 8.4 counts at most \(27N^2\) fresh vertices per test, and Lemma 8.5 bounds a component by \(9(q_0 + 27hN^2)\), where \(h\) is the number of requested pairs.

Sections 9 and 10 break it

Pálfy's dictionary, Proposition 9.4. An invariant subdirect subgroup of the socle is a product of diagonal strips indexed by the cosets of a subgroup U above the point stabilizer, with the strip identifications given by a homomorphism β extending the stabilizer action α. Containment of subgroups is reverse containment of domains together with restriction. Because every subgroup above a subdirect one is subdirect, the whole filter above Y_J becomes the group interval [A, U_J].

Four facts are then forced, and together they are Proposition 9.7.

• (E1) Each \([A, U_J]\) is fenced, so \(U_J\) modulo the core \(C_J\) of \(A\) has a unique minimal normal subgroup \(R^{I_J}\), and the reverse tests make \(R\) the same for all proper nonempty \(J\). The group \(R\) need not be \(T\).
• (E2) Domains grow as faces shrink. If \(J \subsetneq K\) then \(U_J < U_K\) and \(\beta_K\) restricts to \(\beta_J\), the equal-type transport of Section 2 applies, and the domains of a family with proper union \(K\) generate \(U_K\).
• (E3) Every image \(\beta_J(U_J)\) equals \(\alpha(A)\), which contains \(\operatorname{Inn}(T)\). The containment comes from the detector: a proper invariant subgroup of \(T\) would transport to a vertex strictly between \(D\) and \(X\) lying under a coatom of \([D, X]\), and every such coatom is above a \(d_i\) whose socle part is subdirect, which the diagonal-link argument forbids. The equality then follows from the fence on \([A, U_J]\), by Lemma 2.2 applied to the kernel of \(\beta_J\).
• (E4) If a family of proper faces has union \(\{1, 2, 3, 4\}\), the forward groups meet in \(D\), so their socle parts meet in \(D \cap S = 1\). A common extension of their \(\beta\)'s to the subgroup their domains generate would give a nontrivial subdirect subgroup inside that trivial intersection, so no common extension exists.

The paper's Figure 2. Solid edges are restrictions of actual extensions on nested domains. Proposition 10.8 shows that if α killed the core of an atom, lifts of socle factors from the three faces through it would glue to a common extension on the full union, which (E4) forbids; so α(C_x) contains Inn(T) for every atom. Lemma 10.9 passes this to all proper faces by intersecting cores, and Lemma 10.2 then glues {1, 2, 3} and {2, 3, 4}, which is again forbidden.

Lemma 10.2 is the hinge, and it is short. Let \(Q\) be the least normal subgroup of \(A\) whose image under \(\alpha\) contains \(\operatorname{Inn}(T)\). It exists because the image of an intersection of two normal subgroups contains the image of their commutator, and so contains the perfect group \(\operatorname{Inn}(T)\). If every domain core \(C_i = \operatorname{core}_{U_i}(A)\) has image containing \(\operatorname{Inn}(T)\), then \(Q \le C_i\), and the analogous least subgroup of \(C_i\) is normalized by \(U_i\) and equals \(Q\). So \(Q\) is normal in every \(U_i\), and conjugation on \(Q / (Q \cap \ker \alpha) \cong T\) defines one homomorphism from the group the \(U_i\) generate to \(\operatorname{Aut}(T)\), restricting to each \(\beta_i\). Proposition 10.8 is the long part: it builds explicit lifts of socle factors inside the three faces through an atom whose core is killed, detects factor labels with core subgroups \(B_k\), and uses a word-collection lemma to show that the lifts generate a subgroup on which \(\alpha\) extends. This reading checked every step of Lemmas 10.1 to 10.10, and Lemmas 10.1, 10.2, 10.5 and 10.7 are among the results OpenAI has formalized in Lean.

What is already formalized

OpenAI's scope note for this family, lean/docs/206.md, names only one result, the companion's colored-graph criterion, and the repository's formalization catalog lists nothing else. The library holds more than that. Two folders matter: OAI/Algebra/Universal, four files on the companion, 729 lines in all; and OAI/GroupTheory/FiniteLattice, fourteen files on the main paper, 2,583 lines in all. The library's root module imports both, and neither contains an unfinished proof, an added axiom, or native evaluation. Only the graph criterion has a comparator challenge, an independent re-check of the proof against a separately written statement that allows only Lean's three standard axioms (propext, Quot.sound and Classical.choice). This post read the files; it did not build the library, which runs to more than 120,000 Lean files.

Result	Paper	In OpenAI's Lean library
A finite lattice is a congruence lattice if and only if it has a finite colored-graph witness	Companion, Theorem 2.2	graph_criterion, with a comparator challenge
The witness test at a fixed size is decidable	Companion, the first half of Corollary 2.3	graphSizeDecidable
The congruence lattice of the coset action on \(G/H\) is the interval \([H, G]\)	Companion, Lemma 3.3: the easy half of Pálfy–Pudlák	coset_action_correspondence
Fences and the normal-subgroup test; a fenced interval is not modular	Main paper, Definition 2.1 and Lemma 2.2	Fenced, normal_test, Fenced.not_modular
Intersections of normal subgroups keep a perfect image	Main paper, Lemma 10.1	perfect_le_map_iInf
The common-core criterion and its conjugation extension	Main paper, Lemma 10.2	common_core
Taking cores without losing a simple image	Main paper, Lemma 10.5	retained_core
Collection with labeled factors	Main paper, Lemma 10.7	collection
Inner automorphisms of a nonabelian simple group	Facts supporting Lemma 9.1	conj_injective, inner_perfect
Degree and field-of-definition bounds for irreducible representations of perfect groups, with a matrix form of Hilbert's Theorem 90	Main paper, inside the proof of clause (C6) of Proposition 4.1, which bounds the degree and the field of definition of a representation	irreducible_perfect_cover_bounds, matrix_hilbert90
Those bounds do not imply the five-chief-factor bound	No counterpart in the paper	cover_estimates_do_not_imply_five_chief_layers

What OpenAI's Lean library covers, result by result. A filled chip in the accent color is formalized there; a plain outline is not; the dashed outline marks Theorem 3.2, which is neither verified nor formalized.

The formal statements are faithful to the paper. Here are Definition 2.1 and the main assertion of Lemma 2.2, verbatim from the library:

def Fenced {α : Type*} [Lattice α] (a b : α) : Prop :=
  (∃ c, a < c ∧ c < b) ∧
    ∀ c, a < c → c < b →
      ∃ u v, a < u ∧ u < v ∧ v < b ∧
        c ⊓ u = a ∧ c ⊓ v = a ∧ c ⊔ u = b ∧ c ⊔ v = b

theorem normal_test (D R : Subgroup G) [R.Normal]
    (hf : Fenced D (⊤ : Subgroup G)) : R ≤ D ∨ D ⊔ R = ⊤ := by

Lemma 10.2 as OpenAI's library states it

The ambient group K is generated by the domains U i, all containing A, and T is a simple group that is not abelian.

def Statement (ι : Type*) [Finite ι] [Nonempty ι]
    (A : Subgroup K) (U : ι → Subgroup K) (hAU : ∀ i, A ≤ U i)
    (alpha : A →* MulAut T) (beta : ∀ i, U i →* MulAut T) : Prop :=
  (∃ x y : T, x * y ≠ y * x) →
  (⨆ i, U i) = ⊤ →
  (∀ i, ∀ a : A, beta i (Subgroup.inclusion (hAU i) a) = alpha a) →
  (∀ i, (MulAut.conj : T →* MulAut T).range ≤
    (((A.subgroupOf (U i)).normalCore.map (U i).subtype).comap A.subtype).map
      alpha) →
  (MulAut.conj : T →* MulAut T).range ≤
      (A.normalCore.comap A.subtype).map alpha ∧
    ∃! b : K →* MulAut T, ∀ i, ∀ u : U i, b u = beta i u

One file has no counterpart in the paper. It proves a negative statement:

theorem cover_estimates_do_not_imply_five_chief_layers :
    ¬ (∀ (G : Type) (_ : Group G) (_ : Finite G) (_ : Group.IsPerfect G),
      ∀ (s : ChiefNormalSeries G), PerfectCoverEstimates G →
      (∀ i, ¬ Group.IsSolvable (s.factor i) → PerfectCoverEstimates (s.factor i)) →
      s.nonabelianCount ≤ 5) := by

In words: the representation-theoretic estimates on the degree and the field of definition, even when they hold for every nonsolvable chief factor, do not bound the number of nonabelian chief factors by five. That is consistent with the paper as released, which does not derive the bound but imports it from Burness, Liebeck and Shalev.

Everything else is unformalized.

• labels and label transport (Lemma 2.3 and Propositions 2.6 to 2.9);
• Theorem 3.2 itself, apart from the estimates above;
• the lattice of Section 8, the dictionary and detector of Section 9, and the rest of Section 10, including its final contradiction;
• Theorem 1.2, and the hard direction of Pálfy–Pudlák that Theorem 1.1 needs;
• from the companion: the representation of L7, the least-carrier reduction, the undecidability theorem and the minimum lattice.

What Lean could reach, and what it cannot

Lean is a good place to finish the elementary half of this proof.

• Classical logic is native. The two non-constructive steps cost nothing.
• Mathlib already has much of the algebra. Mathlib as OpenAI pins it (commit d13f23b, 24 September 2026) has Dedekind's law, normal cores, Goursat's lemma, the correspondence between blocks and overgroups of a stabilizer, Sylow's theorems, transfer, Schur–Zassenhaus, Jordan–Hölder, the simplicity of \(A_n\), Jordan's theorems on primitive groups containing a transposition or a 3-cycle, the intransitive maximal subgroups of \(S_n\) and \(A_n\), the Iwasawa criterion, Chevalley–Warning, Hilbert's Theorem 90, Maschke's theorem, character orthogonality, root data and Cartan matrices, semisimple Lie algebras, and affine group schemes.
• OpenAI's library is a head start. It covers perhaps a quarter of the elementary half, and another family's files contain a finite Ramsey theorem for hypergraphs.
• Large AI-assisted formalizations already exist. The Feit–Thompson odd order theorem was formalized in Lean this summer, in about 841,000 lines, most of them written by AI agents.

What that buys comes in three tiers.

• Within reach. The conditional theorem "chain rigidity and Schreier's theorem imply a negative answer to the FLRP": Section 2, Definition 3.1 and Theorem 3.2 stated as a hypothesis, the Section 8 lattice built for every \(N\), Sections 9 and 10, and the hard direction of Pálfy–Pudlák. This is a matter of weeks by hand. The missing infrastructure is modest: minimal normal subgroups, socles, chief series, characteristically simple groups as powers of simple groups, and subdirect products of many factors, since Mathlib's Goursat lemma handles two.
• Feasible with more work. The companion's least-carrier reduction and its case analysis, with Schreier's theorem as a hypothesis; its representation of L7; and its undecidability reduction, with its structural theorems as hypotheses. The last also needs Hilbert's tenth problem finished in Mathlib, which so far has Matiyasevich's key step, that exponentiation is Diophantine, and lists the rest as a to-do; the full theorem has been formalized in Coq.
• A cheap audit. Check the numerical and Ramsey skeleton of Sections 3 to 7 against abstract hypotheses, as OpenAI's non-implication file does for one estimate. That tests whether the growth and Ramsey bookkeeping follows from the stated inputs without formalizing the inputs.

Some things remain out of reach.

• Theorem 3.2, now mainly because of algebraic groups. Sections 5 to 7 need simple algebraic groups in positive characteristic, their rational modules and highest weights, Steinberg's tensor product and restriction theorems, and Seitz's classification of irreducible triples. Mathlib has none of this, and I found no Lean formalization of Aschbacher's theorem, Larsen–Pink, Steinberg's theorems or the triples. Without that vocabulary, even a conditional formalization cannot state its inputs faithfully.
• Schreier's theorem, as a theorem. As a hypothesis it is one line of Lean. As a theorem it waits on the classification, and the classification is no longer unimaginable in Lean: the odd order theorem now has Lean proofs, FormaTheoria's AI-assisted development reaches the Bender–Suzuki theorem with Glauberman's \(Z^*\) theorem and the Brauer–Suzuki theorem along the way, and Inna Capdeboscq and Damiano Testa lead a human–AI project aimed at the whole classification. These are still the opening chapters of a proof spread over ten to twenty thousand pages, and Schreier's theorem comes at the end, after a family-by-family computation of outer automorphism groups.
• The companion's structural theorems. The undecidability reduction is within reach, but the theorems it rests on share Theorem 3.2's dependencies, by the companion's own account; this reading did not cover them.
• Nothing is lost on the Busy Beaver lattice. With classical logic, Lean defines the least nonrepresentable lattice in a line by Nat.find once existence is proved. The Busy Beaver device serves only the companion's claim that the lattice is specified by bounded arithmetic, and the definition computes nothing either way.

The same split would hold in any proof assistant. Where the library support is thinner, the elementary half costs more; the core is out of reach everywhere for now.

The undecidability claim

What this reading covered

This reading covered the companion's Sections 1 to 4.4, 15 and 17, about forty of its 180 pages. It did not cover Sections 5 to 14 or 16, which carry the structural weight of both its negative family and its undecidability theorem. Everything said below about those sections comes from the paper's own summaries.

The companion makes five claims.

1. A graph criterion (Theorem 2.2). A finite lattice is a congruence lattice of a finite algebra if and only if it has a finite colored-graph witness. So representability is semidecidable, and a decision procedure exists if and only if a computable bound on witness size exists. This is the part with a Lean proof, and it reformulates the fact that a finite algebra's congruences are determined by its unary polynomials.
2. Undecidability (Theorem 15.3). No algorithm decides representability from an order table. Equivalently, no computable function of the lattice size bounds the least representing carrier.
3. Recognizing intervals is undecidable too (Corollary 15.4). No algorithm decides whether a finite lattice is a subgroup interval of a finite group.
4. A direct family (Theorems 4.1 and 16.7). A family of nonrepresentable lattices built directly, with a computable size ceiling \(M^*\) for one member.
5. A minimum lattice (Theorem 17.9). A minimum nonrepresentable lattice \(L_0\), specified by bounded arithmetic over a Busy Beaver constant, with \(7 < |L_0| \le M^*\).

The companion's Theorem 15.3. The quantifier structure is sound, and the trick is neat: the algorithm never constructs the template with unknown weights, which serves only to prove that an existing solution has a bounded replacement. The whole burden is the dashed box.

Why it is not absurd. Several things speak for it.

• A subgroup interval can keep its shape while the group orders around it grow: \([A_{n-1}, A_n]\) is a two-element chain for every \(n \ge 5\), while the index \(|A_n : A_{n-1}| = n\) is unbounded. So a lattice of fixed size can carry unbounded integers, and a counting theorem saying that the size of a template depends only on its syntax is the kind of statement one expects.
• Recognizing natural alternating actions from lattice data is classical business: Jordan's theorem on prime cycles, Bochert's bound on the index of primitive groups, Burnside's theorem on groups of prime degree, and the classification of multiply transitive groups, all of which the companion lists among its inputs.
• Reading addition from equal totals and multiplication from squares, with a factor of 32 in its equation (15.2) correcting the cross term, is elementary once sizes can be read at all.
• The checkable parts were right: the representation of L7 holds up in a GAP computation, the graph criterion is standard, the least-carrier lemma is Pálfy and Pudlák's, and the case analysis of its Proposition 4.11 is the familiar one from Aschbacher's work.

Why skepticism is warranted. Several things speak against taking it on trust.

• The heart of the argument is a recognition theorem for arbitrary representations: whatever finite algebra represents a template, its congruence lattice must reveal the encoded integers in a common alignment, even after the least-carrier reduction passes to a nontrivial lattice image. That is the strongest kind of claim in this subject, and it sits in a hundred pages that no one outside OpenAI has read.
• The two papers share one methodology, uniform bounds along paths over all finite groups obtained through the classification. A flaw in that methodology would sink both, so they are not independent confirmations of each other.
• The specification of \(L_0\) through a Busy Beaver constant is logically sound, but it gives no way to find the lattice.
• OpenAI's own caveat applies: the collection holds results at different stages of verification, and the unformalized ones "could have issues". In Lean, this family has its graph criterion and some lemmas, nothing more.

Assessment

The negative answer has two routes in the two papers, both resting on unverified uniformity theorems obtained through the classification. I would call it plausible and not yet refereed. The undecidability claim is more exposed than the negative answer, because it needs the stronger recognition machinery of the companion's Sections 10 to 14 on top of the same methodology. I would not cite either result as established yet, and I would not bet against the negative answer either.

What would settle it

Four things would move the question from plausible to settled.

1. A referee for Theorem 3.2. It is the one claim that decides the matter, and it needs specialists in the subgroup structure of classical groups and the representation theory of algebraic groups in positive characteristic.
2. A Lean statement of exactly what remains. The conditional theorem described above, built on OpenAI's existing files, would state the open question once, precisely, as a single hypothesis.
3. A reading of the companion's Sections 5 to 14 and 16, before anyone forms a view on undecidability or trusts the size ceiling.
4. An audit of the imported results at the level of clauses, starting with Basile's Theorem D and the rows of Burness and Testerman's table of irreducible triples that Lemmas 7.1 and 7.2 use.

Sources

The manuscripts and the code:

• OpenAI's collection, with its README on how the results were produced.
• A negative solution to the finite lattice representation problem, PDF and LaTeX sources.
• Finite congruence lattices: characterization and undecidability.
• The Lean folders at the commit read here: OAI/Algebra/Universal and OAI/GroupTheory/FiniteLattice; the comparator challenge, FiniteCongruenceGraph.json.
• Mathlib at commit d13f23b, the version OpenAI's library pins.

The formalization landscape:

• Yawara Ishida's Lean proof of the odd order theorem.
• Nie, Zhang, Tang, Testa, Yau, Li and Zhou, FormaTheoria: constructing large-scale Lean theories from mathematical literature, August 2026.
• Capdeboscq and Testa, a modular human–AI approach to the classification of finite simple groups in Lean.

The literature the main paper leans on hardest:

• T. C. Burness, M. W. Liebeck and A. Shalev, Generation of second maximal subgroups and the existence of special primes, Forum of Mathematics, Sigma 5 (2017).
• A. Basile, Second maximal subgroups of the finite alternating and symmetric groups, PhD thesis, Australian National University, 2001.
• C. Tian, The exceptional seven-element lattice as a subgroup interval in \(\mathrm{PSL}_2(64)\), posted on ResearchGate, 28 August 2026.