# Finite lattice representation and undecidability > Some finite lattices are not the congruence lattice of any finite algebra, and no program can tell which. Plain-English explainer, Lean status and sources. Canonical: https://closedform.nishachay.tech/e/openai-math-2026-206/ Last updated: 2026-10-14 **Some finite lattices are not the congruence lattice of any finite algebra, and no program can tell which.** **Trust:** Formal proof listed · **Papers:** 2 · **First paper:** September 24, 2026 · **Field:** Algebra · **Entry:** 206 *Explained by AI.* Drafted by one AI model and checked sentence by sentence against the paper by a different one. Spot a mistake? Report an error. An algebra's congruences are the groupings its operations respect, and they form a lattice. The finite lattice representation problem asks whether every finite lattice arises this way from a finite algebra. These papers claim the answer is no. They also claim no program can decide which finite lattices arise. A colored-graph test for which lattices arise has a Lean proof. ## At a glance - **First step:** 1980 (Péter Pálfy and Pavel Pudlák, the link to subgroup intervals) - **Significance:** Major. It would settle a central open question of universal algebra, in the negative, and add an undecidability result. - **Trust:** Formal proof listed - **Field:** Algebra (2 papers) ## The explanation Take three objects, a, b and c. Sort them into groups. There are five ways: all apart, three ways to pair two of them, or all together. Ordered by merging, these five groupings form a small diagram. Mathematicians call such a diagram a lattice: any two of its points have a least point above both and a greatest point below both. Now add a rule that moves a to b, b to c, and c to a. Call a grouping a congruence if the rule respects it. Objects in one group must land in one group. Pairing a with b now fails, because the rule then pairs b with c. Only two groupings survive: all apart and all together. A finite algebra is a finite set with finitely many such rules. Its congruences, ordered by merging, always form a lattice. Different rules give different lattices. The finite lattice representation problem runs the other way. Pick any finite lattice. Is there a finite algebra whose congruences form exactly that lattice, with nothing extra? The rules may be anything at all, and as many as needed. Grätzer and Schmidt showed in 1963 that every lattice of a broad kind is the congruence lattice of some algebra[1]. That algebra need not be finite[2]. In 1980, Pálfy and Pudlák tied the finite question to finite groups. Every finite lattice has a finite algebra exactly when every finite lattice is an interval in the subgroup lattice of a finite group[3]. That interval is the set of subgroups between two fixed ones. Many lattices were known to work. Every finite lattice of width at most two does[4]. Among lattices with at most seven elements, only one possible exception was left, and the paper handles it[5]. The two papers claim the answer is no. One claims there is a finite lattice that no finite algebra of any kind realizes[6]. The other claims something stronger. No computer program can take a lattice's table and always decide whether a finite algebra realizes it[7]. If every lattice worked, the program that always says yes would decide it. So the stronger claim also gives the negative answer[8]. The same undecidability is claimed for subgroup intervals in finite groups[9]. There is a smallest counterexample, with more than seven elements[10]. Its description uses a Busy Beaver number, so its actual size is not computed[11]. The single obstacle is that nothing about a hypothetical algebra is bounded. Every lattice in the argument is finite. But a group realizing it could have any order, any rank and any field size[12]. The paper builds lattices whose shapes force long chains of simple subgroups inside any such group. It then needs a bound on those chains that holds for every finite group at once[13]. The classification of finite simple groups, a large body of earlier work, supplies the key inputs[14]. There is also a positive tool. The paper turns a lattice into a question about finite colored graphs. A lattice is realizable exactly when a suitable colored graph exists[15]. Searching through graphs finds every yes answer. What fails is a stopping rule for the no answers[16]. How sure is this? A computer proof checker called Lean has a formal proof of the colored-graph criterion. That covers the equivalence between realizability and the graph test. The undecidability results, the subgroup-interval result and the counterexample lie outside that check. They rest on long arguments using the classification of finite simple groups. No specialist review of either paper has been published. **What it doesn't show.** This does not give the size of a counterexample, or a way to compute it. ## Where it came from This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026. ## Hype check Major if it holds. Only the colored-graph criterion has a Lean proof; the negative answer and undecidability rest on long arguments using the classification of finite simple groups. No specialist review is published. ## Words used - **Lattice:** An ordered set where any two elements have a least element above both and a greatest element below both. - **Finite algebra:** A finite nonempty set with a finite list of operations, each taking a fixed number of inputs. - **Congruence:** A grouping of an algebra's elements that its operations respect: grouped inputs give grouped outputs. - **Subgroup interval:** All subgroups of a group lying between two fixed subgroups, ordered by inclusion. - **Undecidable:** No computer program can answer every instance of the question correctly and always stop. - **Busy Beaver number:** A specific whole number defined from small computer programs; it exists, but no general method computes such numbers. ## The original papers (2) - [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf) - September 24, 2026 - [A negative solution to the finite lattice representation problem](https://github.com/openai/math/blob/main/preprints/A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026/paper.pdf) - September 24, 2026 - [Lean notes](https://github.com/openai/math/blob/main/lean/docs/206.md) ## Quoted lines from the paper (16) [1] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > Gr\"atzer and Schmidt proved that every algebraic lattice is the full congruence lattice of an algebra. [2] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > The carrier in that theorem need not be finite. [3] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > P\'alfy and Pudl\'ak proved that every finite lattice is a congruence lattice of a finite algebra if and only if every finite lattice is an interval in a subgroup lattice of a finite group. [4] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > Positive representation results include all finite lattices of width at most two. [5] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > DeMeo's analysis leaves only one possible exception among lattices with at most seven elements. [6] From [A negative solution to the finite lattice representation problem](https://github.com/openai/math/blob/main/preprints/A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026/paper.pdf): > Thus the finite lattice representation problem has a negative answer. [7] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > There is no deterministic Turing machine that, given the order table of a finite nonempty lattice, always halts and decides \(\mathcal R(L)\). [8] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > Part \textup{(ii)} resolves the finite lattice representation problem negatively, since otherwise the constant affirmative algorithm would be a decider. [9] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > We also prove that recognition of full subgroup intervals in finite groups is undecidable. [10] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > Every finite lattice of smaller cardinality is representable, and \(\lvert L_0\rvert>7\). [11] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > Its constants include one ordinary Busy Beaver integer. The description does not evaluate that integer, the minimum cardinality, or the entries of the order table. [12] From [A negative solution to the finite lattice representation problem](https://github.com/openai/math/blob/main/preprints/A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026/paper.pdf): > Uniformity is the obstacle: every lattice in the construction is finite, but a hypothetical representing group has no prescribed bound on its order, Lie rank, or field size. [13] From [A negative solution to the finite lattice representation problem](https://github.com/openai/math/blob/main/preprints/A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026/paper.pdf): > The bound must be independent of the finite group in which the configuration is represented. [14] From [A negative solution to the finite lattice representation problem](https://github.com/openai/math/blob/main/preprints/A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026/paper.pdf): > The classification of finite simple groups enters this stage through maximal-subgroup structure and representation theory. [15] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > A finite nonempty lattice is representable if and only if it satisfies the finite colored-graph criterion in …. [16] From [Finite congruence lattices: characterization and undecidability](https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf): > The criterion in Part \textup{(i)} gives a search that terminates on representable lattices; it does not provide a computable stopping rule for negative instances. ## Other sources - [openai/math release notes (2026): model provenance and review status](https://github.com/openai/math/blob/main/README.md): “manuscripts and supporting proof artifacts produced by an internal OpenAI model” ## Related - [Donovan's conjecture over fields and complete mixed-characteristic DVRs](https://closedform.nishachay.tech/e/openai-math-2026-203/) - Algebra - [The blockwise Alperin weight conjecture](https://closedform.nishachay.tech/e/openai-math-2026-202/) - Algebra - [Saxl’s conjecture and universal tensor squares](https://closedform.nishachay.tech/e/openai-math-2026-205/) - Algebra - [The ℓ¹-Bass conjecture for all discrete groups](https://closedform.nishachay.tech/e/openai-math-2026-207/) - Algebra - [Tensor saturation for even spin groups](https://closedform.nishachay.tech/e/openai-math-2026-204/) - Algebra - [Algebra](https://closedform.nishachay.tech/science/mathematics/algebra/) - Field · 18 results - [Open since the 1980s](https://closedform.nishachay.tech/open-since/1980s/) - Era · 60 results - [Lean-checked results](https://closedform.nishachay.tech/trust/lean-checked/) - Trust · 242 results - [Report an error](https://github.com/nishachay/closed-form/issues/new?template=report-error.yml&labels=entry-error&title=%5Bentry%20206%5D%20)