AnnalsChallenge形式化定理数据集发布

2026年10月14日，arXiv Artificial Intelligence 刊出报道，研究者发布 AnnalsChallenge，一个包含 50 条用 Lean 4 和 Mathlib 手工形式化的定理语句数据集，每条对应 2020 年以来发表于《数学年刊》的论文主要结果。报道称，所有形式化均经人工复核并由 AI 审计，数据集不含形式化证明，已被 NeurIPS 2026 的 AI-MATH 研讨会接收。该数据集以 Thomas Browning 等作者名义发布，来源明确说明“We release them without formalised proofs.”，即仅提供定理语句而不含证明。目前进展为数据集已公开并获研讨会接收，尚无后续跟进报道。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。