2026 年 10 月初，集合论学者 Asaf Karagila 的邮箱被同行塞满了。大家都在追问他当年立誓送给百年难题分割原则破解者的那瓶威士忌，到底打不打算寄给 Sam Altman。几乎同时，为巴内特猜想倾注 24 年心血的图论研究者 Jake Boggan 在 Hacker News 留下叹息，形容自己看到 OpenAI 开源库第 180 号问题标着已获证明时，像在车祸里骤然失去了旧爱。
人类数学家还没来得及消化存在主义的悲凉，代码本身先露了馅。翻开 GitHub 上的 BarnetteHamiltonian.lean，核心主定理结尾赫然写着 sorry——在 Lean 定理证明器里，这四个字母专门用来跳过未完成的推导。不到三周后的 10 月 26 日，遭遇学界反弹的 OpenAI 紧急调转船头，不再批发倾倒手稿，而是精选出理论计算机、基础数学和理论物理 3 项重磅证明，并请来 2004 年诺贝尔物理学奖得主 David Gross 等外部顶尖学者担任牧羊人独立把关。
从月初狂撒 700 多篇半成品，到月末毕恭毕敬请人类泰斗逐行审稿，OpenAI 这记急转弯把 AI 冲击基础科学的真实现状摊在了桌面上。目前最卡脖子的早已不是推理算力，而是没人敢直接相信机器写出的结论。
-- OpenAI BarnetteHamiltonian.lean 核心片段
theorem barnette_conjecture (G : Graph) [PlanarEmbedding G]
[Bipartite G] [ThreeRegular G] [ThreeConnected G] :
HasHamiltonianCycle G := by
sorry三项新证明的清单与边界
为了挽回 10 月初批发未审手稿造成的声誉危机，OpenAI 在 10 月 26 日抛出的三项新成果采取了截然不同的公开与审查策略：
- 理论计算机科学（推翻指数时间假说 ETH）。针对布尔可满足性问题（SAT，仅 100 个变量就有 31 位数种可能组合），ETH 假说认为最坏情况下不存在亚指数时间的捷径。OpenAI 声称其 AI 给出了一个确定性算法，能在 $2^{O(n (\log \log n) / \sqrt{\log n})}$ 时间内精确计算固定宽度 CNF 公式的满足赋值数量，从而证伪 ETH。目前自然语言论文与 Lean 证明已开源，由 ETH 原始提出者 Russell Impagliazzo、Ramamohan Paturi 以及 MIT 教授 Ryan Williams 组成三人小组，在不签保密协议、不拿报酬、不代表背书的前提下公开审查。
- 基础数学（证明全维度波局部平滑猜想）。针对 Christopher Sogge 于 1991 年提出的猜想（人类学者仅在 2019 年证明二维情况），OpenAI 声称在任意维度下完成了证明，并直接导出几何学中的 Kakeya 猜想（人类直到 2025 年才证明三维情况）与傅里叶分析中的 Stein 限制猜想在全维度成立。该项未设专职审查组，论文与 Lean 代码已直接公开。
- 理论物理（四维相互作用量子场论的存在性）。试图为纯 Yang-Mills 理论、量子色动力学（QCD）及最简大统一理论在四维时空补上严格数学地基。这踩中了克雷数学研究所七大千禧年大奖难题之一（奖金 100 万美元）的前半部分，但 OpenAI 明确表示未解决后半部分的质量间隙（mass gap）。该项材料暂未公开，由诺奖得主 David Gross 领衔，联合千禧年难题起草人之一的 Arthur Jaffe、Michael Douglas、Igor Klebanov 和 Nikita Nekrasov 共五位学者闭门核查并亲自改写。
即便推翻 ETH 的证明完全成立，P vs NP 问题依然没有解决，现代密码学也不会一夜崩塌。ETH 倒塌只代表 SAT 问题进入亚指数时间（SUBEXP），并未进入多项式时间（P），且亚指数算法无法通过归约自动传递给所有 NP 问题。
真正受冲击的是理论计算机学界。过去几十年里，数百篇图论、计算生物学和数据库论文都把假设 ETH 成立当作算法无法再快的地基，一旦地基抽走，这批论文便失去了严密性。而在工业界，芯片设计与软件测试常用的工业级 SAT 求解器平时处理的本就不是最坏情况，早已能应对数百万个变量，未来一年内未必会因此产生波澜。
编译通过的假象与缩水的定义
为什么机器已经用 Lean 语言逐行检查过逻辑，还要劳驾诺奖得主和假说提出者人工审查？因为形式化验证有一个致命盲区，Lean 只能保证从前提到结论的推导没有漏洞，却无法保证代码里写的数学定义真的对应人类原本想解决的问题。
回看 AI 推理在学术领域的进路，这里横亘着两条路线。DeepMind 的 AlphaProof 在 2024 年国际数学奥林匹克中解出 6 题中的 4 题，拿到 28 分银牌水平，或是 Anthropic 在 11 天内用 1300 万行代码完成费马大定理端到端形式化，都是在人类已知边界的题目里做严格闭环。OpenAI 则直接跳进了无人知晓答案的开放深水区。
在 GitHub 的 openai/math 仓库里，OpenAI 月初用内部未公开模型一口气覆盖约 4000 个开放数学问题，抛出 722 篇手稿（10 月 6 日批次统计为 719 篇），分属 372 个结果族。独立审计项目 MathVet 随后对这批材料做了预审，揭开了形式化代码背后的猫腻：在 242 个附带 Lean 代码的项目里，只有 149 个真正完整陈述了论文标题宣称的定理，另外 93 个项目实际上只证明了更窄、更弱的特例或辅助引理。
这种代码编译通过、命题暗中缩水的错位，在 10 月 26 日推翻 ETH 的新材料里也能抓到现行。对比 OpenAI 在 GitHub 公开的两份文件，其 10 月 25 日的自然语言手稿宣称算法时间界限是 $2^{O(n (\log \log n) / \sqrt{\log n})}$，但配套的 Lean 范围文档实际形式化的界限，却多带了一个 $(\log \log n)^2$ 的额外弱化因子。更早的 9 月 8 日，OpenAI 宣称用 Lean 解决千禧年难题 Navier-Stokes 方程的特定表述，同样被学界发现加了平滑外力的限定条件，偏离了原始问题的核心困难，甚至在早期合作中闹出要求数学家剔除 Anthropic 共同作者的风波。
到了月初的第 244 家族分割原则证明里，这种不对称更是被推向极端。分割原则由 Bernstein 与 Beppo Levi 在 1901 至 1902 年提出，人类学者 Frank Gilson 刚在 2026 年 9 月因拓扑构造缺陷撤回论文。OpenAI 抛出的自然语言手稿被 Karagila 斥为达到初审拒稿水准，引理荒唐且生硬搬用未审阅的教学讲义；而附带的 Lean 代码虽然宣称编译通过，行数却庞大到常人无法肉眼核查。只要底层定义存在平凡化漏洞，机器就会在错误的跑道上算出一堆毫无价值的正确。
当顶尖学者沦为机器的语义审计员
我更在意的是这背后的权力关系倒置。从 8 月发布 10 项进展、10 月初倾倒 700 多篇手稿，到 10 月底精选 3 项成果请学者当牧羊人，OpenAI 甚至向西蒙斯基金会捐出 500 万美元资助 AI 成果研讨会，并主动声明放弃科学发现的署名功劳。
它不得不退让。因为月初那批手稿直接触发了针对数学界的拒绝服务攻击。OpenAI 在自己的 GPT-5 科学报告里都承认，AI 有时会直接重现人类已发表的证明却不标注原始文献归属。商业公司甩出一批语焉不详的预印本成本极低，转头就能收获舆论红利；但甄别真伪、核对文献、排查定义偷工减料的核查债务，全盘压在了人数有限的基础学科学者肩上。数学家们不得不停下手头的研究，去给估值几千亿美元的商业机构当免费的数据清洗工；若是不理会，资助方又会误以为机器早已解决一切，进而挤压基础学科经费。
韩非子讲过，循名实而定是非，因参验而审言辞。检验真伪不能只看言辞内部能不能自圆其说，必须核对宣称的标题（名）与底层的定义（实）是否一致。机器消灭了推导步骤里的低级算错，却把造假和缩水藏进了定义层。在今天的 AI 科研里，Lean 编译器只管审言辞，而循名实的苦差事全落在了人类学者头上。
这在物理学里尤为凶险。纯数学和计算机科学处理的是人造符号，尚且会溜进 $(\log \log n)^2$ 这样的界限弱化；到了量子场论里，即便 AI 在某个网格近似模型上用 Lean 证出了定理，这个数学模型的边界条件和连续性假设到底符不符合真实物理世界，机器根本无从判断。所以 David Gross 领衔的五人物理小组干脆扣下了 AI 的原始材料，决定自己重新撰写论文。
当年佩雷尔曼把庞加莱猜想的证明扔在预印本网站上，同行也花了数年去补全细节，但佩雷尔曼的论文带着人类心智清晰的几何直觉，那是真正的学术对话。OpenAI 丢出来的则是外壳光鲜的自然语言文本，内里塞着尚未闭合的 sorry、暗中弱化的定义和不可读的形式化碎片，买椟还珠，莫过如此。
把署名功劳让给牧羊人，算是一次聪明的公关止损，但代价远没有结算完。接下来最值得盯紧的指标有三个：一是 OpenAI 能不能把 180 号问题里那行刺眼的 sorry 从内核里彻底抹掉；二是 Impagliazzo、Paturi 和 Williams 三人小组针对 ETH 证明的审查报告，看那个多出来的 $(\log \log n)^2$ 因子之外还有没有定义漏洞；三是看 David Gross 团队最终会不会公开并认可那份量子场论证明。
在这几份人工审计报告落地之前，Karagila 的威士忌不必开封，学者们也无须为旧爱过早哀悼。