Epoch AI 发布 FrontierMath Erdős 基准：用 Lean 验证的 68 道未解 Erdős 问题评测 AI 数学能力

Epoch AI 发布 FrontierMath Erdős 基准，由 erdosproblems.com 创建者 Thomas Bloom 挑选 68 道截至 2026 年 8 月仍未解决的、兼具重要性与难度的 Erdős 问题，用 Lean 形式化验证（50 题来自 Google Formal Conjectures 项目），代码开源，每题默认推理预算 $300。