Skip to content

2026

The ETH refutation and what it means for algebra research in complexity

On 26 and 27 October 2026 (UTC), six hours apart, OpenAI and Anthropic each released a preprint claiming that the Exponential Time Hypothesis (ETH) is false: there is a deterministic algorithm that counts the satisfying assignments of a 3-CNF on \(n\) variables in time \(2^{o(n)}\), which refutes ETH because counting decides. Each paper was written by an internal model, each comes with a Lean 4 formalization of its theorem, and neither is refereed. This post says what the two papers claim and how, who can check what, what the Lean files state and what no machine checks, and then whether the claims, if they stand, would change anything for the algebraic approach to complexity. By that I mean the approach to constraint satisfaction built on polymorphisms and clones, the field I work in, not Valiant's algebraic complexity of circuits and tensors; the distinction turns out to matter, since the two algorithms are algebraic in Valiant's sense and not in mine. The short version: the formal theorems are checked by Lean's kernel against statement files, the prose proofs are refereed by nobody yet, and whether the statements say what the papers mean is for human readers, one of whom reports below; the algebraic theory classifies problems up to polynomial time, so almost none of it moves; its fine-grained branch loses the separations it proved under ETH and sees its open question move to a finer scale; and the form of the Strong Exponential Time Hypothesis that most fine-grained lower bounds actually use survives.

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.