先把结果摆出来。三维复空间到自身的一个多项式映射，雅可比行列式恒等于 −2，非零常数，满足猜想的全部前提。然后三个不同的输入点 (0, 0, −1/4)、(1, −3/2, 13/2)、(−1, 3/2, 13/2) 全被送到同一个 (−1/4, 0, 0)。不单射就没有逆，多项式逆更谈不上。雅可比猜想死在三维，padding 一下四维以上跟着死。
我喜欢这件事的地方在这儿。它不需要你相信任何人。过去每一条「AI 解决了数学难题」的新闻，你都得先信一个机构的声誉、一个评审流程、一个作者的人品，然后才轮到信结论。这次验证成本是二十行 SymPy 加几秒钟。Alpöge 7 月 20 日夜里在 X 上贴出来的，模型据说是世界杯决赛那场算的；一天之内 SymPy、Wolfram、Isabelle/HOL 之外还有四份独立写出来的 Lean 4 形式化全部跑通。这个验证密度在数学史上找不到先例。
补几条原帖没展开的。
「78 年」这个数要核对。 Keller 1939 年提出，到 2026 年是 87 年，英文报道口径统一写 87。如果标题里的 78 指的是另一条线索，麻烦回帖指正，可能是我读漏了。
死的只有三维及以上。 n=2 那半边还活着，而且只被计算验证到 100 次。这道题最讽刺的地方就在这里：你以为倒下的是难的那半边，其实容易的那半边还原封不动。
反例暴露的结构比结论值钱。 这个映射不是 proper 的，它的像缺一条余维 2 的曲线 Γ，非 proper 的轨迹落在一个超曲面 Σ 上。所以 refined 的定理活下来了，proper 的 Keller 映射仍然是多项式自同构。Gowers 说这是他听说的第一个够大的 AI 解决问题。也有人泼冷水，说反例结束一场争论，却不像证明那样告诉你「它为什么曾经看起来是对的」。我偏后者多一点。
它还没过同行评议。 到 8 月初，Alpöge 承诺的完整论文没出来，现在形态是一条 X 帖子加几份形式化。有位 OpenAI 的研究者说内部模型独立找到了基本一样的反例，这说明结构不是某个系统的偶然，但「独立」到什么程度没人核实。
下一根钉子已经换了。 不是正确性，是新颖性。反例出来几天之内，高维反例的族就开始在社区里流传。陶哲轩当年论证「证明太长没人愿意逐行验」是为正确性发愁，同一套论证现在搬到了新颖性上：生成定理的速度上去了，判断「这条是不是别人已经做过了」变成新瓶颈。已经有人在做了，AViD 那套 Lean 4 自动新颖性判定就是冲这个来的。
一句话收尾：n=2 那半边还开着，谁把它关上，谁才算真的结束这道题。