The finite lattice representation problem

The finite lattice representation problem asks whether every finite lattice is isomorphic to the congruence lattice of some finite algebra. Grätzer and Schmidt showed in 1963 that every algebraic lattice is the congruence lattice of an algebra, but the representing algebra may be infinite. Two manuscripts in OpenAI's public mathematics collection, both dated 24 September 2026, claim a negative answer: one constructs a finite lattice that is not an interval in the subgroup lattice of any finite group, and its companion claims that representability cannot be decided by an algorithm. The collection's Lean formalization covers the companion's colored-graph characterization of the representable lattices, not the negative answer.

Background

As recounted in the manuscripts' introductions:
- Representation theorems. Grätzer and Schmidt proved that every algebraic lattice is the congruence lattice of an algebra, without a finite carrier in general. Pálfy and Pudlák proved in 1980 that every finite lattice is the congruence lattice of a finite algebra if and only if every finite lattice is an interval in the subgroup lattice of a finite group; this is an equivalence between two universal statements, not between the two properties of an individual lattice.
- Partial results. Pudlák and Tůma embedded every finite lattice in the partition lattice of a finite set, which need not realize it as a full congruence lattice; Repnitskiĭ and Tůma represented every finite lattice as an interval in the subgroup lattice of a countable locally finite group; Snow represented all finite lattices of width at most two; and DeMeo's analysis left one possible exception among the lattices with at most seven elements.
- Subgroup intervals and decidability. Baddeley and Lucchini reduced questions on intervals of height two to finite simple groups, with further reductions by Börner and by Aschbacher that Pálfy compared. McNulty separated the existence question from the question whether representability can be decided from the order table of a lattice.

The original results

A nonrepresentable lattice, 24 September 2026. The main theorem of A negative solution to the finite lattice representation problem states that there is a finite nonempty lattice that is not isomorphic to the congruence lattice of any finite nonempty algebra of any finite signature. It is deduced, through the Pálfy–Pudlák equivalence, from a second theorem: there is a finite lattice that is not isomorphic to the interval between a subgroup and the whole group in any finite group. The manuscript notes that this obstruction is self-dual, so by the Galois correspondence it is also not the lattice of intermediate fields of any finite separable field extension.
Characterization and undecidability, 24 September 2026. The main theorem of Finite congruence lattices: characterization and undecidability states four things: a finite nonempty lattice is representable if and only if it satisfies an explicit colored-graph criterion, which is decidable for each candidate graph size; no Turing machine decides representability from the order table of a lattice; there is a nonrepresentable lattice of minimum cardinality, larger than seven, specified by finite formulas; and it is undecidable whether a finite lattice is a full subgroup interval of a finite group. The manuscript also gives a representation of the remaining seven-element lattice.
Scope, as stated: the representing algebras are arbitrary finite algebras, not restricted to a variety or a carrier size. The first manuscript's lattice depends on a chain-length parameter whose existence is proved without an explicit value. The companion's minimum counterexample is specified through a Busy Beaver constant that is not evaluated, and the companion notes that the search for affirmative witnesses is effective, so only negative instances escape an algorithm.
Method, as described: the first manuscript proves a uniform rigidity theorem for chains of subgroups labelled by nonabelian simple groups, an absolute bound on the length of a tested chain whose end labels differ, using the classification of finite simple groups through the bound of Burness, Liebeck and Shalev on chief factors of second maximal subgroups, Aschbacher's classes, Larsen and Pink's theorem, Landazuri–Seitz bounds, Steinberg's and Lübeck's representation theory, Seitz's irreducible triples and Ramsey arguments. It then builds one finite lattice from a Boolean lattice of rank four and a small detector configuration with inserted chain tests, and shows that a minimal representation would force a common extension of homomorphisms that the construction forbids. The companion encodes principal congruences as edge colors of a finite complete graph, builds a nonrepresentable family from affine subgeometries, and proves undecidability by encoding integer equations into lattices whose numbers are stored as sizes of permutation blocks, so that a decider would bound the solutions of every solvable Diophantine equation, contrary to the negative solution of Hilbert's tenth problem.
Sources. Commit adc7f12 of the openai/math repository: A negative solution to the finite lattice representation problem and Finite congruence lattices: characterization and undecidability.
Formalization. The scope note, present since the repository's first commit of 6 October 2026, links the companion manuscript. It states that the Lean development proves the colored-graph characterization: a finite nonempty lattice is representable exactly when it admits the specified finite graph witness, whose edge colors encode the required congruence relations. It states that the undecidability and subgroup-interval conclusions are outside it. Comparator statement: FiniteCongruenceGraph.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 1 November 2026)
2026-08-28 to 2026-09-19	Report L10 is representable in the repository UniversalAlgebra/fin-lat-rep-gap, on a note of Chenxiao Tian	Prior work, attribution	The repository holds GAP programs for the article of W. DeMeo, R. Freese and P. Jipsen, Representing finite lattices as congruence lattices of finite algebras. Its report recomputes in GAP the interval in PSL(2,64) given in Chenxiao Tian's note of 28 August 2026, The exceptional seven-element lattice as a subgroup interval in PSL2(64), and confirms that it realizes the last lattice with at most seven elements not previously known to be representable, called L₇ in DeMeo's thesis. It finds five further intervals of this shape in GAP's library of tables of marks, the smallest in Sp(6,2), which gives an algebra on 34,560 elements. The companion manuscript represents the same lattice in PGL(2,64); the blog post in the next row identifies the two representations.	GitHub repository; the report is dated 17 September 2026 and was revised on 19 September 2026, before the collection's release on 6 October 2026. Tian's note is posted on ResearchGate and was not read here.
2026-10-07	W. DeMeo, OpenAI and the finite lattice representation problem, blog post	Reading, expert commentary	A post by the author of the 2012 thesis that left the seven-element case open, written with Claude as a reading assistant. It reports that an AI-assisted reading found the lattice-theoretic half of the first manuscript, its Sections 2 and 8 to 10, correct given Schreier's theorem, and that the result rests on the chain-rigidity Theorem 3.2, proved over about fifty pages with the classification of finite simple groups, which it calls unverified and in need of specialist refereeing. It states that the counterexample family is explicit up to a length parameter that is proved to exist but never bounded, and that OpenAI's Lean library formalizes several lemmas of the first manuscript beyond what the scope note names, but not Theorem 3.2. Its reading of the companion covered about forty of 180 pages; it finds the logic of the undecidability argument sound but did not read the structural sections. It reports that the companion's representation of the seven-element lattice is confirmed by a GAP computation and also appears in Tian's note of 28 August 2026, which the companion does not cite.	Personal blog, released under CC BY 4.0. The post states that the line-by-line checks it reports are the model's, not a referee's verification. Read on 1 November 2026.
2026-10-08	MathVet, a GitHub review of openai/math, tables at repository commit `c76f1e4` of 14 October 2026	Review, fidelity of the formal statement	Rates this family "supporting-only": the Lean states only the companion's colored-graph characterization, and nothing in it states that some finite lattice is not representable or that representability or subgroup-interval membership is undecidable. It records a sandboxed Comparator pass on 8 October 2026, with 469 lines in the dependency cone.	Review repository. Read on 1 November 2026.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification, two kernels	Records the challenge `FiniteCongruenceGraph` as certified: Lean's default kernel and the nanoda kernel both accept the solution, in 18 s. C. Toledo's report lists the lane's results.	Repository. The run concerns the formalized statement only.
2026-10-10 to 2026-10-14	con-leche development journal, task #348	Verification, second kernel	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions does not list this family's challenge, so it was accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee reviews rank_029 of the first manuscript and rank_074 of the companion, in JJardine919/openai-math-audit	Review, AI-assisted audit	Both report no gap. The review of the first manuscript states that it checked the reduction lemmas, the final rigidity argument, the lattice construction and the gluing, but did not verify the growth catalogue, the algebraic path lifts or the packet composition-length theorem line by line, and that two external inputs are used as black boxes: the five-chief-factor bound of Burness, Liebeck and Shalev and Basile's bound on intervals of height two in alternating and symmetric groups. The review of the companion states that it checked the graph criterion, the Diophantine reduction and the least-carrier argument line by line, notes that the undecidability proof needs an absolute stock integer whose uniformity is argued only briefly, and skimmed the affine construction and the exclusions based on the classification.	Part of the completed Lattice24 audit; the reviews are published under CC BY 4.0.
2026-10-17	AI Proved What?, episode 206 A lattice no algebra fits?, remade version of 24 October 2026	Reading, exposition	Video explainer of the two preprints, of 87 and 180 pages. It recalls the theorems of Grätzer and Schmidt and of Pálfy and Pudlák and the remaining seven-element case, and states that neither paper gives a counterexample of known size. It reports its own checks: the correspondence between coset actions and subgroup intervals on ten small examples, and the interval between PGL(2,2) and PGL(2,64), rebuilt from 7,303 double cosets, with seven subgroups of orders 6, 18, 42, 60, 126, 504 and 262,080, as the companion names them.	Episode status, last checked 30 October 2026: posted as preprints, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, headline claims not formalized, only the colored-graph test and the coset correspondence; no expert reaction found. The site states that it is made with Anthropic's Claude. Read on 1 November 2026.
2026-10-18	AI Proof Watch, record OpenAI reports a colored-graph criterion for finite congruence lattices	Catalogue record, assessment	The record assesses the colored-graph characterization that the Lean scope covers. It rates the importance as notable and the AI involvement as AI-led, lists the undecidability, the nonrepresentable examples and the subgroup-interval conclusions as outside the selected formal statement, and rates the technical verification as formal, on OpenAI's reported Lean proof, and the human understanding as few, the default when no named explanation is documented.	Curated public tracker; record published 18 October 2026, assessment reviewed 31 October 2026. Read on 1 November 2026.

Notes

The background summarizes the manuscripts' own account of earlier work.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.