雅可比猜想被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:{ℂ}^n\to {ℂ}^n$ 的雅可比行列式是一个非零常数，那么 $F$ 是否一定有多项式逆映射？

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

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

为什么重要

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

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

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

$$\begin{array}{cc}F(x,y,z)=(& (1+xy{)}^{3}z+y^2(1+xy)(4+3xy),\\ & y+3x(1+xy{)}^{2}z+3x{y}^2(4+3xy),\\ & 2x-3x^{2}y-x^{3}z)\end{array}$$

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

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

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

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

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

验证三对一映射

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

$$\begin{array}{cc}{P}_1& =(0,0,-\frac{1}{4})\\ P_2& =(1,-\frac{3}{2},\frac{13}{2})\\ P_3& =(-1,\frac{3}{2},\frac{13}{2})\end{array}$$

验证 $P_1$：平凡到令人咂舌

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

$$\begin{array}{cc}{f}_1& =1^3\cdot (-\frac{1}{4})+0=-\frac{1}{4}\\ f_2& =0+0+0=0\\ f_3& =0-0-0=0\end{array}$$

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

验证 $P_2$：开始有趣了

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

$$xy=1\cdot (-\frac{3}{2})=-\frac{3}{2},1+xy=-\frac{1}{2}$$

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

$$y^2=\frac{9}{4},4+3xy=4-\frac{9}{2}=-\frac{1}{2}$$

代入 $f_1$：

$$\begin{array}{cc}{f}_1& =(-\frac{1}{8})\cdot \frac{13}{2}+\frac{9}{4}\cdot (-\frac{1}{2})\cdot (-\frac{1}{2})\\ & =-\frac{13}{16}+\frac{9}{16}\\ & =-\frac{4}{16}=-\frac{1}{4}\end{array}$$

代入 $f_2$：

$$\begin{array}{cc}{f}_2& =-\frac{3}{2}+3\cdot 1\cdot \frac{1}{4}\cdot \frac{13}{2}+3\cdot 1\cdot \frac{9}{4}\cdot (-\frac{1}{2})\\ & =-\frac{3}{2}+\frac{39}{8}-\frac{27}{8}\\ & =-\frac{12}{8}+\frac{39}{8}-\frac{27}{8}=0\end{array}$$

代入 $f_3$：

$$\begin{array}{cc}{f}_3& =2\cdot 1-3\cdot 1^2\cdot (-\frac{3}{2})-1^3\cdot \frac{13}{2}\\ & =2+\frac{9}{2}-\frac{13}{2}\\ & =\frac{4}{2}+\frac{9}{2}-\frac{13}{2}=0\end{array}$$

$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=-\frac{13}{16}+\frac{9}{16}=-\frac{1}{4}\text{(与 }{P}_2\text{ 完全相同)}$$

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

$$\begin{array}{cc}{f}_2& =\frac{3}{2}+3\cdot (-1)\cdot \frac{1}{4}\cdot \frac{13}{2}+3\cdot (-1)\cdot \frac{9}{4}\cdot (-\frac{1}{2})\\ & =\frac{3}{2}-\frac{39}{8}+\frac{27}{8}\\ & =\frac{12}{8}-\frac{39}{8}+\frac{27}{8}=0\end{array}$$

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

$$\begin{array}{cc}{f}_3& =2\cdot (-1)-3\cdot 1\cdot \frac{3}{2}-(-1)\cdot \frac{13}{2}\\ & =-2-\frac{9}{2}+\frac{13}{2}\\ & =-\frac{4}{2}-\frac{9}{2}+\frac{13}{2}=0\end{array}$$

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

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

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

Lean 4 验证

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

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

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

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

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

雅可比行列式为常数 $-2$

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

$$J_F=\left[\begin{array}{ccc}\frac{\partial f_1}{\partial x}& \frac{\partial f_1}{\partial y}& \frac{\partial f_1}{\partial z}\\ \frac{\partial f_2}{\partial x}& \frac{\partial f_2}{\partial y}& \frac{\partial f_2}{\partial z}\\ \frac{\partial f_3}{\partial x}& \frac{\partial f_3}{\partial y}& \frac{\partial f_3}{\partial z}\end{array}\right]$$

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

$$\begin{array}{cc}\frac{\partial f_1}{\partial x}& =3y{(1+xy)}^{2}z+y^3(7+6xy)\\ \frac{\partial f_1}{\partial y}& =3x{(1+xy)}^{2}z+2y(1+xy)(4+3xy)+x{y}^2(7+6xy)\\ \frac{\partial f_1}{\partial z}& ={(1+xy)}^3\\ \frac{\partial f_2}{\partial x}& =3{(1+xy)}^{2}z+6xy(1+xy)z+3y^2(4+3xy)+9x{y}^3\\ \frac{\partial f_2}{\partial y}& =1+6x^2(1+xy)z+6xy(4+3xy)+9x^2{y}^2\\ \frac{\partial f_2}{\partial z}& =3x{(1+xy)}^2\\ \frac{\partial f_3}{\partial x}& =2-6xy-3x^{2}z\\ \frac{\partial f_3}{\partial y}& =-3x^2\\ \frac{\partial f_3}{\partial z}& =-x^3\end{array}$$

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

$$\det (J_F)=-2$$

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

Lean 4 验证

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

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

15
-- 在多个点验证行列式恒为 -2
16
#eval jacobianDet 0 0 0
17
#eval jacobianDet 1 2 3
18
#eval jacobianDet 1 (-3/2) (13/2)
19
#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+3x{y}^2(4+3xy)$ —— 在 $y$ 的基础上对称地贴了两块补丁
• $f_3=2x-3x^{2}y-x^{3}z$ —— 简单得不像话，干净到只有三项

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

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

三对一碰撞的设计感

最绝的是那三个碰撞点：

$$(0,0,-\frac{1}{4}),(1,-\frac{3}{2},\frac{13}{2}),(-1,\frac{3}{2},\frac{13}{2})$$

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

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

结语

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