arXiv cs.AI· Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard·· 3 天前AI 评分24
AnnalsChallenge：来自《数学年刊》的 50 条 Lean 4 形式化定理陈述数据集
A dataset of formalised theorem statements from the Annals of Mathematics
AI 导读
研究者发布 AnnalsChallenge，包含 50 条用 Lean 4 和 Mathlib 手工形式化的定理陈述，每条均为 2020 年以来发表于《数学年刊》论文的主要结果。所有形式化均经人工审核并由 AI 审计，数据集不含形式化证明，已被 NeurIPS 2026 的 AI-MATH 研讨会接收。
正文 · AI 翻译
摘要：近期利用 AI 进行数学自动形式化的进展令人瞩目。衡量这一进展需要既困难又可信的形式化陈述数据集。我们提出 AnnalsChallenge：50 条用 Lean 4 结合 Mathlib 手工编写的形式化定理陈述。每一条都是 2020 年以来发表在《数学年刊》上的一篇论文的主要结果。每个形式化都经过人工审查，随后由 AI 审计。我们发布这些内容时不附带形式化证明。
| 评论： | 已被 AI-MATH@NeurIPS 接收，第六届数学推理与 AI 研讨会，NeurIPS 2026 |
| 主题： | 人工智能（cs.AI） |
| MSC 分类： | 68V20（主），68V15（次） |
| ACM 分类： | I.2.3 |
| 引用为： | arXiv:2610.18301 [cs.AI] |
| （或 arXiv:2610.18301v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.18301 arXiv 颁发的 DOI，经由 DataCite（待注册） |
提交历史
发件人：Kevin Buzzard [查看电子邮件]
[v1]
2026年10月13日星期二 12:48:33 UTC（16 KB）
来源：arXiv cs.AI · arxiv.org