The Annals Challenge

My team of post-docs funded by this Renaissance Philanthropy grant has constructed a dataset of 50 Lean statements, corresponding to 50 important recent mathematical theorems! The 50 theorems were all published in the Annals of Mathematics (a prestigious mathematical journal) in the 2020s. We build on mathlib, Lean’s mathematics library; my team has built many new definitions and got them merged into mathlib as part of this project.

As well as the dataset, we would like to issue two challenges related to it.

A challenge for humans — state more theorems

We have formalized the statements of around 20 percent of the papers which have appeared in the Annals of Mathematics since 2020. However it seems to be a formidable challenge to get this percentage up to anywhere near 100 percent. A paper in the Annals might mention the Fukaya category associated to a symplectic manifold in the statement of its main theorem, or cuspidal automorphic representations for a connected reductive group, or any number of other complex mathematical definitions. mathlib does not have any of these definitions, and if it continues to grow at the current rate, then it might well be a very long time before it does have them.

The reason that I think this is a problem: if some AI comes up with a new proof about the Fukaya category associated to a symplectic manifold, or automorphic representations, then currently it is extremely difficult to even state that theorem in Lean, let alone to verify the proof. Reading AI-generated mathematics is still a pretty weird and sometimes exhausting experience; the machine sometimes stresses trivialities, or is vague about technical details. If a proof came with Lean code which at least guarantees that the argument is correct, a human can be more confident that they are not wasting their time reading it. However, if it takes thousands of lines of Lean code before we can even state the theorem then the human is going to have to read that too, which is equally miserable and furthermore can only be done by the small subset of mathematicians who have learnt Lean.

A challenge for AI — autoformalize the proofs

The 50 formal statements will shortly be up on lean-eval, under the Annals tag. AIs can be given access to the pdf paper and then they can try to formalize it. But be warned — some proofs will take much longer to formalize than others! At least two of them use 10,000 pages of unformalized group theory, and at least one of them uses 2,000 pages of unformalized algebraic geometry. However at least one of the papers could have been written by Gauss in theory, and should be very easy to mop up. I will let the AIs discover which is which.

The reason for the AI challenge

I have now met many many humans who see challenges like this and say “What is the point? The formalization will teach us nothing new”. But what they mean is that the formalization will almost certainly teach us nothing new about mathematics. Manual formalization of proofs has historically taught humans many abstractions. For example Bourbaki, who were manually formalizing many decades ago, discovered filters. Us humans in the Lean community have seen many stories of the form “we manually formalized the proof of a hard theorem and here is an explanation of why the process taught the authors to think more clearly about mathematics”. This is a big win of manual formalization, when done properly. We will not get that win with the challenge and I am happy to concede this fact.

But instead we will get other wins. For example we will get to find out if the theorem is actually true. This is a serious matter. As well as publishing 213 papers since 2020, the Annals has also published 8 corrigenda/errata and two retractions — so a figure of around 4.7% for errors somewhere in the paper, and of 1% for what was presumably retractions of the main theorem. So a ball-park estimate is that perhaps 2 or 3 of the papers whose main statements we attempted to formalize will, in future, get an erratum, which might say something like “so unfortunately we can currently only prove the main theorem under the extra assumption that X is pseudo-normal, an assumption which should not be necessary and which we hope to remove in future work”. Part of the point of this challenge is that we do not have to live like that any more. And perhaps there’s a 50-50 chance that one of these papers is unformalizable. Let’s find the error early.

On top of that, we will spot more minor typos and imprecisions which make the main theorem of the paper trivially false. I say “more” because we have already spotted several such typos, four of which were in papers written by Fields Medallists. All of the errors in the Fields Medallists’ papers in question are sins of omission — the theorems should have an additional assumption that the non-negative integer needs to be at least three, or the set needs to be nonempty. But they are all there, unfixed, and in the Annals of Mathematics. All of these typos are fixed in the Lean repository. Let’s make the papers better.

Thanks to the team

Whilst I “managed” this work, I did very little of the hard graft; my work was mostly limited to code review and understanding the material. Many thanks to my RenPhil team, which consists of Thomas Browning, Katerina Hristova, David Ledvinka and Justus Springer, for writing the code. Thanks also to our summer interns Jack McKoen and Hang Lu Su, whose work will undoubtedly feature in future releases of theorems.