cs.AIOct 13, 2026
SaveA dataset of formalised theorem statements from the Annals of Mathematics
Organizations: Department of Mathematics, Imperial College London · Department of Philosophy, Carnegie Mellon University
Abstract
Recent progress in autoformalisation of mathematics using AI has been impressive. Measuring this progress requires datasets of formal statements that are both hard and trustworthy. We present AnnalsChallenge: 50 formalised theorem statements written by hand in Lean 4 using Mathlib. Each is the main result of a paper published in the Annals of Mathematics since 2020. Every formalisation was manually reviewed and then audited by AI. We release them without formalised proofs.
Figures & tables
| Difficulty | Sample | Formalised |
|---|---|---|
| 1 | 40 | 36 |
| 2 | 37 | 11 |
| 3 | 56 | 3 |
| 4 | 44 | 0 |
| 5 | 30 | 0 |
| Total | 207 | 50 |
Table 1: Distribution of papers by estimated difficulty of formalising their main theorem statements.
| Subject area (MSC) | Papers | Formalised | % |
|---|---|---|---|
| Algebraic geometry | 54 | 8 | 14.8% |
| Number theory | 50 | 20 | 40.0% |
| Partial differential equations | 29 | 2 | 6.9% |
| Differential geometry | 27 | 3 | 11.1% |
| Dynamical systems and ergodic theory | 21 | 4 | 19.0% |
| Group theory and generalizations | 20 | 8 | 40.0% |
Table 2: Subject-area coverage of the 207 papers considered and the 50 papers whose main theorem statements were formalised. Papers may belong to more than one subject area.
| Model/Harness | Proofs formalised / 50 | % |
|---|---|---|
| Axiom Prover (Axiom Math) | 40/50 | 80.0% |
| Humanifa + GPT 5.6 sol | 34/50 | 68.0% |
| NEAR AI w/ DeepSeek V4 | 33/50 | 66.0% |
| Tau (caj.al) | 23/50 | 46.0% |
| Midas | 20/50 | 40.0% |
| Total | 40/50 | 80.0% |
Table 3: Accepted community proof submissions on LeanEval as of 2 October 2026.