A lattice no algebra fits?
Two preprints claim that some finite lattice is not the congruence lattice of any finite algebra, and that no algorithm can decide which finite lattices are
Covers result 206 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.
3:56. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
An algebra, in the most general sense, is a set with some operations on it, any number, of any finite arity. A congruence is a way of gluing elements together that respects all the operations, and the congruences of an algebra, ordered by inclusion, always form a lattice. Three points with no operations at all have five congruences, arranged in a diamond. In 1963 Grätzer and Schmidt showed that every algebraic lattice arises this way, but the algebra may have to be infinite.
The finite version stayed open: is every finite lattice the congruence lattice of some finite algebra? Pálfy and Pudlák showed in 1980 that this is the same as asking whether every finite lattice appears as an interval of subgroups, between a subgroup H and a finite group G. (Our computer checks one half of this link on 10 small examples: the congruences of G acting on the cosets of H match the interval exactly.) By 2012, every lattice with at most seven elements was known to work, except possibly one.
Result 206 bundles two OpenAI preprints, both dated September 24, 2026, that answer no. A negative solution to the finite lattice representation problem (87 pages) proves that some finite lattice is not an interval of subgroups in any finite group, and gets the answer through Pálfy and Pudlák. Finite congruence lattices: characterization and undecidability (180 pages) builds its own family of counterexamples and claims more: no algorithm can decide, from a lattice’s table, whether it is the congruence lattice of a finite algebra, or a full interval of subgroups. It also settles that last seven-element case: the lattice is the interval between a group of order 6 and a group of 262,080 elements, and our computer rebuilt that interval and found exactly the seven subgroups the paper names.
What it doesn’t claim
A counterexample of known size. Both papers prove one exists; the smallest has more than seven elements, and the longer paper pins down its exact size only through an uncomputed Busy Beaver number. The shorter paper’s lattice is shown not to be a subgroup interval; the congruence-lattice answer follows only through the global Pálfy–Pudlák equivalence.
Where it stands
- Posted as preprints
- OpenAI, 87 and 180 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Headline claims not formalized; only the colored-graph test and the coset link (docs)
Last checked October 19, 2026. Neither preprint has been revised since they were added to the repository in its initial commit on October 6, 2026. The Lean formalization (the checked statement) covers only the colored-graph test, which the paper calls established background, and the link between cosets and intervals; the counterexamples and the undecidability are not formalized. Neither paper is among those OSVerify reviewed, and we found no expert reaction.
How the proof goes
- Into finite groups. Both counterexample proofs translate lattices into finite groups and use the classification of finite simple groups.
- The shorter paper. Lattices with long chains of small test pieces force, in any group realizing them, the same simple group at both ends of a long enough chain (Theorem 3.2). A four-dimensional cube of subgroups and a detector then force a gluing of homomorphisms that cannot exist (Theorem 10.10).
- The longer paper: yes is checkable. A colored graph whose existence is equivalent to a representation (Theorem 2.2) is a finite certificate for yes; searching graph sizes one by one finds every yes, but may run forever on a no (Corollary 2.3).
- No is not. Integer equations are encoded in lattices, with numbers stored as sizes of permutation blocks and products checked with a squaring trick (Lemma 15.2). A decider would bound the smallest solution of every solvable equation, which would solve Hilbert’s tenth problem, known to be unsolvable (Theorem 15.3).
The numbers in the video
- The interval between PGL2(F2) and PGL2(F64) rebuilt from its 7,303 double cosets (ours): seven subgroups, of orders 6, 18, 42, 60, 126, 504 and 262,080, as the paper names them.
- The coset link checked on 10 small examples, and the squaring identity of Lemma 15.2 (ours).
Read the source
- A negative solution to the finite lattice representation problem (PDF), 87 pages.
- Finite congruence lattices: characterization and undecidability (PDF), 180 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 206.
The 2 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
Transcript
Read the full script
0:00The question
An algebra, in the most general sense, is a set with some operations on it, any number, of any kind. A congruence is a way of gluing elements together that respects all the operations. The congruences of an algebra, ordered by inclusion, always form a lattice: any two have a smallest common coarsening and a largest common refinement. For example, three points with no operations at all have five congruences, arranged in a diamond. In 1963, Grätzer and Schmidt showed that every reasonable lattice arises this way, but the algebra may have to be infinite. The finite version stayed open: is every finite lattice the congruence lattice of some finite algebra? Pálfy and Pudlák showed in 1980 that this is the same as asking whether every finite lattice appears as an interval of subgroups, between a subgroup H and a finite group G. Our computer checks one half of this link on 10 small examples: the congruences of G acting on the cosets of H match the interval exactly. By 2012, every lattice with at most seven elements was known to work, except possibly one.
1:12The claim
Result 206 bundles two OpenAI preprints, both dated September 24, 2026, that answer no. The shorter, 87 pages, proves that some finite lattice is not an interval of subgroups in any finite group, and gets the answer through Pálfy and Pudlák. The longer, 180 pages, builds its own family of counterexamples, and claims more: no algorithm can decide, from a lattice’s table, whether it is the congruence lattice of a finite algebra, or a full interval of subgroups. It also settles that last seven-element case: the lattice is the interval between a group of order 6 and a group of 262,080 elements. Our computer rebuilt that interval and found exactly the seven subgroups the paper names. Not claimed: a counterexample of known size. Both papers prove one exists; the smallest one has more than seven elements, and the longer paper pins down its exact size only through an uncomputed Busy Beaver number.
2:18How the proof goes
Both proofs translate lattices into finite groups and use the classification of finite simple groups. The shorter paper builds lattices with long chains of small test pieces, and shows that in any group realizing them, the simple groups at both ends of a long enough chain must agree. A four-dimensional cube of subgroups and a detector then force a gluing of homomorphisms that cannot exist. The longer paper first gives a finite certificate for yes: a colored graph whose existence is equivalent to a representation. Searching graph sizes one by one finds every yes, but may run forever on a no. Then it encodes integer equations in lattices, with numbers stored as sizes of permutation blocks, and products checked with a squaring trick. If an algorithm could decide representability, it would bound the smallest solution of every solvable equation, which would solve Hilbert’s tenth problem. That problem is known to be unsolvable.
3:18Where it stands
Both preprints are unrefereed and have not been revised. The Lean formalization covers only the colored-graph test, which the paper calls established background, and the link between cosets and intervals. The counterexamples and the undecidability are not formalized. Neither paper is among those OSVerify reviewed, and we found no expert reaction. If they hold, one of universal algebra’s best-known open questions has the answer no, and no single algorithm can tell which finite lattices are the exceptions.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.