🔥 今日值得一读
68个未解数学难题，GPT-6 Astra仅解出3%，其他AI全军覆没！
FrontierMath Erd\H{o}s
📖 AI 总结
本文介绍了一个名为 FrontierMath Erdős（FME）的新基准测试，由 Epoch AI 的 Tom Adamczewski 与曼彻斯特大学的 Thomas F. Bloom 共同提出。该基准包含 68 个截至 2026 年 8 月仍未解决的 Erdős 数学问题，从 652 个开放问题中依据数学价值与难度筛选而来。AI 系统需在 Lean 证明助手中自主完成证明或反证。研究团队以每个问题 300 美元的统一预算，对五个 AI 模型进行了评估。结果显示，仅 GPT-6 Astra 取得 3% 的解决率，其余模型均为 0%。该工作针对此前 AI 解决开放数学问题多为个案展示、缺乏系统评估的不足，提供了统一、可复现的评测框架，为衡量 AI 在高等数学推理上的真实能力提供了重要参照。
🔑 关键词速览
| FrontierMath Erdős (FME) | 一个包含 68 个未解决 Erdős 问题的基准测试，用于评估 AI 在 Lean 中证明或反驳猜想的能力。 |
| Erdős problems | 由数学家 Paul Erdős 提出的数学猜想，许多至今未解决，常涉及数论、组合数学等领域。 |
| Lean | 一种交互式定理证明器，用于形式化数学证明，确保推理的严谨性。 |
| proof assistant | 辅助用户构造和验证形式化数学证明的软件工具，如 Lean、Coq 等。 |
| conjecture | 数学中尚未被证明或反驳的命题，通常基于部分证据或直觉提出。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅