Source-linked AI summary
A dataset of formalised theorem statements from the Annals of Mathematics
Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard
TL;DR
Measuring AI autoformalisation progress calls for datasets of theorem statements that are both difficult and trustworthy. AnnalsChallenge provides 50 manually formalised Lean 4 statements from recent Annals papers, reviewed by humans and audited by AI. Mathlib could state these results, and more than half had proof submissions within weeks of release.
Problem
Assessing AI autoformalisation progress requires datasets of formal statements that are both hard and trustworthy.
Source: §1 · p. 1Method
The authors manually formalised 50 recent Annals main-result statements in Lean 4 using Mathlib, then manually reviewed and AI-audited them.
Source: §1 · p. 1, §2.3 · p. 3, §2.5 · p. 3Results
Mathlib could state 50 recent main results, and more than half of the statements had formalised proof submissions within weeks of release.
Source: §5.1 · pp. 4–5Takeaways & Limitations
The authors read the rapid proof submissions as strong interest and an indication that autoformalisation will play an important role in future mathematical review.
Source: §5.1 · p. 5Mathlib still lacks foundations in many areas, making some remaining results often impossible to state for now.
Source: §3 · p. 4
Abstract
from arXiv · showhide
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.
1 Introduction
ANNALSCHALLENGE collects formalised statements of recent Annals of Mathematics results to assess Mathlib’s readiness, enrich its library, and gauge AI autoformalisation. It targets contemporary pure mathematics across a broad research spectrum.
1 Introduction
- The dataset covers 50 main results from Annals papers published in volumes 191–203, about a quarter of the 207 papers from 2020 to mid-2026.The statements are written in Lean 4 using Mathlib.Source: §1 · p. 1
- ANNALSCHALLENGE aims to assess Mathlib’s readiness for contemporary pure mathematics, add missing definitions and theorems, and gauge AI autoformalisation progress.Source: §1 · p. 1
- It is presented as the first formalisation challenge for contemporary pure mathematics, unlike competition benchmarks such as miniF2F [Zheng et al., 2022], FIMO [Liu et al., 2023], and PutnamBench [Tsoukalas et al., 2024].Source: §1 · p. 1
- Other datasets target school-to-undergraduate mathematics or single fields, while research-level datasets differ in source and construction.Examples include FormalMATH [Yu et al., 2025], ProofNet [Azerbayev et al., 2023], CombiBench [Liu et al., 2025], FATE [Jiang et al., 2026], ArXivLean [Gehrunger et al., 2026, Dekoninck et al., 2026], FormalConjectures [Firsching et al., 2026], and SorryDB.Source: §1 · p. 2
- The dataset was released on GitHub and LEANEVAL, where submitted proofs are checked for correctness without additional axioms in a sandbox.Source: §1 · p. 2
2 Methodology
The authors selected recent Annals theorem statements for broad subject coverage, formalised them manually in Lean with Mathlib, and applied layered human and AI review.
2 Methodology
- The project prioritises trust, faithfulness to the informal source, and correctness, with human review of local definitions and author consultation when intent is unclear.Source: §2 · p. 2
2.1 Statement selection process
- The team triaged 207 papers by estimated statement-formalisation difficulty, rating each from 1 (definitions already in Mathlib) to 5 (major formalisation work).A low rating does not imply an easy proof; some elementary statements rely on the unformalised classification of finite simple groups.Source: §2.1 · p. 2
2.2 Dataset statistics
- Subject areas came from the Annals website or MathSciNet, and papers could count in multiple areas, so Table 2’s subject totals exceed the number of papers.Source: §2.2 · p. 3, Table 2 · p. 3
2.3 Formalisation philosophy
- Over ten months, the team formalised statements using Mathlib, adding reusable definitions there and keeping rare paper-specific definitions local.Formalisations preserve the source’s generality, naming conventions, and notation while staying close to its natural-language statement.Source: §2.3 · p. 3
2.4 Manual review
- Mathematicians reviewed each statement for edge cases, missing hypotheses, inconsistencies, and interpretive errors, consulting authors about suspected gaps in source papers.Source: §2.4 · p. 3
2.5 AI audit
- After manual review, multiple AI audits found no significant issues in 32 papers, missing assumptions in 7, and formalisation mistakes in 11; all identified issues were fixed before release.Since release, no further misformalisations had been found.Source: §2.5 · p. 3
3 Lessons from the formalisation process
The formalisation process exposed two constraints: implicit conventions can make theorem statements ambiguous, and gaps in Mathlib can block even stating results in some fields.
3 Lessons from the formalisation process
- In some areas, unstated regularity assumptions or context-dependent definitions make the intended theorem unclear and less amenable to direct formalisation.Examples include Fourier transforms and PDE solutions, whose intended meanings may vary.Source: §3 · p. 4
- Mathlib’s missing foundations leave many remaining papers in fields such as symplectic geometry, Lie theory, and moduli stacks often impossible to state for now.The authors describe formalising the remaining 157 papers as a natural goal, but expect building the relevant mathematics in Mathlib to take a long time.Source: §3 · p. 4
4 Autoformalisation results
Community autoformalisation submissions succeeded on many lower-difficulty statements, but the reported results come from an uncontrolled evaluation with non-standardised submission conditions.
4 Autoformalisation results
- Accepted community proofs covered 40 of the 50 challenges, but compute budgets, attempts, human involvement, and source access were not standardised.Source: §4 · p. 4
- Autoformalisation succeeded on 28 of 36 difficulty-level-1 papers, all 11 level-2 papers, and 1 of 3 level-3 papers.The authors caution that proof difficulty may be uncorrelated with statement-formalisation difficulty.Source: §4 · p. 4
5 Conclusion and future work
ANNALSCHALLENGE states 50 recent main results on Mathlib across a broad range of modern research mathematics; within weeks, more than half had formalised proofs submitted to LEANEVAL. Future work includes expanding theorem coverage, scaling with AI while reviewing definitions, and including other journals.
5.1 Conclusion
- 50 recent main results were stated on Mathlib, though the difficulty distribution shows that substantial formalisation work remains.The dataset covers a broad range of modern research mathematics.Source: §5.1 · p. 4
- Within weeks of release, more than half of the statements had formalised proofs submitted to LEANEVAL, indicating strong interest in the dataset.The authors view this interest as an indication that autoformalisation will play an important role in future mathematical review.Source: §5.1 · p. 5
5.2 Future work
- Future work includes adding theorems in underrepresented areas, scaling with AI while carefully reviewing definitions, and covering journals with different subject balances.Several underrepresented areas have limited Mathlib coverage, so extending them would require building out the library first.Source: §5.2 · p. 5
A AI audit prompt
The AI audit prompt asks reviewers to check whether Lean statements and docstrings faithfully match the paper, especially for subtle errors in theorem statements and relied-upon definitions. It directs auditors to test special cases, but not to fill in proofs from scratch.
A AI audit prompt
- Reviewers are asked to check the Lean formalisation and docstring against the paper, especially for subtle statement errors or unfaithful definitions.The prompt suggests testing special cases or proving or disproving simpler cases when useful.Source: A AI audit prompt · p. 7
- The audit is limited to finding misformalisation, not completing the theorem proofs from scratch.The prompt says not to fill in the sorries, while welcoming simpler proofs or disproofs that indicate an error.Source: A AI audit prompt · p. 7
- Reviewers are instructed to commit suggestions to the named branch without pushing, for later human review.Source: A AI audit prompt · p. 7
B Missing or implicit hypotheses in papers
The appendix records slips and implicit hypotheses found in published theorem statements, including boundary cases and assumptions needed for arguments or definitions. Examples range from parameter restrictions to measurability and a condition on T.
B Missing or implicit hypotheses in papers
- The appendix records essentially trivial slips in published versions of formalised theorems.Source: B Missing or implicit hypotheses in… · p. 7
- For the Lorentzian-polynomial theorem, allowing n = 0 and d = 2 makes the statement false: the relevant Hessian condition gives an empty set, while the comparison set contains the zero polynomial.Source: B Missing or implicit hypotheses in… · p. 7
- The fractional expectation-threshold theorem needs ℓ(F) ≥ 2, since ℓ(F) = 1 makes log(ℓ(F)) zero while p_c(F) lies in (0, 1).Source: B Missing or implicit hypotheses in… · p. 7
- The Talagrand selector-process statements omit assumptions used in their arguments, including an inequality condition for a contradiction and finiteness of the collection C.The proof-generated collections C are finite, while countability is needed for the sum to make sense.Source: B Missing or implicit hypotheses in… · pp. 7–8
- Other corrections include requiring nonempty A, n ≥ 3, measurable X and Y, vanishing constant coefficients, and T > 1 in their respective results.The appendix also notes an implicit hypothesis on isolated hypersurface singularities through the origin and a typo in the definition of λSSS.Source: B Missing or implicit hypotheses in… · p. 8