Skip to content

Formal verification

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.

The typechecker as a reward signal

A proof assistant answers one question all day long: is this term a proof of that goal? The answer is an exit code from a process that never reads your explanation of what you were trying to do. I have spent several months building a search loop whose every judgment comes from that exit code, so this is a report on the signal itself: what it is exactly, what it gives a loop that trains or evaluates a reasoning system, and the four things the measurements say it does not give.

Building the Agda MCP: field notes

In July a Claude Code session working in ualib/agda-algebras formalized about 1200 lines of literate Agda, ran fifteen or so typecheck iterations and four full-library builds, and never once called the Agda MCP server I built for exactly that job. The server was configured. Its four tools were listed in front of the model on every turn. The session used agda from a shell prompt instead, every single time.

The session wrote its own post-mortem, and that document became a pivotal design record. Four of the rules the server now runs on are in it, and each exists to address a defect I can name. The project page has the artifacts and the current numbers.

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.