三位数学家读 OpenAI 的 722 篇手稿：准黎曼证明是已知工具的新串法，流体工程什么都没变

准黎曼猜想：命题早在 Mathlib 里，所以可以信；方法到不了二分之一

Kontorovich 说他没想到有生之年能看到准黎曼猜想被证明。他对证明正确有“百分之百的信心”，理由是：它的 Lean 命题本来就在 Mathlib 里，不是 OpenAI 自己写的，而证明没有留下任何未完成的步骤。他读了证明的大意：把 Möbius 函数嵌进去、用六次特征去扭，这些都是解析数论学者的“家常手法”，被以恰好的顺序串了起来。结果是一整条竖带：实部在八分之七到一之间没有零点；还有第二个证明到十二分之十一左右。他说这个方法本质上降不到二分之一，到二分之一就是完整的黎曼猜想，那需要新想法。同一期里他前面说这“不是真正的新想法”，后面又说准黎曼猜想“需要很多很多新想法，而它想出来了”。

“The Lean statement was already in the library, was already in Mathlib, so the fact that they have a sorry-free proof gives me 100% confidence that the proof is right.”Alex Kontorovich

Unique Games：结论是真的，但还没人能读懂它为什么成立

Moitra 说 Unique Games 猜想在他入行时还在争论真假，2010 年代意见年年在变；Dor Minzer 和 Irit Dinur 证明了较弱的 2 对 1 版本，他原以为人类再要 10 到 20 年。OpenAI 这批结果说它是真的。他说放出之前几周就有传言，Minzer 在一篇论文的脚注里写因为传言要提前放出自己的方法。他说这些证明“不太好读”，不能很快指出关键的新想法在哪；现在要做的是消化这些证明。他还说，放出前几小时他问提出这个猜想的 Subhash Khot，如果出来正面证明他会不会读，Khot 说不会。

“they're not very readable papers. It's not like you can point to them and really quickly identify what's a new key idea.”Ankur Moitra

Navier-Stokes：重要的数学，对工程没有用

Brunton 是做流体的工程师。他描述 AI 的构造：一条特殊的涡丝在第三个方向上被拉长、变细，半径按一个特定的速率收缩，流体总能量保持有限，但在这条细丝上涡量变成无穷大，像花样滑冰收臂越转越快。他说在 AI 之前数学家开始觉得能找到这种反例时，他就已经吃惊。但到这种爆破发生时，尺度已经小到不再是流体，Navier-Stokes 方程本身不成立了。所以“日常的工程流体计算几乎完全没变”：设计机翼或人工心脏仍然要超算和风洞。他的说法是，解决了一个百万美元的数学问题，还有一个万亿美元的工程问题：怎样快速预测流动、做逆向设计。

“it operates at a regime that's so non-physical that it doesn't really affect my day-to-day engineering.”Steven Brunton

形式化：一千三百万行的费马大定理之后，“把纸上的证明变成没有漏洞的 Lean 证明”已经做到

Kontorovich 说他在普林斯顿数学系做报告，讲 AI 只能在 Mathlib 上面搭一两层、是在“拼凑”，两天后 Anthropic 放出一千三百万行、从公理出发的费马大定理 Lean 证明，他说自己报告里讲的“全错了”。费马大定理的命题很初等，一眼就能看出写对了，不需要核对命题是否对得上。他说这证明不干净，要成为 Mathlib 质量还要大量工作；但“能不能把人写在纸上的证明变成没有未完成步骤的形式证明”这个问题，他认为已经解决。

只放了成功的那一成，边界画不出来

Moitra 说 OpenAI 据说给了几千个问题，只放出正面的解答，成功率大约一成，所以没法看出哪些问题会被解决、哪些不会。他还担心两件事：看起来最安全的问题是那些显然需要一个全新想法的问题，而一旦有人把那个想法公开，AI 就能把它推到头，数学家可能因此更不愿分享想法；还有，这么多 AI 论文需要有人审，他希望找到集体核验的办法，而不是靠已经超负荷的期刊。