A dataset of formalised theorem statements from the Annals of Mathematics

2026-10-15 · ArXiv

arXiv:2610.18301v1 Announce Type: new

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.

原文链接：https://arxiv.org/abs/2610.18301

查看更多资讯请见 AI 行业资讯。