# Finite lattice representation and undecidability

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

- [Finite congruence lattices: characterization and undecidability](../../preprints/Finite-Congruence-Lattices-Characterization-and-Undecidability-September-24-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Colored-graph criterion for finite congruence lattices | [FiniteCongruenceGraph.lean](../ComparatorChallenges/FiniteCongruenceGraph.lean) |