FrontierMath Erdős

简介

FrontierMath Erdős 由 Epoch AI 与 Thomas Bloom 构建，收录 68 个截至 2026 年 8 月仍未解决的 Erdős 问题，全部用 Lean 4 形式化。模型以智能体方式运行（可用 bash、Lean/Mathlib、SageMath、Python 及离线数学文献库），每题一次尝试、预算上限 300 美元或 72 小时，必须写出能通过 Lean 检查的完整证明或反证。得分为解决的问题占比。