Finite-Lattice-Representation Problem

### What is the conjecture

Every finite lattice is isomorphic to the congruence lattice of some finite algebra. Formally, for any finite lattice $L$, there exists a finite algebra $A$ such that $L \cong \text{Con}(A)$, where $\text{Con}(A)$ denotes the lattice of congruences of $A$.

**Sources:**
- https://en.wikipedia.org/wiki/Finite_lattice_representation_problem, http://garden.irmacs.sfu.ca/op/finite_congruence_lattice_problem, https://arxiv.org/pdf/2104.06539, https://en.wikipedia.org/wiki/Congruence_Lattice_Problem, https://arxiv.org/abs/1204.4305

### Prerequisites needed

**Formalizability Rating:** 3/5 (as of 2026-01-20)

Mathlib contains foundational concepts for lattice theory and universal algebra (Lattice.Basic, Algebra.Order.Lattice), but formalizing this problem requires significant new infrastructure. Specifically, the formalization needs: (1) a rigorous definition of congruence lattices for arbitrary finite algebras, (2) a formal definition of lattice isomorphism in the context of congruence lattices, (3) computational methods to verify representations for small lattices (as current research focuses on lattices with at most 7 elements). The representation problem is inherently non-constructive in its statement, making formalization non-trivial despite basic lattice theory being available.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-08
* ams-16
* ams-20

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me.

Start by reading Lattice.Basic and Algebra.Order.Lattice to determine what lattice and universal-algebra foundations are available. Then assess the missing congruence-lattice and finite-algebra infrastructure described in the issue; done means adding a formal Lean representation of the conjecture, with any required supporting definitions and verification methods.

Written by the indexing model from the issue text.