Summary (Overview)

• ANNALSCHALLENGE is a novel dataset of 50 formalised theorem statements written in Lean 4 using Mathlib, each representing the main result of a paper published in the Annals of Mathematics (volumes 191–203, 2020–2026).
• The dataset covers 50 out of 207 papers (24.2%) from this period, spanning 13 subject areas, with notable coverage in combinatorics (61.5%), convex/discrete geometry (60.0%), number theory (40.0%), and group theory (40.0%).
• The formalisations were manually written over ten months, then reviewed by human experts and audited by multiple AI systems (Claude Fable 5 and GPT 5.6 Sol Ultra) to ensure correctness and faithfulness to the original papers.
• Within weeks of release on LEANEVAL, community submissions produced accepted formal proofs for 40 of the 50 statements (80%), demonstrating strong interest and the rapid progress of AI autoformalisation.
• The dataset is designed to serve three purposes: assessing Mathlib's readiness for contemporary research mathematics, enriching Mathlib with missing definitions, and benchmarking AI autoformalisation of existing proofs.

Introduction and Theoretical Foundation

The paper addresses the challenge of measuring progress in autoformalisation—the automated translation of informal mathematical statements and proofs into formal, machine-checkable language. Recent advances in AI have made this field increasingly promising, but measuring progress requires datasets that are both hard (reflecting real research-level mathematics) and trustworthy (formalisations that faithfully represent the original statements).

The authors position ANNALSCHALLENGE against existing datasets:

• Competition-based: miniF2F (Olympiad problems), FIMO (IMO shortlisted problems), PutnamBench (Putnam Competition)—these are at undergraduate or high-school level.
• Undergraduate-level: FormalMATH, ProofNet.
• Domain-specific: CombiBench (combinatorics), FATE (algebra)—these focus on single areas.
• Research-level: ArXivLean (extracts statements from abstracts), FormalConjectures (open problems), SorryDB (gaps in existing Lean projects).

ANNALSCHALLENGE is distinct as the first formalisation challenge for contemporary pure mathematics research spanning multiple areas, drawing from one of the most prestigious mathematics journals. The key innovation is its focus on the statements of theorems (not proofs), which allows the dataset to test whether modern research mathematics can even be expressed in existing formal systems, independent of the difficulty of proving.

Methodology

Design Principles

The dataset is built on three core principles:

1. Trust: Use Mathlib definitions whenever possible (community-reviewed); local definitions are carefully reviewed by humans and AI.
2. Faithfulness: The formalised statement should be as close as possible to the informal source.
3. Correctness: When the informal statement has gaps or errors, correct it to match the author's presumed intent; when unclear, consult the authors directly.

Statement Selection Process

The authors triaged all 207 papers (excluding retractions, errata, corrigenda) from volumes 191–203:

• Each paper was read, and the main result(s) identified.
• A difficulty rating from 1 to 5 was assigned, reflecting the difficulty of formalising the statement (not proving it) given the current state of Mathlib:
  • 1: Formalised directly with existing Mathlib definitions.
  • 5: Requires definitions that would be a major research project to formalise.

Table 1: Distribution of papers by estimated difficulty

Formalisation Philosophy

• Statements were formalised manually over ten months.
• Mathlib was the only dependency; new definitions were added to Mathlib where of broader interest, or developed locally for paper-specific cases.
• The formalisations preserve the generality, naming conventions, and notation of the original papers.

Manual Review

In-depth review checked for: incorrect edge cases, inconsistencies with the paper, missing hypotheses, and interpretation errors. The team included mathematicians with expertise across fields and Lean experience. In cases where the paper itself had issues (typically missing implicit hypotheses), the authors of the original papers were consulted.

AI Audit

After manual formalisation, multiple AI audits were run on each file:

1. Claude Fable 5 (Max Effort)
2. GPT 5.6 Sol Ultra
3. Claude Fable 5 (Max Effort) again

Results of the audit:

• 32 papers: No issues of mathematical significance found.
• 7 papers: The AI revealed missing (mostly trivial) assumptions in the original papers making the theorem false as stated.
• 11 papers: The AI revealed mistakes in the formalisation itself, which were fixed after manual review.

Empirical Validation / Results

Subject Area Coverage

Table 2: Subject-area coverage (papers may belong to more than one area)

Autoformalisation Results on LEANEVAL

Table 3: Accepted community proof submissions as of 2 October 2026

Success breakdown by statement difficulty: 28/36 difficulty-1 papers, 11/11 difficulty-2 papers, and 1/3 difficulty-3 papers. Note that these results come from independent community submissions rather than controlled evaluations—compute budgets, attempts, human involvement, and access to source papers were not standardised.

Theoretical and Practical Implications

Lessons from Formalisation

The authors discovered that mathematical practice in some areas makes formalisation harder than expected:

• Authors often write with implicit conventions clear to experts but not explicitly stated (e.g., measurability of functions/sets).
• Ambiguous definitions such as the Fourier transform (explicit function vs. distribution-valued) or "solution of a PDE" (classical vs. various weak solutions) require careful interpretation.
• These issues highlight a gap between informal mathematical practice and the precision required for formalisation.

State of Mathlib

The dataset reveals both progress and gaps:

• Progress: Mathlib is "beginning to be ready" for research-level mathematics—50 recent main results could be stated.
• Gaps: Many fundamental theories are still missing, making statements essentially impossible to even express, including:
  • Symplectic geometry
  • Riemannian geometry
  • Kähler geometry
  • Lie theory
  • Intersection theory
  • Infinity categories
  • Moduli stacks
  • Automorphic representations
  • Shimura varieties

Trustworthiness Challenge

Misformalisation is a known difficulty in this space. For context, the FormalConjectures repository (3,604 statements) has had 511 misformalisation fixes merged—highlighting the importance of the rigorous human + AI review process used here.

Conclusion

Main Takeaways

1. ANNALSCHALLENGE provides a novel, trustworthy benchmark for research-level mathematics formalisation, covering a broad range of subject areas.
2. Mathlib is making real progress toward supporting contemporary research mathematics, though much remains out of reach.
3. The rapid community response (80% of statements proved within weeks) signals strong interest and suggests autoformalisation will play an important role in the future of mathematical review and verification.

Future Directions

The authors identify three directions:

1. State more theorems, especially in underrepresented areas (topological groups, Lie groups, PDEs, differential geometry). This would require building out Mathlib first, as several areas are barely covered.
2. Scale up with AI, for instance using definitions from Tau Ceti (an AI-managed library). Every definition would still need careful review to maintain trustworthiness.
3. Cover other journals whose subject balance differs from that of the Annals of Mathematics.

The paper positions ANNALSCHALLENGE as a living resource—released on GitHub and LEANEVAL—that will continue to evolve as Mathlib grows and AI autoformalisation capabilities advance.