Skip to content

Mathematics

OpenAI and the finite lattice representation problem

On 6 October 2026 OpenAI published a collection of 722 mathematical manuscripts written by an unreleased internal model. Two of them claim a negative answer to the finite lattice representation problem (FLRP), which asks whether every finite lattice is the congruence lattice of a finite algebra. This post explains what the main paper proves and how, which parts of it a careful reading could check, where the risk sits, what the proof assumes, and how much of it is already formalized in Lean. The short version: in an AI-assisted reading the lattice-theoretic half holds up; the whole weight rests on one unverified theorem about finite groups; the proof builds an explicit family of candidate lattices but certifies none, because a parameter it needs is never bounded; and more of it is formalized than OpenAI's own documentation says, though not the part that matters.

Quotients without quotient types

Universal algebra is about quotients. Kernels, the isomorphism theorems, subdirect representation, the Birkhoff HSP theorem, etc. Every one of these takes the quotient of an algebra by a congruence. So a formalization of the subject, in a language with no quotient types, has to answer what 𝑨 ╱ θ means.

agda-algebras answers this question, twice. Each of two trees in that repository provides its own answer, and a comparison of the two is the most useful thing I could hand another practitioner, because it is concretely exhibited, rather than abstractly argued.

Congruences of Partial Algebras

The repository par-alg-rep contains some notes describing a few results that we worked out in the fall of 2016, while I was a postdoc at University of Hawaii, although the main result—a straight-forward proof of the fact that every finite lattice is the congruence lattice of a finite partial algebra—was discovered during a visit to Chapman University in October 2016.

3-SAT and Partition Lattices

It is not hard to see that 3-SAT reduces to the problem of deciding whether all coatoms in a certain partition lattice are contained in the union of a collection of certain principal filters. Therefore, the latter problem, which we will call the covered coatoms problem (CCP), is NP-complete. In this post we simply define CCP. Later we check that 3-SAT reduces to CCP, and then develop some ideas about constructing a feasible algorithm to solve CCP.