AI 连破三大数学猜想：Jacobian 猜想 87 年反例与形式化验证的新时代

AI 连破三大数学猜想：从反证法看 2026 年的形式化数学革命

2026 年 7 月 20 日，世界杯决赛正踢得胶着。数学家 Levent Alpöge 发了一条推文——Claude Fable 找到了 Jacobian 猜想的一个反例。87 年的公开问题，反例只有一行多项式。

同一天，剑桥数学家 Kevin Buzzard 在博客上写了一篇长文，标题是 "Human mathematicians are being outcounterexampled"（人类数学家正在被反超）。他整理了两个月内发生的三件事：

• 5 月 20 日：ChatGPT 构造了 Erdős 单位距离猜想的反例
• 7 月 11 日：OpenAI Sol 找到了 Grothendieck 关于群概形问题的反例
• 7 月 20 日：Claude Fable 找到了 Jacobian 猜想的反例

三个问题跨度从离散几何到代数几何，从 40 年到 87 年。AI 没有用暴力搜索——它理解了问题结构，然后构造了一个精确的反例。

Jacobian 猜想：87 年，一行公式

Jacobian 猜想由 Ott-Heinrich Keller 于 1939 年提出，是代数几何中最著名的未解问题之一。其核心命题是：如果一个多项式映射的 Jacobian 行列式是非零常数，那么这个映射一定有多项式逆。

换句话说：一个看起来"可逆"的多项式映射，必定真的可逆。

Alpöge 和 Fable 构造的反例是一个 C³ → C³ 的多项式映射，其 Jacobian 行列式为常数 -2，但它将三个不同的点映射到同一个点。这意味着该映射不可逆，猜想在三维以上不成立。

反例的具体公式可以在 Alpöge 的推文中找到。ulam.ai 网站随后发布了一篇详细论文，给出了代数验证和全局几何分析。论文指出，这个反例并未解决二维版本的猜想——proper Keller 映射仍然是自同构。Jelonek 定理表明，要证明二维情况，只需要证明渐近值集的余维至少为 2。

Paul Lezeau 在 Alpöge 公布反例后数小时内，手动将其形式化并提交了 Pull Request 到 DeepMind 的 Formal Conjectures 仓库。这个仓库维护了大量数学猜想的 Lean 形式化版本——一旦人类就猜想的形式化表述达成共识，验证 AI 生成的证明或反例就变成了机械检查。

从 Erdős 到 Grothendieck：反例的进阶之路

两个月前的事件链条同样值得关注。

Erdős 单位距离猜想认为，平面上 n 个点最多能形成 O(n^(1+c/log n)) 个单位距离对。ChatGPT 用 Golod-Shafarevich 定理（1960 年代的一个深刻数论结果）构造了反例。OpenAI 公布后，Logical Intelligence（由图灵奖得主 Yann LeCun 联合创立）的系统在不到一周内将整个证明自动形式化为 Lean 代码。

一个月后，OpenAI 的 Boris Alexeev 用新的 Sol 模型完成了 Erdős 反例的完全形式化——从数学公理出发，不需要任何额外假设。Sol 在三周内生成了 120 万行 Lean 代码。作为参照，Lean 的数学库 mathlib 用了九年才积累到 230 万行。

Grothendieck 的反例则发生在 7 月。UChicago 教授 Akhil Mathew 在 Imperial College 的 FLT（Fermat 大定理形式化）工作坊期间，让 Sol 尝试解决 Grothendieck 提出的关于有限自由群概形的问题：序为 n 的有限自由群概形是否被 n 零化。Sol 找到了一个 1076 行的 Lean 形式化反例——一个序为 4 的群概形不被 4 零化。

Buzzard 在验证时特意检查了代码不会删除硬盘文件（Lean 是编程语言，恶意代码可以执行任意命令），确认后编译运行，五分钟内完成了验证。

形式化验证：为什么这很重要

这三个反例的共同点是：它们都被形式化为 Lean 代码并通过了编译检查。

传统数学论文的同行评审依赖于人类专家的阅读和理解。但对于高度技术性的证明——比如涉及全局类域论的 Erdős 反例——即使是领域专家也可能遗漏错误。形式化将证明转化为机器可检查的代码，消除了"人类看漏了"的可能性。

Buzzard 对此的态度很明确：他拒绝阅读任何未经形式化的 AI 生成的非正式数学。"I was not reading AI-generated informal mathematics and could he please formalize the entire thing in Lean." 四小时后，Akhil 用 Fable 完成了自动形式化。

形式化的另一个优势是可组合性。DeepMind 的 Formal Conjectures 仓库、Lean 社区的 mathlib 库，以及 Logical Intelligence、Logos Research、Harmonic、Axiom AI 等多家公司的自动形式化工具，正在构建一个共享的形式化基础设施。一旦猜想被形式化表述，任何工具找到的证明或反例都可以被独立验证。

更大的图景：250K 行代码与 $200/月

Buzzard 的博客还透露了一个更广泛的趋势：AI 辅助数学研究正在加速。

他的博士生 Andrew Yang 在获得 Sol 和 Fable 访问权限后的两周内，写了 25 万行 Lean 代码，基本完成了模形式提升定理的形式化——这是 Buzzard 正在进行的 Fermat 大定理形式化工作的关键组成部分。

当一位同事对研究生每月花 $200 订阅 Sol 和 Fable 表示不解时，Buzzard 回复说："任何不花 $200 订阅这些工具的博士生才是不理性的。" 他了解到 Harvard 已经开始为所有博士生、博士后和教师提供免费的 Fable 访问。

这个趋势的意义在于：AI 正在改变数学研究的速度。传统上，一个 PhD 学生可能需要数月甚至数年来形式化一个中等复杂度的定理。现在，有了 AI 辅助，这个时间缩短到了数周。而反例的发现速度更快——从提出问题到找到反例，有时只需要几个小时。

AI 的策略：反例是低垂的果实

Buzzard 和 Mathew 观察到一个有趣的模式：AI 在寻找反例方面表现格外突出。这可能并非巧合。

反例的构造通常需要：

1. 深刻理解问题背后的代数或几何结构
2. 精确计算多项式或构造具体的数学对象
3. 验证构造满足反例所需的条件

AI 在第 2 和第 3 点上具有天然优势——它可以快速枚举和计算复杂表达式。而第 1 点，随着大语言模型对数学文献的掌握越来越深，也在快速改善。

Buzzard 甚至半开玩笑地建议 Mathew 下一个目标试试 Hodge 猜想。

反例之外：人类下一步做什么

找到反例只是第一步。以 Grothendieck 群概形问题为例，反例本身（1076 行 Lean）给出了"这不对"，但数学家真正需要的是"为什么不对"——理解反例背后的结构性洞察。

Mathew 正在从更深的层面分析 Grothendieck 反例，试图从中提取超越"一个随机的环表示和一个随机计算"的数学洞见。Jacobian 猜想的反例同样如此——ulam.ai 的论文已经开始分析其全局几何性质和构造机制的推广可能性。

AI 提供了原材料；人类的角色是从中提炼出新的数学理解。

2026 年夏天，AI 辅助数学研究进入了一个新阶段。三个重量级反例，形式化验证成为标配，多家 AI 公司竞逐自动形式化赛道。正如 Buzzard 所说——"What a time to be alive."