GPT-6 Astra 独解 5 道 Erdős 难题，68 题基准仅它非零分
量子位 · wechat · 2026-09-04
Epoch AI 与曼彻斯特大学发布 FrontierMath Erdős（FME）基准：68 道人类至今未解的 Erdős 数学难题，要求模型用 Lean 形式化证明作答。GPT-6 Astra 是五个顶级模型中唯一非零分者（3% 得分率），放宽预算后累计解开 5 道猜想，包括 Erdős 1931 年提出的第 1 号问题与 1962 年的 Erdős-Sós 猜想。
基准设计回应陶哲轩批评：此前 AI 数学成果被陶哲轩在国际数学家大会指出五大问题——成功率未知、算力不公开、人类引导不透明、可能数据污染、缺乏系统比较。FME 的对策：
- 只用未解问题消除「背答案」
- 提交 Lean 形式化证明，由 Lean 内核裁决
- 统一条件：每题 300 美元预算、72 小时、一次尝试
- 双 Docker 容器隔离验证，防范多种作弊手段
选题：由 erdosproblems.com 维护者 Bloom 从 652 个开放问题中挑选最难、最有数学意义的 68 题，且相互独立；50 题的 Lean 陈述取自 DeepMind 的 FormalConjectures 库。
成绩细节：标准测试解出 2 题（花费 218/247 美元、各约 15-16 小时）；追加尝试累计 5 题，其中第 126 号问题给出三种初等证明，最强结果达 |S(A)|≫n^{1/2}。全部尝试总花费超 22 万美元，按此估算解出一道重要开放问题期望成本约 1 万美元。
局限：形式化成本可能低估真实能力；基准只测解题，不测提出好问题的能力。68 题中仍有 63 题未解。
所属事件:Epoch AI 发布 FrontierMath Erdős，GPT-6 Astra 首破零分(10 条相关)→
「模型」频道最新
- 开发者实测:Gemini Argon 分析调试日志优于 Fable 5.1 — ShikharMurty · 2026-10-21
- 用户让 ChatGPT「尖叫」，它陷入无限循环 AAAAHHH 停不下来 — AutomaticScene · 2026-10-21
- 开源新模型 Ornith-1.5-122B 发布:SWE-bench 84.5%,单卡 DGX 可跑 — _akhaliq · 2026-10-21
- qev-0.8B:3.5毫秒决策、1.3GB本地跑的微型模型登顶 — fajfas3 · 2026-10-21
- Gemini 3.1 Pro 玩「两真一假」：bot 太沉迷账本，秒被识破谎言 — mimi10v3 · 2026-10-21
- 1.3B 开源模型 OXR 登顶三大文档解析榜，百页 101 秒 — aftahi_ai · 2026-10-21