Paper · arXiv
A dataset of formalised theorem statements from the Annals of Mathematics
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.
| Authors | Thomas Browning, Katerina Hristova, David Ledvinka et al. |
|---|---|
| Primary category | cs.AI |
| Published | 13 October 2026 |
| Last updated at source | 13 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 15 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.