Skip to content

Blog

Notes on machine-checked mathematics: formalization in Agda, tooling that lets language models work inside a proof assistant, and the algebra and lattice theory underneath most of it.

The two previous sites

Eight of the posts here were rescued from them, and every URL those sites served still resolves. The archive has the pages that are kept but are no longer part of the current site.

Posts are also listed by tag, by year under Archive, and by subject under Categories.

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.

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.