Research
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 ar
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.
Related
- From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
- FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization
- What is mathematics now, and what should it be?
Source: arXiv cs.AI | 2026-10-15