arXiv：cs.AI· Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard·· 6 小时前
AnnalsChallenge：50 条《数学年刊》定理的 Lean 4 形式化数据集发布
A dataset of formalised theorem statements from the Annals of Mathematics
AI 导读
研究者发布 AnnalsChallenge，包含 50 条用 Lean 4 与 Mathlib 手工形式化的定理陈述，每条对应 2020 年以来《数学年刊》论文的主要结果。所有形式化均经人工复核并由 AI 审计，且仅公开陈述、不附带形式化证明，用于衡量 AI 数学自动形式化的进展。该数据集已被 NeurIPS 2026 的 AI-MATH 研讨会接收。
正文
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.
| Comments: | Accepted at AI-MATH@NeurIPS, the 6th workshop on mathematical reasoning and AI, NeurIPS 2026 |
| Subjects: | Artificial Intelligence (cs.AI) |
| MSC classes: | 68V20 (Primary), 68V15 (Secondary) |
| ACM classes: | I.2.3 |
| Cite as: | arXiv:2610.18301 [cs.AI] |
| (or arXiv:2610.18301v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.18301 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Kevin Buzzard [view email]
[v1]
Tue, 13 Oct 2026 12:48:33 UTC (16 KB)
来源：arXiv：cs.AI · arxiv.org