雅可比猜想被AI推翻——世界杯决赛夜，Fable一脚踢翻了85年的数学猜想

前言

世界杯决赛夜，一个数学家用AI聊天，顺手终结了一个85年的猜想。

2026年7月，Anthropic 研究员、哈佛前Junior Fellow Levent Alpöge 在 X 平台上发了一条推文——一个显式的多项式映射，雅可比行列式为常数 -2，却有三个不同的原像映射到同一个点。这意味着，雅可比猜想（Jacobian Conjecture）被证伪了。

Levent Alpöge 原始推文

更有趣的是，这个反例是他在世界杯决赛期间，随口问了一句 AI 模型 Fable，然后 Fable 就给他吐出来了。

thanks to my other close friend fable for working during the world cup final

“感谢我的好朋友 Fable，在世界杯决赛期间帮我干活。”

雅可比猜想：一个“大一就能听懂”的猜想

在数学界，大多数著名的未解问题——黎曼猜想、P vs NP，别说理解了，你连问题陈述都未必能读下来。但雅可比猜想是个异类。

猜想说了什么

雅可比猜想（1939年由 Ott-Heinrich Keller 提出，后经 Shreeram Abhyankar 推广）问的是这样一个问题：

如果一个多项式映射 F: \mathbb{C}^n \to \mathbb{C}^n 的雅可比行列式是一个非零常数，那么 F 是否一定有多项式逆映射？

用更直白的话说：在微积分里，如果一元函数的导数处处不为零，那它局部可逆。在多元情况下，如果雅可比行列式（导数的多元版本）是一个处处非零的常数，那这个多项式映射是否全局可逆，而且逆映射也是多项式？

这听起来非常“理所当然”。毕竟线性代数里，矩阵行列式非零就意味着可逆——这就是 Cramer 法则。雅可比猜想本质上是在问：Cramer 法则能不能推广到多项式？

为什么重要

这个猜想在数学界的分量不轻。它是 Steve Smale 列出的21世纪最重要的18个数学问题之一。更有意思的是，张益唐（就是那位证明了孪生素数猜想弱形式的传奇数学家）的博士论文，据说就是因为依赖了一个与雅可比猜想相关的错误引理而整个垮掉。我现在在知乎看相关问题都是在讨论张益唐 :)

反例：三行多项式，终结85年猜想

话不多说，直接上反例。定义多项式映射 F: \mathbb{C}^3 \to \mathbb{C}^3：

\begin{aligned}
F(x, y, z) = \bigl(
&(1+xy)^3 z + y^2 (1+xy) (4+3xy), \\
&y + 3x(1+xy)^2 z + 3 x y^2 (4+3xy), \\
&2x - 3x^2 y - x^3 z
\bigr)
\end{aligned}

就这三行。没有深层数论，没有无穷级数，没有抽象代数几何——就是三个你能在大一微积分作业里看到的多项式。

这个映射有两个关键性质：

第二条直接证伪：雅可比行列式为常数非零，但映射不可逆（因为不单射，不可能有多项式逆映射）。

手动验证——任何人都能算

说实话，这个反例最让我感动的不是它推翻了猜想，而是它的验证简单到任何人都能算。不像之前的单位距离猜想那样命题简单但完全看不懂证明证伪，但这个的证伪过程非常简单，包括已经遗忘很多高数的大学生。不用上 arXiv，不用懂深入的代数几何，拿张草稿纸就能算。

验证三对一映射

需要验证三个不同的点都映射到 (-\frac{1}{4}, 0, 0)：

\begin{aligned}
P_1 &= (0, 0, -\tfrac{1}{4}) \\[4pt]
P_2 &= (1, -\tfrac{3}{2}, \tfrac{13}{2}) \\[4pt]
P_3 &= (-1, \tfrac{3}{2}, \tfrac{13}{2})
\end{aligned}

验证 P_1：平凡到令人咂舌

对于 (0, 0, -\frac{1}{4})，xy = 0，1+xy = 1：

\begin{aligned}
f_1 &= 1^3 \cdot (-\tfrac{1}{4}) + 0 = -\tfrac{1}{4} \\[4pt]
f_2 &= 0 + 0 + 0 = 0 \\[4pt]
f_3 &= 0 - 0 - 0 = 0
\end{aligned}

P_1 \mapsto (-\frac{1}{4}, 0, 0)。算完你可能怀疑这反例是凑出来的——没错，它就是凑出来的。

验证 P_2：开始有趣了

对于 (1, -\frac{3}{2}, \frac{13}{2})，先算中间量：

xy = 1 \cdot \left(-\tfrac{3}{2}\right) = -\tfrac{3}{2}, \quad 1+xy = -\tfrac{1}{2}

(1+xy)^2 = \tfrac{1}{4}, \quad (1+xy)^3 = -\tfrac{1}{8}

y^2 = \tfrac{9}{4}, \quad 4+3xy = 4 - \tfrac{9}{2} = -\tfrac{1}{2}

代入 f_1：

\begin{aligned}
f_1 &= \left(-\tfrac{1}{8}\right) \cdot \tfrac{13}{2} + \tfrac{9}{4} \cdot \left(-\tfrac{1}{2}\right) \cdot \left(-\tfrac{1}{2}\right) \\[4pt]
    &= -\tfrac{13}{16} + \tfrac{9}{16} \\[4pt]
    &= -\tfrac{4}{16} = -\tfrac{1}{4}
\end{aligned}

代入 f_2：

\begin{aligned}
f_2 &= -\tfrac{3}{2} + 3 \cdot 1 \cdot \tfrac{1}{4} \cdot \tfrac{13}{2} + 3 \cdot 1 \cdot \tfrac{9}{4} \cdot \left(-\tfrac{1}{2}\right) \\[4pt]
    &= -\tfrac{3}{2} + \tfrac{39}{8} - \tfrac{27}{8} \\[4pt]
    &= -\tfrac{12}{8} + \tfrac{39}{8} - \tfrac{27}{8} = 0
\end{aligned}

代入 f_3：

\begin{aligned}
f_3 &= 2 \cdot 1 - 3 \cdot 1^2 \cdot \left(-\tfrac{3}{2}\right) - 1^3 \cdot \tfrac{13}{2} \\[4pt]
    &= 2 + \tfrac{9}{2} - \tfrac{13}{2} \\[4pt]
    &= \tfrac{4}{2} + \tfrac{9}{2} - \tfrac{13}{2} = 0
\end{aligned}

P_2 \mapsto (-\frac{1}{4}, 0, 0)。

验证 P_3：对称性的精妙

对于 (-1, \frac{3}{2}, \frac{13}{2})，xy = -1 \cdot \frac{3}{2} = -\frac{3}{2}，1+xy = -\frac{1}{2}，与 P_2 相同。因此依赖 u=1+xy 的项完全一致。

f_1（只依赖 y^2 和 u，不依赖 y 的符号）：

f_1 = -\tfrac{13}{16} + \tfrac{9}{16} = -\tfrac{1}{4} \quad \text{(与 }P_2\text{ 完全相同)}

f_2（x=-1 导致关键项的符号翻转）：

\begin{aligned}
f_2 &= \tfrac{3}{2} + 3 \cdot (-1) \cdot \tfrac{1}{4} \cdot \tfrac{13}{2} + 3 \cdot (-1) \cdot \tfrac{9}{4} \cdot \left(-\tfrac{1}{2}\right) \\[4pt]
    &= \tfrac{3}{2} - \tfrac{39}{8} + \tfrac{27}{8} \\[4pt]
    &= \tfrac{12}{8} - \tfrac{39}{8} + \tfrac{27}{8} = 0
\end{aligned}

f_3（x=-1，x^2=1，x^3=-1）：

\begin{aligned}
f_3 &= 2 \cdot (-1) - 3 \cdot 1 \cdot \tfrac{3}{2} - (-1) \cdot \tfrac{13}{2} \\[4pt]
    &= -2 - \tfrac{9}{2} + \tfrac{13}{2} \\[4pt]
    &= -\tfrac{4}{2} - \tfrac{9}{2} + \tfrac{13}{2} = 0
\end{aligned}

P_3 \mapsto (-\frac{1}{4}, 0, 0)。

三个不同的点，全部映射到同一个像。

这不光是“不单射”：这是一个三对一的碰撞。没了单射性，多项式逆就不存在；多项式逆不存在，雅可比猜想就死了。

Lean 4 验证

本文的 Lean 4 代码由 AI 生成 因为我不会 Lean，而且我也不想装 Mathlib 编译什么包，所以改用纯 Lean 4 内核求值器 #eval 进行数值验证。

以上验证过程可以用 Lean 4 形式化。把多项式映射定义清楚，然后用 #eval 交给内核求值器计算：

-- 多项式映射 F: ℚ³ → ℚ³
def F (x y z : Rat) : Rat × Rat × Rat :=
  ((1 + x*y)^3 * z + y^2 * (1 + x*y) * (4 + 3*x*y),
   y + 3*x*(1 + x*y)^2 * z + 3*x*y^2 * (4 + 3*x*y),
   2*x - 3*x^2*y - x^3*z)

-- 三个不同的点，映射到同一个像 (-1/4, 0, 0)
#eval F 0 0 (-1/4)
#eval F 1 (-3/2) (13/2)
#eval F (-1) (3/2) (13/2)

#eval 是 Lean 4 的内核求值器，可以直接计算 Rat（有理数）的算术表达式。三个 #eval 的输出均为 (-1/4, (0, 0))。

雅可比行列式为常数 -2

要完整验证，还得确认雅可比行列式确实是常数 -2。雅可比矩阵 J_F \in \mathbb{C}^{3 \times 3}：

J_F = \begin{bmatrix}
\frac{\partial f_1}{\partial x} & \frac{\partial f_1}{\partial y} & \frac{\partial f_1}{\partial z} \\[8pt]
\frac{\partial f_2}{\partial x} & \frac{\partial f_2}{\partial y} & \frac{\partial f_2}{\partial z} \\[8pt]
\frac{\partial f_3}{\partial x} & \frac{\partial f_3}{\partial y} & \frac{\partial f_3}{\partial z}
\end{bmatrix}

令 u = 1+xy，v = 4+3xy，逐项求导：

\begin{aligned}
\frac{\partial f_1}{\partial x} &= 3y(1+xy)^2 z + y^3(7+6xy) \\[4pt]
\frac{\partial f_1}{\partial y} &= 3x(1+xy)^2 z + 2y(1+xy)(4+3xy) + xy^2(7+6xy) \\[4pt]
\frac{\partial f_1}{\partial z} &= (1+xy)^3 \\[8pt]
\frac{\partial f_2}{\partial x} &= 3(1+xy)^2 z + 6xy(1+xy)z + 3y^2(4+3xy) + 9xy^3 \\[4pt]
\frac{\partial f_2}{\partial y} &= 1 + 6x^2(1+xy)z + 6xy(4+3xy) + 9x^2y^2 \\[4pt]
\frac{\partial f_2}{\partial z} &= 3x(1+xy)^2 \\[8pt]
\frac{\partial f_3}{\partial x} &= 2 - 6xy - 3x^2 z \\[4pt]
\frac{\partial f_3}{\partial y} &= -3x^2 \\[4pt]
\frac{\partial f_3}{\partial z} &= -x^3
\end{aligned}

这九个偏导代入 3 \times 3 行列式公式后，几乎所有项都互相抵消。你可以在 SymPy、Mathematica 甚至让 GPT 帮你展开。结果是：

\det(J_F) = -2

一个非零常数，完美满足雅可比猜想的条件。但映射却不单射——猜想被推翻。

Lean 4 验证

行列式恒等式同样可以丢给 Lean 验证。由于没装 Mathlib，无法使用 Matrix.det，AI 改用 3×3 行列式显式展开公式——本质一模一样：

-- 雅可比行列式（3×3 展开公式，等价于 Matrix.det）
def jacobianDet (x y z : Rat) : Rat :=
  let u := 1 + x*y
  let a11 := 3*y*u^2*z + y^3*(7+6*x*y)
  let a12 := 3*x*u^2*z + 2*y*u*(4+3*x*y) + x*y^2*(7+6*x*y)
  let a13 := u^3
  let a21 := 3*u^2*z + 6*x*y*u*z + 3*y^2*(4+3*x*y) + 9*x*y^3
  let a22 := 1 + 6*x^2*u*z + 6*x*y*(4+3*x*y) + 9*x^2*y^2
  let a23 := 3*x*u^2
  let a31 := 2 - 6*x*y - 3*x^2*z
  let a32 := -3*x^2
  let a33 := -x^3
  a11*(a22*a33 - a23*a32) - a12*(a21*a33 - a23*a31) + a13*(a21*a32 - a22*a31)

-- 在多个点验证行列式恒为 -2
#eval jacobianDet 0 0 0
#eval jacobianDet 1 2 3
#eval jacobianDet 1 (-3/2) (13/2)
#eval jacobianDet (-1) (3/2) (13/2)

以上四个 #eval 结果均为 -2。对于多项式恒等式，在足够多的点上验证等价于代数恒等式。如果装了 Mathlib，原教旨写法是用 Matrix.det + native_decide 做全称量化证明（∀ x y z），但手里没榔头不代表钉子敲不进去。

这个反例有多“狗屎”

行，验证完了，来聊点更有趣的。说实话，这个反例的出现方式，本身就堪称数学史上的一个行为艺术。

世界杯 + AI = 85年猜想终结者

85年来，世界上最聪明的数学家们——包括 Smale、Abhyankar、Mumford 这些泰斗级人物——前仆后继地尝试证明或推翻这个猜想，发表了无数论文。有人试图证明 n=2 时猜想成立，有人试图推广到更高维。

结果呢？一个 AI 在足球赛中场休息时就把反例吐出来了。

你知道这意味着什么吗？Alpöge 甚至没有专门坐下来“做研究”——他只是在看球赛的间隙，出于无聊，随口问了 AI 一句。这在数学史上大概是前无古人的：一个85年悬案，死于世界杯决赛夜的沙发消遣。 或者说，这个反例的难度可能是某个大一学生就能灵机一动出来的，但时间等不及了，AI 给出来了。

反例的“丑陋优雅”

仔细看一下这组多项式：

• f_1 = (1+xy)^3 z + y^2 (1+xy) (4+3xy) —— 嵌套的 (1+xy)，配上 4+3xy，像胡乱拼凑的
• f_2 = y + 3x(1+xy)^2 z + 3 x y^2 (4+3xy) —— 在 y 的基础上对称地贴了两块补丁
• f_3 = 2x - 3x^2 y - x^3 z —— 简单得不像话，干净到只有三项

你说它“丑”吧，确实丑——没人会凭空写出这种多项式。你说它“美”吧，每一项都恰到好处地让 3 \times 3 行列式中的巨量复杂项互相抵消，最终剩下一个干干净净的 -2。

这种“丑陋的优雅”，说实话，非常符合 AI 的风格——它不在乎式子好不好看，只在乎能不能通过计算。

三对一碰撞的设计感

最绝的是那三个碰撞点：

(0, 0, -\tfrac{1}{4}),\quad (1, -\tfrac{3}{2}, \tfrac{13}{2}),\quad (-1, \tfrac{3}{2}, \tfrac{13}{2})

注意 P_2 和 P_3 的对称性——x 和 y 的符号同时翻转，而 f_1 中 y 只以 y^2 出现、f_2 和 f_3 中的符号翻转被精确抵消，于是这两个看起来“对称”的点被映射到了完全相同的像。

这种精巧的对称性，你要说是人设计出来的我信，你要说是 AI 暴力搜索出来的……我也信。毕竟对 AI 来说，“构造一个满足这些约束的多项式”就是把问题丢进搜索空间然后等几秒钟的事情。

结语

AI 时代，“被吓到眩晕瘫坐在椅子上，那一刻就像看到原子弹爆炸” 这个不断在数学界发生，当然这个已经在计算机领域出现到令人无感了，但我想说AI的智力工程能力才刚刚开始……