A dataset of formalised theorem statements from the Annals of Mathematics
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.
Fallback brief based on the available RSS feed; no unsupported details have been added.
Source: arXiv
Original article: https://arxiv.org/abs/2610.18301
Leave a Reply