A dataset of formalised theorem statements from the Annals of Mathematics

Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su +2

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.