Guest post: Auto-formalization adventures in number theory

David Loeffler (UniDistance Switzerland)

Like everyone in the mathematical world, I was amazed by the news stories that broke at the beginning of this month about AI-assisted formalization of mathematics, especially the successful Claude formalization of Fermat's last theorem. Based on what I'd heard, I thought it would be a while before AI's could tackle Fermat. To my lasting shame, I actually gave a seminar talk only a few days before the FLT announcement, confidently predicting that it was probably a year away at least! Little did I know that the formalization effort was already under way as I spoke.

I learned via the Lean Zulip chat that Prove2Me had been used in coordinating the FLT formalization, so I thought I'd have a look at Prove2Me and maybe try it out for myself. I was very pleasantly surprised to see how easy it was to set up a "mission", with ready-made prompts supplied to guide your AI agent through the setup.

Mission 1: a 1980's classic

For my first mission, I chose a classic number theory research paper from the 1980s, "On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer" by Mazur, Tate and Teitelbaum. This paper is one of the cornerstones of Iwasawa theory – it is famous enough to be known just by its authors' initials "MTT", so that became the name of my mission too. I explained to ChatGPT the specific statement from the paper I wanted formalized, let it devise some intermediate milestones along the way, and ticked the boxes to approve that the statements looked correct (maybe a little less carefully than I should have done). That was enough to launch the mission.

I watched fascinated as the "mission graph" grew. Initally it reminded me of the Hydra of Greek mythology - a many-headed monster, which sprouted multiple new heads each time one was chopped off. My agent, soon joined by others, was working backwards from the initial target, submitting proofs that one of the still-unproved statements followed from a list of several, hopefully simpler statements – which then became goals for the next round. Eventually, the hydra-like growth phase started to slow down, and the Hydra's heads began to turn dark green¹ showing that those theorems were solidly proved. After a very short time – only 3 days – I woke up to see a message from my colleague Chris Birkbeck (who had been contributing some of his own agent-power to the project) saying that the MTT mission was complete, and the main theorem of the first half of the paper was formalized!

I was very happy with this, because it settled an annoying inconsistency in the literature. The theorem that my mission had formalized says, very roughly, that there exists a certain kind of function satisfying an "interpolation property" specifying its values at certain special points; this interpolation property is a little messy to write down. There are several accounts of this theorem in the various published papers; and, way back in 2017, an unusually careful number theorist (Michael Fütterer, a PhD student in Heidelberg at the time) spotted that the statements are not all compatible with each other. The two versions differ by a sign, and there is no way that the two different versions can be true at once. Embarrassingly, Fütterer found that the papers which state this theorem are roughly equally split between the two sign choices, with famous landmark papers in both camps! Fütterer's analysis strongly suggested that MTT's choice of sign is the correct one; and having now formalized a proof of the precise statement given in MTT, we can now finally be sure that MTT's formulae are indeed correct (and either the papers with the other sign choice are wrong, or mathematics itself is inconsistent).

Altogether the process was very smooth. There were only a couple of slight hiccups I noticed. Firstly, my list of 7 intermediate milestones was misguided. I had hoped to divide up the project into roughly equal chunks, but in the end most of them were ticked off almost immediately and the vast majority of the work concentrated on a single milestone – I would have been better off giving just a bare goal without specifying any milestones, and letting the agents pick their own route. Secondly, there were a few dead ends: occasionally the agents would submit sketches "reducing" one of the open goals to new subsidiary goals that were actually impossible to prove, usually because running hypotheses (like "0 < N") hadn't been propagated to the new goals. This needed a bit of corrective action, deprecating these bogus statements and the reductions assuming them, but in each case it was relatively painless.

Misson 2: A recent breakthrough

A week or so later, in a brief gap amid the start-of-semester teaching rush, a random thought struck me. Way back in February this year, I'd had an email exchange with a colleague (Farrell Brumley) about a recent preprint by two young number theorists, Daniel Kriz and Asbjørn Nordentoft, Horizontal p-adic L-functions (Arxiv preprint: https://arxiv.org/abs/2310.20678), proving many new results about non-vanishing of L-functions. The results were intriguing, but the methods were very strange indeed, involving taking an infinite sequence of arbitrary choices and sticking them together in a highly non-canonical fashion. Kriz and Nordentoft's paper had existed in preprint form for some while, but hadn't yet been published, and I had heard rumours that some of the experts in the area were not completely convinced that these unorthodox methods could be correct.

Unusually for a cutting-edge paper in number theory (a notoriously technical field), the Kriz-Nordentoft paper has relatively few pre-requisites. It uses the modular symbol theory developed in MTT, and one substantial but well-known theorem due to Friedberg and Hoffstein involving quadratic twists; the rest is all new. Building on the existing MTT mission, I found myself wondering if I could formalize Kriz-Nordentoft. I figured that either possible outcome would be valuable: if the formalization succeeded, the paper would be vindicated and the experts' doubts dispelled; if the agents got stuck on some specific incorrect calculation or unjustified claim, then the authors would have something concrete to work on – either would be better than the paper remaining in limbo indefinitely. The main risk was that the formalization might take forever, but I felt that the rapid success of the MTT formalization was grounds for confidence. So I picked a representative result from among the paper's half-dozen or so main theorems, and set that up as a mission goal (without any intermediate milestones, learning from my mistake with MTT).

I will write more about how the mission unfolded in a moment, but it was successful: the first case of Theorem 1.1 in the Kriz-Nordentoft paper is correct. The mission verified it assuming only 3 standard theorems whose correctness is not in any doubt (the Friedberg-Hoffstein theorem, the existence of modular-form Galois representations, and the Chebotarev density theorem). One of the proofs in the paper does have a non-trivial gap as currently written; but it is easily fixable in a way that does not change the final statement.

A bumpy ride

In comparison with the very smooth and rapid success of my first mission, the formalization of the KN paper was much more challenging, and required a lot of careful human monitoring and input. With the the MTT project, the AI agents were remarkably successful at making useful reductions and formulating intermediate results: very few of the proposed reductions turned out to be useless or counterproductive. In contrast, for Kriz-Nordentoft, the attempts of AI agents to break up the theorem into manageable pieces were far less successful overall. Very often I found myself having to deprecate and re-work whole branches of the mission graph, because the agents had formulated definitions and intermediate lemmas in an over-restrictive way so the lemmas could not be proved, or (conversely) the formulations were too loose, and hence insufficient to prove the intended goal. It is curious that this happened much more often for the KN mission; perhaps this reflects fact that the theory in MTT is described in multiple highly detailed papers, textbooks and lecture notes, while the Kriz-Nordentoft paper is new and stands alone, so there is far less data for the AI's to base their formalization on.

(As a concrete suggestion to Prove2Me's designers, I'd like to observe that this process of deprecating chunks of the mission graph and replacing them with revised formulations is rather painful to carry out: since nodes are immutable once submitted, one has to individually drop in replacements for any nodes relying on the incorrect ones, one at a time in dependency order, until all the replacements are in position - and only then deprecate the bad node and anything relying on it it. AI agents can automate this to a considerable extent, but it takes a lot of time and credits, and leaves the project in a very muddled state, blocking other agents from contributing, until the replacement is complete. I wonder if some sort of "batch" model, changing a group of related nodes all in one go, might make this less painful?)

The other difficulty I encountered was about constructing new objects. Kriz-Nordentoft's paper involves building a very complicated new mathematical object -- the "horizontal p-adic L-function" of the paper's title (let's call it an HPLF, for short) -- and then proving numerous lemmas about this specific object's properties and behaviour, before eventually applying it to prove the non-vanishing theorems that are the paper's main goal. However, this does not map very well onto Prove2Me's Hydra-like model of collaborative theory-building, gradually breaking down a complicated goal into smaller pieces and working on these in parallel. One cannot prove theorems about an object that hasn't been defined yet! So when a hard construction needs to be formalized, it can bring the whole mission to a standstill. Worse still, if a candidate formalisation of the construction turns out not to be 100% correct, the immutability of Prove2Me nodes makes it extremely awkward to fix, since every theorem and proof using the definition needs to be individually deprecated and re-created.

Instead, one can try to hide the definition behind an existential statement: defining a list of properties characterizing what an HPLF should be. Then we can formulate propositions, "Theorem A: there exists an HPLF", and "Theorem B: if an HPLF exists, then [desirable things hold]". This allows development to proceed in parallel in the two branches, but again it is very difficult and time-consuming to adjust if the list of characterizing properties is too strict (so no object with those properties exists) or too loose (so other "junk" objects besides the intended one satisfy the conditions). This happened several times in the KN project, and the deprecation-and-replacement operations frequently took hours to complete (even without counting the extended interruptions while I waited for my ChatGPT usage credits to recharge).

As a result, although the KN project is much smaller overall than the MTT project (about 17k code lines as compared to 29k), the amount of effort involved was much larger, as was the time taken (about three weeks overall).

Footnotes

1. In the Greek legends, Hercules defeated the Hydra with some help from his side-kick Iolaus: after Hercules chopped off each head, Iolaus used a burning torch to seal the severed necks so the heads would not re-grow. The legends do not record what colour the Hydra was, and based on Prove2Me's colour scheme, I now like to imagine its live heads as light blue, and the stumps cauterized by Iolaus as dark green. The goddess Hera – Hercules' sworn enemy – also sent a crab to pinch Hercules' feet as he fought the Hydra, which seems like a perfect role for ChatGPT's incessant usage-limit warnings. ↩