Research

One question runs through my work: what mathematics is mechanizable, and which machine-checked results can we trust? The labels have changed, from lattice theory to complexity to type theory to a blockchain ledger to language models; the interest has not. Each time it was a question about structure that could become an effective procedure, or an argument that could be made to answer to a machine. The project pages and the publications carry the evidence; this page tells the story.

Congruence lattices and a sixty-year-old problem

An algebra is a set with operations on it, and its congruences, the equivalence relations those operations respect, form a lattice that records how the algebra comes apart. The finite lattice representation problem asks which finite lattices arise this way from finite algebras. Drop "finite" and Grätzer and Schmidt answered it in 1963: every one does. Keep it and, sixty years on, nobody knows; Pálfy and Pudlák showed in 1980 that the question is equivalent to one about intervals in the subgroup lattices of finite groups.

My thesis settled every lattice with at most seven elements save one and contributed two general methods: overalgebras, which manufacture representable lattices to order, and parachutes, which compose the known theorems of the form "if this lattice is an interval, the group must look like this" into a route to a negative answer. Even then the representations were found by computer search. The project page has the details, and the one seven-element lattice that got away.

From structure to decision procedures

The decade after the thesis went mostly to complexity. The algebraic approach to constraint satisfaction observes that a problem's difficulty is decided by an algebra, the polymorphisms of its template, so classifying finite algebras by their equations classifies computational problems by their complexity. Four papers from those years each turn a structural question into a decision: with Cliff Bergman, universal algebraic methods for constraint satisfaction problems, for the small algebras the general theory misses; with Libor Barto and Antoine Mottet, constraint satisfaction problems over finite structures, extending Schaefer's classification to structures with operations; with Ralph Freese and Matthew Valeriote, polynomial-time tests for difference terms, for a property that had looked out of reach; and with Peter Mayr and Nik Ruškuc, bounded homomorphisms and fiber products of lattices, which makes boundedness decidable for finitely presented lattices.

Making the arguments checkable

Wanting those arguments checkable rather than merely careful took me into dependent type theory. I began a library of universal algebra in Lean in 2018 and moved it to Agda the next year; Lean stayed a second instrument, in teaching and in a 2025 lecture series on formal cryptography. With Jacques Carette the library became agda-algebras, a formalization of the subject as a whole in constructive Martin-Löf type theory, whose flagship result is the first constructive, machine-checked proof of Birkhoff's HSP theorem. The theorem dates from 1935; what was new was learning what a machine demands that a textbook does not, above all where in the universe hierarchy each object lives.

The library is now 339 modules and about 67,000 lines of Agda outside its frozen legacy tree, and the representation problem is the first research program running on it: the problem stated as a type, 27 small-lattice representations certified by the type checker, one error in our own catalogue found that way, and, in September 2026, the Kurzweil–Netter duality theorem closed with no postulates, with a proof that its classical surjectivity lemma implies excluded middle and so had to be restated.

A specification that has to run

Since 2023 I have worked with the Formal Methods team at IO on the Cardano ledger specification, a different discipline from formalizing a theorem. The human-readable specification is generated from the Agda, so there is no prose for the formal model to disagree with; Haskell is extracted from it and run in conformance tests against the production implementation, so it has to agree with a separately written system that live nodes run; and it tracks a chain that changes under it, era by era (FMBC 2024). A formal semantics that executes and is tested against reality is an unusually rich source of checkable signal, and that lesson is the bridge to the current work.

Letting a machine work inside the proof assistant

agda-native-air is infrastructure that lets a language model work inside Agda the way a person does: load a file, ask what a hole wants, try a term, read the verdict. A small server (ADR 0002) exposes Agda's interaction protocol to coding agents; a search loop (ADR 0001) drives it to prove theorems with Agda as the only judge of every step; and a benchmark of 43 obligations makes every claim about the loop reproducible.

The record is small and its ceilings are stated. The loop proves 8 of the 43 obligations. On the standard-library side it proves exactly the six whose proofs are single terms; the other sixteen need an induction, a case split, or a reasoning block, which term-mode search cannot express. The agda-algebras obligations were built with single-term proofs, and there the constraint is what gets proposed: retrieval from a corpus added no solves once each obligation's own original was excluded, while a labeled control with the exclusion off committed every excluded lemma, which locates the constraint in ranking thousands of in-scope lemmas. Every number is on the tracking issue with its run identifier. Nine field sessions record the server as a daily instrument, and the Kurzweil–Netter development above was composed through it.

What connects them

Each phase took a question about structure and asked what a machine could do with it: find a representation by search, decide a property in polynomial time, check a proof, execute a specification, judge a candidate term. A type checker's verdict is an exit code, not an opinion; it is dense, it cannot be talked into "probably green", and it makes a negative result as usable as a positive one.

What I want to work on next

The open problems are specific. Ranking at scale is the measured binding constraint of proof search over a corpus, and the next step is learned premise selection, judged against the loop's honesty ledgers and a recall instrument rather than solve counts alone. The term-mode ceiling is the largest known win: thirteen of the sixteen unreachable standard-library proofs are one shape of structural induction, and reaching them means adding case-split moves without giving up Agda as the only judge.

Two questions reach past Agda. The loop's shape, a verdict only the checker gives, a cheap lane for questions that never decides one, and a benchmark with ledgers, is not specific to one prover, and I want to know exactly what transfers to Lean and what does not. And the ledger says something concrete about formalizing a real language's semantics and building verified analyses on it: the semantics has to execute and be tested against reality, or it is a description rather than a specification. Those are the two directions I most want to spend the next several years on.