∑math20

Algebra · Result 206

Finite lattice representation and undecidability

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 2

First page of Finite congruence lattices: characterization and undecidability

Finite congruence lattices: characterization and undecidability

OpenAI · September 24, 2026

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.

Read PDF Download Source

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}
}
First page of A negative solution to the finite lattice representation problem

A negative solution to the finite lattice representation problem

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite
@misc{OAI:A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026,
  author = {{OpenAI}},
  title = {{A negative solution to the finite lattice representation problem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026/paper.pdf}{OAI:A-Negative-Solution-to-the-Finite-Lattice-Representation-Problem-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The finite lattice representation problem asks which finite lattices occur as the full congruence lattice of a finite algebra. The formalization proves the paper's colored-graph characterization: a finite nonempty lattice is representable exactly when it admits the specified finite nonempty graph witness, whose edge colors encode the required congruence relations. This selected theorem is the equivalence with the graph criterion; the paper's undecidability and subgroup-interval conclusions are outside it.

Comparator links

ResultComparator statement
Colored-graph criterion for finite congruence latticesFiniteCongruenceGraph.lean

Scope note on GitHub →