A dataset of formalised theorem statements from the Annals of Mathematics
arXiv:2610.18301
Abstract
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.
arXiv commentAccepted at AI-MATH@NeurIPS, the 6th workshop on mathematical reasoning and AI, NeurIPS 2026