arXiv Artificial Intelligence· Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, Jack McKoen, Kevin Buzzard·· 20 小时前AI 评分26
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 研讨会接收。
来源：arXiv Artificial Intelligence · arxiv.org