oai-math-revised beta

Browse › Algebra › 206 Finite lattice representation and undecidability

Finite congruence lattices: characterization and undecidability

OpenAI · September 24, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We give an explicit colored-graph characterization of the finite nonempty lattices that occur as full congruence lattices of finite algebras, and prove that deciding this representation property is undecidable. In particular, the finite lattice representation problem has a negative answer. We also prove that recognition of full subgroup intervals in finite groups is undecidable.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Comments and discussion

  • William DeMeo, OpenAI and the finite lattice representation problem (blog post, 2026-10-07). An AI-assisted reading of both manuscripts that finds this paper's logic sound, checks its L7 representation in GAP, and calls the undecidability claim "more exposed" because Sections 5–14 and 16 were not covered. It also reports that Chenxiao Tian gave the same seven-element representation in PSL₂(64) in an August 28, 2026 note not in the paper's bibliography. [AI-generated per source] [family-level]

Formalization

  • OpenAI math release, lean/docs/206.md (mirror) (Lean scope note). The note says the release's Lean development proves this paper's colored-graph criterion (Theorem 1.1(i)), with a comparator statement in FiniteCongruenceGraph.lean; the undecidability and subgroup-interval conclusions are outside it.
  • franzhusch, Finite-Lattice-Representation Problem (google-deepmind/formal-conjectures issue #1795, opened 2026-01-20). An open issue proposing a Lean formalization of the affirmative conjecture that every finite lattice is Con(A) for a finite algebra A, which this paper claims to refute; it has no linked pull request or comments. [family-level]

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026,
  author = {{OpenAI}},
  title = {{Finite congruence lattices: characterization and undecidability}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf}{OAI:Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/206.md. The Lean statements have not been checked by people against the paper's claims.

Family 206: Finite lattice representation and undecidability

Some finite lattices are not congruence lattices of any finite algebra, answering the finite lattice representation problem negatively. Moreover, no algorithm decides whether a finite lattice has such a representation, or whether it is a full subgroup interval of a finite group.

Other papers in this family: