Algebra·OpenAI Math·Result 206·Lean formalisation listed
Finite lattice representation and undecidability
One of the 372 results in OpenAI's public mathematics catalogue, filed under algebra: 2 preprints, the latest dated 24 September 2026. This page quotes OpenAI's own summary of the claim, links the papers and abstracts, and will embed the animation.
Latest paper
Finite congruence lattices: characterization and undecidability
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
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. (Lean)
Papers (2)
Finite congruence lattices: characterization and undecidability
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.
A negative solution to the finite lattice representation problem
We give a negative solution to the finite lattice representation problem. We prove that there is a finite nonempty lattice that is not the full congruence lattice of any finite nonempty algebra of any finite signature.
Status
Preprint. The papers have not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Related results in Algebra
- 207The ℓ¹-Bass conjecture for all discrete groupsLean
- 208Finite symmetric tensor categories and the Verlinde tower
- 209Integral counterexamples to Gersten’s conjecture
- 210Foulkes' conjecture for sixth powers and quadratic stabilizationLean
- 193Serre’s intersection-multiplicity conjecture
- 194Lech’s multiplicity conjectureLean