Measuring progress in AI autoformalisation needs formal statement datasets that are both hard and trustworthy. Existing benchmarks focus on competition, undergraduate, or single-domain mathematics rather than contemporary research results.

The authors triaged all 207 Annals of Mathematics papers from volumes 191–203 by how hard it would be to state their main theorems in current Mathlib, rated on a scale of 1 to 5. They hand-formalised 50 main results in Lean 4 on top of Mathlib, adding missing definitions to Mathlib or, for paper-specific ones, defining them locally. Each statement was manually reviewed and audited by AI, and statements were corrected to match the authors' intent, sometimes after consulting those authors. The dataset was released on GitHub and on LeanEval without proofs, where submitted proofs are checked without extra axioms.

Most formalised statements came from difficulty levels 1–2, and coverage varies widely by subject area. Many fields remain unstatable because Mathlib lacks definitions in areas such as Riemannian geometry and Shimura varieties. In community submissions to LeanEval, which were not run under controlled conditions, proofs were accepted for 40 of the 50 statements; the best single system, Axiom Prover, accounted for all 40.