arXiv · cs.AI· Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard·· 1 天前
AnnalsChallenge 发布《Annals of Mathematics》定理形式化数据集
A dataset of formalised theorem statements from the Annals of Mathematics
arXiv:2610.18301v1阅读论文 PDF ↗
仅依据论文摘要整理；未读取全文，实验条件、证明与基准细节请核对原文。
作者：Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard
研究任务与主要进展
Thomas Browning 等发布 AnnalsChallenge 数据集，包含 50 个由作者手工编写的 Lean 4 形式化定理陈述，使用 Mathlib，覆盖 2020 年以来发表于《Annals of Mathematics》论文的主要结果。每条形式化均经人工审查并由 AI 审计，但数据集不包含形式化证明。
阶段、条件与复现 · 深读核对
- 新能力对应什么具体任务与最小输入输出？
- 代码、模型、数据、许可与可用入口是否明确？
- 效果、总成本、失效条件与实际工作流如何验证？
这些是阅读核对问题；材料未说明的条件保留未知。请结合上方论文版本、资料范围与原文核验。
来源：arXiv · cs.AI · arxiv.org