A dataset of formalised theorem statements from the Annals of Mathematics
Not on the map. Why?
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.
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
7 of 23 references.
References · 7
- 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
- 2026Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMscited by 137
- 2019The Lean mathematical librarycited by 134
- 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 31
- 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 27
- 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 10
- 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?cited by 8
Built on by
Not cited yet.