OpenAI近日一口气发布了十项惊人的数学进展，其中包括首次证明非Sofic群的存在性、给出全新的电路下界、攻克最近向量问题难度极限以及双人量子博弈并行重复指数衰减定理。
哥伦比亚大学副教授Henry Yuen对其中最后一个成果感触最深。2016年，他曾在此问题上取得重大突破，却未彻底解决。十年来，他屡战屡败，甚至一个月前还尝试用ChatGPT 5.5寻找终极证明，结果收效甚微。如今，OpenAI的模型似乎“踩在他的肩膀上”，轻轻一脚就把球送进了球门。
几天前，Lijie Chen发给Yuen等人一份论文草稿。当时Yuen忙碌无暇细读，如今公布后，他忍不住要谈谈自己的看法。量子并行重复定理曾是Yuen研究生阶段耗费数年心血钻研的领域，也是他最引以为傲的成果。他记得无数个在咖啡馆和深夜里拆解Ran Raz经典定理的午后，吞下了成吨的数学工具，最终证明了多项式衰减，并借此建立了对自己实力的信心。
Yuen相信OpenAI的证明是正确的，毕竟已有Lean形式化验证。但他同时也感到失望，因为这份证明读起来满是“AI味儿”。它冗长地铺垫却绕了半天，关键环节像变魔术一样让人一头雾水。证明突然跳转到“用预解式找purification”，中间几乎没有逻辑阶梯，随后是一连串奇怪的矩阵熵计算，最后才告诉你这条路走得通。更令人头疼的是，最精妙的Uhlmann变换技巧本应是高潮，却被AI弃子如泥沙，毫无预警地丢在第四节，没有解释直觉从何而来。Yuen希望OpenAI能多花些提示词，把这篇文稿好好梳理一下。
更扎心的是第二层：Lean验证通过，不等于理解。机器可以保证每一步推导无懈可击，但“为什么这一招有效”“它在理论版图里意味着什么”“还能用在哪里”——这些问题，Lean一个都答不了。Yuen坦言，他到现在还在消化这份证明。答案摆在面前，他却要像读外行论文一样，一行行去还原AI没说出口的直觉。没错，Lean只是形式化，不代表他真懂了。他不禁怀疑：如果AI把魂牵梦绕的难题都解决了，数学家还剩下什么？虽然问题接踵而至，但他越来越确定：数学家接下来的日子不会闲，既要驯服这些思想巨兽，还得把它们的黑话翻译成人话。
上周，Ramana Kumar用300行Lean证伪了最出名的未解之谜“科拉兹猜想”。这个问题自1937年提出以来，数学家们始终无法证明其成立，也没找到反例。如果被证伪，无疑是爆炸性新闻。可惜的是，3天后这份证明被判无效，因为实际上只是利用了Lean内核的一个底层漏洞。OpenAI的Daniel Selsam带着专门研究网络安全的AI协助Lean FRO做了一次内核审计，结果发现了不止一起漏洞。
几乎同一时间，Rutgers大学教授Alex Kontorovich发文提醒：别把Lean当全能验证者。他直指死穴——语义对齐。即使Lean内核无懈可击，Lean也只管代码编译，谁来确保你写的定义和人类直觉意图是一回事？Lean能确认的只有逻辑无误，但绝不验证“这段形式化陈述真的对应你想证的那个定理吗？”这个更要命的问题。而在ICM 2026的演讲中，Kontorovich曾指出：形式化数学最大的盲区不在“推对了导”，而在“说对了话”。最后把关的，还得是人类专家。当年Liquid Tensor Experiment之所以封神，靠的恰恰是研究者对每个数学定义近乎偏执的人工审查。两位教授的话指向同一个事实：AI能证明，机器能验证，但理解和把关，还是人类的活。