Epoch AI 发布 FrontierMath Erdős：68 个开放 Erdős 问题全部形式化为 Lean，并采用固定预算机器可验证评测

Epoch AI 于 9 月 1 日正式发布 FrontierMath Erdős，由 Thomas Bloom 参与筛选 68 个截至 2026 年 8 月仍开放、具有较高数学意义和难度的 Erdős 问题。所有题目都被形式化为 Lean statement，AI 系统必须在固定预算内提交完整 Lean proof 或 disproof 才算解决；公开 benchmark 页面同时提供 methodology、Lean statements 与 evaluation scaffold，以改善此前开放数学问题评测中存在的 curation、verification 与 replicability 问题。