陶哲轩钦点的”闭卷考试”，GPT-6 5道全对，Fable 5.1吃零蛋：AI数学的遮羞布被硬核撕了
AI飞行客 陶哲轩钦点的”闭卷考试”，GPT-6 5道全对，Fable 5.1吃零蛋：AI数学的遮羞布被硬核撕了
昨天聊了 GPT-6 Astra 把孪生素数上界从 246 推到 186，我当时说”这不是最重要的事”，更重要的是实时证明的范式跃迁。
结果今天就来了一个更加猛的、也更搞事的——Epoch AI 和曼彻斯特大学发布的 FrontierMath Erdős（FME）基准测试。
68道Erdős生前留下的未解数学猜想，5个顶级AI模型同场开考，Lean形式化验证，双容器隔离防作弊。
GPT-6 Astra 是全场唯一非零分的模型，拿下了 3%（68解2，追加后共5道）。
GPT-5.6 Sol、GPT-5.5、Claude Fable 5.1、Claude Fable 5——全部零分。
四个模型加起来，一道都没解出来。
—
这考试有多严？陶哲轩亲自压阵
你可能觉得”才3%有什么可吹的”。
那你得先看看这场考试是谁出的题、怎么监考的。
今年 ICM（国际数学家大会）上，陶哲轩亲自点名批评了此前所有”AI攻克数学猜想”的报道——说它们存在五个致命问题：
1. 只报成功不报失败，不知道成功率； 2. 算力消耗不公开； 3. 人类引导了多少不透明； 4. 训练数据很可能已经包含了答案； 5. 不同模型之间从未做过系统比较。
FME 就是对这五条批评的直接回应。
考题等于闭卷加防作弊：
– 68道题全是 Erdős 生前提出、至今没人解决过的开放猜想——模型不可能在训练数据里”背到”答案； – AI 必须用 Lean 形式化证明助手提交证明，由 Lean 内核做最终裁决——通过就是通过了，没通过就是没通过，没有”大模型式糊弄”的空间； – 所有模型完全相同条件：每道题预算 300 美元、72 小时、只能尝试一次； – 两个隔离的 Docker 容器，一个跑 Agent，一个跑 Lean 编译器——防篡改环境、防恶意代码、防定义偷换。
这不是高考，这是闭卷盖了钢印。
攻破的5道题，每一道都足够单独发顶刊
GPT-6 Astra 在标准测试中解出了 2 道，追加预算后又解出 3 道。
最值得单独说几嘴的：
第1号问题——反证（Erdős 18岁时的”第一个认真问题”）
1931年，18岁的 Erdős 提出了关于”解离集密集度”的猜想。GPT-6 Astra 用线性代数构造了反例，直接否定了这个持续了近百年的猜想。最低花费仅 47 美元/5 小时就跑了其中一次成功尝试，而且三种不同的论证方法都被发现了。
第548号问题——Erdős-Sós 猜想（1962年，极值图论最诱人问题之一）
这是 Erdős 和 Sós 联合提出的关于图与树包含关系的经典猜想。此前有大量特殊情形的部分成果，但一直没有完整证明。Astra 花了 363 美元/20 小时给出完整的归纳证明。
第571号问题——Turán 数增长阶猜想
Erdős 和 Simonovits 猜想极值图论中 Turán 数的增长阶可以取任何有理数 α∈[1,2)。Astra 给出了对任意有理 α 的完整证明。花费 617 美元/41 小时。Bloom（曼彻斯特大学教授，第二作者）说这是五个解中最难的一个——”对这个证明的完整人类理解，包括它与已有大量工作的关系，还需要一些时间。”
挖个重点：Bloom 说需要时间才能完全理解的那个证明，可能才是整场考试中最恐怖的部分。 人类评审员居然不能立刻看懂 Astra 的证明。
3% 的成绩：是 AI 太弱，还是考试太难？
现在可以回答那个问题了。3% 低不低？
68 道 Erdős 活着的时候都没解决的数学猜想，人类数学家面对同样的题目，正在参与这场考试的”对照组”——但到现在也没有任何一位人类数学家宣布解出了其中任何一道。
68道题中，有Erdős悬赏上万美元的题目，有一题Erdős到去世前都在追问改进，有被Bloom本人筛选为”任何一个被人类解决都值得发一篇顶刊”的硬骨头。
Astra 在 300 美元预算约束、72 小时时限、封闭容器、Lean 编译验证的条件下，从 68 道中解出了 2 道，花费不到 500 美元。
如果这是一个人类研究生，需要用多长时间？花多少钱？
那如果你的预算不是 300 美元，而是 Colleague 能负担的预算——零。如果允许模型无限尝试呢？
这说明不是 Astra 弱，是这道题的难度天花板本身极高。而 Astra 在极低预算下成为了第一个撞开那扇门的参赛者。
但 Kate 真正关心的是那个”验证悖论”
最后说一个今天几乎没有人在报道里提到的事。
Astra 解出的第 571 号问题（Turán数增长阶）——Bloom 说”对这个证明的完整人类理解还需要一些时间”。
当 AI 给出的证明，人类数学家需要”更多时间来理解”时——数学验证链出现了最深刻的分叉。
以前的情况是：AI 产出的证明，人类能够审查，Lean 能够验证。通常 Lean 验证更快。
现在的情况是：Astra 产出了一个 Bloom 确认 Lean 验证通过的、对任意有理α的完整证明，但 Bloom 说他需要更多时间来理解为什么这个论证是对的。
Lean 验证了形式正确性，但人类还没有完全理解证明的”数学直觉”。
这就产生了一个新的工种：数学口译员。
以前写证明是为了让人看懂；现在写证明是为了让 Lean 编译通过。如果未来 AI 数学推论的速度让人类审查员的”理解速度”不再是瓶颈，那数学学科的核心活动会不会从”解题”变成”把AI的解题思路翻译成人类可以理解的叙述形式”？
FME 的总花费：标准基准 + 追加尝试≈24 万美元。而它解出的 5 道题，任何一道被人类解出，都值得在顶刊上发一篇论文、花好几年的经费。
如果你问我：AGI 什么时候来？在数学家开始习惯说”这个证明是 AI 给的，Lean 通过了，但我还没完全看懂”的时候——那条线就已经过了。