# A dataset of formalised theorem statements from the Annals of Mathematics

arXiv: https://arxiv.org/abs/2610.18301 · HTML: https://mlsanity.com/paper/2610.18301/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 23 references that are in the map.
- First posted on arXiv 13 Oct 2026.

## Builds on (most cited first, 7 of 7)

- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics](https://mlsanity.com/paper/2505.03171/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)

## Abstract (arXiv)

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.