A dataset of formalised theorem statements from the Annals of Mathematics

AI summary

Overview

Research area: AI for mathematics / autoformalisation — specifically the construction of a benchmark dataset of formalised mathematical theorem statements for interactive theorem provers (Lean 4 / Mathlib).

Technical level: Advanced. The paper assumes familiarity with Lean 4, Mathlib, the notion of a "sorry" (an unfilled proof obligation), and research-level pure mathematics subject classifications (MSC areas).

Scope: A single-sentence scope: the paper describes AnnalsChallenge, a hand-built dataset of 50 Lean 4 statements of main theorems from papers published in the Annals of Mathematics (volumes 191–203, covering 2020 to mid-2026), released without proofs, together with statistics on subject coverage, formalisation difficulty, an AI audit, and early autoformalisation leaderboard results.

What This Paper Is About

Automated formalisation of mathematics ("autoformalisation") has made rapid progress, but measuring that progress requires benchmarks that are both genuinely hard and trustworthy. Existing datasets are mostly drawn from competitions (Olympiad, Putnam) or undergraduate-level material, so they do not test whether AI systems can handle contemporary research mathematics. This paper addresses that gap by hand-formalising the main theorem statements — not the proofs — of 50 recent papers from one of the top pure mathematics journals, so that models can be challenged to supply the proofs themselves.

Key Contributions

1. AnnalsChallenge, a new research-level benchmark. A dataset of 50 formalised theorem statements in Lean 4 using Mathlib, each being the main result of a paper published in the Annals of Mathematics since 2020 (volumes 191–203, covering 2020 to mid-2026). The paper states this is the first formalisation challenge of its kind for contemporary pure mathematics research.

2. A documented selection and difficulty-rating methodology. All 207 papers in that volume range (excluding retractions, errata and corrigenda) were read and triaged, and each was assigned a difficulty rating from 1 to 5 reflecting how hard it would be to formalise the statement given the current state of Mathlib. 50 papers were then formalised, spanning many subject areas.

3. A two-stage verification pipeline. Every formalisation received an in-depth manual review by mathematicians, followed by multiple AI audits (Claude Fable 5 (Max Effort), then GPT 5.6 Sol Ultra, then Claude Fable 5 (Max Effort) again) using a prompt written to hunt for misformalisations.

4. A public release linked to a live leaderboard. The dataset was released on GitHub and integrated into LeanEval, a public benchmark and leaderboard where submitted proofs are checked for correctness without additional axioms in a sandboxed environment.

Main Findings

• Coverage: The 50 formalised papers represent a quarter of the 207 papers published in the relevant volumes (the subject-area table gives the total as 24.2%).
• Difficulty distribution: Of the 207 triaged papers, 40 were rated difficulty 1 (36 formalised), 37 rated 2 (11 formalised), 56 rated 3 (3 formalised), 44 rated 4 (0 formalised) and 30 rated 5 (0 formalised). A low rating does not imply an easy theorem — several included theorems have elementary statements but proofs depending on the classification of finite simple groups, whose proof spans over ten thousand pages and has not been formalised to date.
• Subject-area coverage (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%; Topological groups, Lie groups 16 / 0 / 0.0%; Several complex variables and analytic spaces 15 / 2 / 13.3%; Probability theory and stochastic processes 14 / 4 / 28.6%; Combinatorics 13 / 8 / 61.5%; Convex and discrete geometry 10 / 6 / 60.0%; Manifolds and cell complexes 10 / 2 / 20.0%; Other 17 / 5 / 29.4%; Total 207 / 50 / 24.2%.
• AI audit outcomes: For 32 of the papers the audit found no issues of mathematical significance; for 7 it revealed missing (mostly trivial) assumptions in the published paper whose absence made the theorem false; for the remaining 11 it revealed mistakes in the project's own formalisation. All identified issues were fixed before public release, and no further misformalisations have been found since release.
• Autoformalisation results (LeanEval, as of 2 October 2026; live since 17 August 2026): 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%). Accepted formal proofs had been submitted for 40 of the 50 challenges. These are independent community submissions, not a controlled evaluation — compute budgets, numbers of attempts, human involvement and access to the source papers were not standardised across submitters.
• Success by difficulty: Autoformalisation succeeded on 28 of the 36 difficulty-level-1 papers, on all 11 difficulty-level-2 papers, and on one of the three difficulty-level-3 papers. The paper notes that the difficulty of the proofs varies widely and may be uncorrelated with the difficulty of formalising the statement.
• Implicit conventions are a real obstacle: Mathematical practice in some areas relies on conventions clear to experts but not explicit — for example implicit measurability or regularity assumptions, or ambiguity in whether the Fourier transform is function- or distribution-valued, or whether a "solution" to a PDE means a classical solution or one of various notions of weak solution.
• What Mathlib still cannot state: Theorems about symplectic geometry, Riemannian geometry, Kähler geometry, Lie theory, intersection theory, infinity categories, moduli stacks, automorphic representations and Shimura varieties are described as often essentially impossible to even state right now.
• A comparison point on misformalisation difficulty: As of 2 October 2026, the FormalConjectures repository contains 3,604 formalised statements and has had 511 misformalisation fixes merged.

Methodology in Plain English

The team first read every paper published in Annals of Mathematics volumes 191–203, excluding retractions, errata and corrigenda — 207 papers in total — identified each paper's main result or results, and rated how hard it would be to formalise the statement with Mathlib as it stands. They then formalised the easiest statements first while deliberately aiming for wide subject-area coverage, writing the statements by hand in Lean 4 over the course of ten months.

Mathlib was the only dependency. Where new definitions were needed, they either added them to Mathlib during the project or, in rare cases where a definition was paper-specific and of no broader interest, developed it locally. Statements were kept as close to their natural-language form as possible, preserving the generality, naming conventions and notation of the original papers.

Three principles guided the work: trust (use Mathlib's community-reviewed definitions where possible), faithfulness (stay as close as possible to the informal source), and correctness (where the informal statement had gaps or was incorrect, correct it to match the author's presumed intent — asking the authors directly when the intention was unclear).

After each statement was formalised, a manual review checked for incorrect edge cases, inconsistencies with the paper, missing hypotheses, and interpretive errors. The reviewing team included mathematicians with expertise across a range of fields and prior experience with Lean formalisation. Only then did multiple AI audits run on each file, searching for subtle misformalisations — the prompt explicitly asked the auditor not to fill in the unfinished proofs but to look for special-case counterexamples or simpler proofs/disproofs that would signal a misformalisation. Findings were reviewed manually and all identified issues fixed before release.

Why This Matters

Impact on research. The paper argues that Mathlib is beginning to be ready for research-level mathematics — fifty recent main results could be stated on top of it, even though the difficulty distribution shows how much remains out of reach. Within weeks of release, more than half of the statements had a formalised proof submitted to LeanEval, which the authors read as strong interest and as an indication that autoformalisation will play an important role in how mathematics is reviewed in the future. The dataset also feeds back into Mathlib by prompting missing definitions and theorems.

Real-world applications:

• Benchmarking AI reasoning systems: Provides a hard, trustworthy yardstick for measuring autoformalisation progress, complementing competition-based datasets such as miniF2F (AMC, AIME and IMO problems), FIMO (IMO shortlisted problems) and PutnamBench.
• Proof-checking infrastructure: The LeanEval integration checks submitted proofs for correctness without additional axioms in a sandboxed environment, giving an automated, ungameable pass/fail signal.
• Library development for mathematics: Formalising statements exposes exactly which definitions and theories Mathlib lacks, guiding where library-building effort should go.
• Quality control on published mathematics: The audit surfaced missing hypotheses and typos in published Annals theorems, demonstrating that formalisation can catch errors in the human literature.

Industry relevance. The dataset is a public benchmark and leaderboard (LeanEval) that AI labs and companies can be evaluated against, and the leaderboard already lists entries from several model/harness teams. It also sits within a funding and tooling ecosystem — the project is funded by Renaissance Philanthropy's 2025 AI for Math Fund, with XTX Markets as founding donor of the fund — reflecting commercial and philanthropic interest in AI-driven mathematical reasoning.

Future Directions

• Formalise the remaining 157 papers. The paper names this as the natural next goal but warns it is not as easy as it sounds, because Mathlib is still missing many fundamental definitions and theories; getting the relevant mathematics into Mathlib will be a long process.
• Build out underrepresented areas. The authors want to state more theorems, especially in the areas underrepresented in their subject-area table — several of which are barely covered by Mathlib, so the library would need to be built out first.
• Scale up with AI, carefully. One proposal is to scale by relying on definitions from Tau Ceti, described as an AI-managed library, while insisting that every definition still receives careful review or the dataset would lose its trustworthiness.
• Extend beyond a single journal. A third direction is to cover other journals, whose subject balance differs from that of the Annals of Mathematics.

Target Audience

AI researchers working on autoformalisation, automated theorem proving and mathematical reasoning benchmarks; Lean and Mathlib contributors and formalisation practitioners; and research mathematicians interested in how contemporary pure mathematics can be stated formally. It is also relevant to research funders and industry teams evaluating AI systems on genuinely hard, trustworthy mathematical tasks. Because of the advanced Lean and research-mathematics content, it is not beginner-friendly.

Authors’ 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.