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 研讨会接收。
正文 · 原文
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