AI攻入数学界：OpenAI先挑千禧年猜想，又向P=NP猜想发难

人们这才看明白，柯洁当年遇到的，其实是一种处境……

十年前，被冲击的是围棋；再往后，轮到程序员；最近被密集轰炸的，换成了数学家。

OpenAI 从千禧年猜想入手，随后一次放出七百多份手稿，把数学界搅得翻天覆地。

更近的一步，是直接干掉 ETH 假设——计算机算法的一大基石，冲着最出名的 P=NP 猜想就去了。

数学可是科学的王后，活跃着人类智商最高的一小撮人。

那 AI 大人这回又看上了什么，偏偏挑这么块硬骨头来啃？

世超翻了一圈，还真别说，可能这嫁衣是数学家们自己做的。

数学这东西，尤其是前沿难题，就算有大佬证出来，也相当难懂，引用横七竖八，光审查证明本身就够费功夫。

何况数学家写证明时，中间常有各种省略和跳步，有时候一句“ 显然可得 ”，一大段推导就跨过去了。

显然不显然先放一边，可不可得怕是都不一定……

计算机性能越来越给力之后，计算机科学家和数学家就动起脑筋，想让机器来承担这部分审查工作，既省事，又能专治这种“ 显然可得 ”。

其中最关键的是叫 Lean 的数学证明系统。它本质上是门编程语言，能把数学命题和证明过程变成机器能理解、能严格检查的形式，也就是代码。

诶，这不就对上了——编程？代码？AI 可太喜欢了。

数学本来就有一套严密的逻辑体系，如今连检查证明的程序都有了，这不是纯纯瞌睡送枕头么。

所以要说 AI 为什么卯上数学，Lean 这类工具提供的验证能力，绝对是其中一块重要拼图。

说了这么多，Lean 到底有多牛？

这么说吧，只要用法正确，凡是通过它验证的，基本就能钉死证明过程没毛病。

因为这东西太铁了，根本不留情面，干起活来就是个细节控。

比如已知 a+b = 10，要证 b+a = 10。

这够显然了吧？诶，不中，你得把“ 显然 ”拆出来，告诉它为什么显然。

换成 Lean 的代码就是这样的： theorem demo (a b : Nat)(h : a + b =10) : b + a =10:= by calcb + a = a + b := Nat.add_comm b a_ = 10:= h

这一步里，得先把 a、b 都是自然数交代清楚，再把题目翻译过去，告诉它已知“ a + b = 10 ”，要证的是“ b + a ”同样等于 10。

接着挑“ calc ”工具做链式推导，再调用定理“ Nat.add_comm ”，即加法交换律，证出 a+b = b+a。走完这一整套，b+a 等于 10 才推得出来。

换句话说，想让证明跑通，就必须老老实实把数学命题翻成它认得的符号语言，再照严格的逻辑规则一步步把证明搭起来。不管是搬前人证过的定理，还是自己新弄出一个结论，都得拿出合法的逻辑依据。

最要紧的一点是，Lean 虽然体量庞大、结构复杂，可数学家个个有强迫症，底层架构和逻辑都理得极清楚：证明和检查被拆成了两件事，前面的证明程序再复杂，最后拍板核验的也只是那个短小精悍的内核。

这样一来，出 Bug 的概率就低了不少，人工二审也省事得多。

另外，Lean 还配了个重量级搭档 Mathlib，可以理解成数学界的开源武器库。代数、微积分、数论、拓扑学等等，前人研究过的东西被数学家们一批批翻成 Lean 能懂的形式，装进了 Mathlib。

眼下这座库已经攒下超过两百万行形式化的数学内容。往后遇到前人证过的定理，不必再从零推起，直接从 Mathlib 里调就行。

说到底，这玩意儿本来就是为让机器看懂而造的，到了 AI 时代，自然就成了大模型练手的好场地。

不过，要是只把 AI 厂商钻研数学看成秀肌肉，那格局就小了。世超翻完资料，觉得还有另一种可能：他们做数学，也许真是顺手的事。

因为 Lean 的潜力远不止这些，它还能跟眼下 AI 圈最热的概念搭上线——AI 的自进化，RSI。

眼下模型训练，算力紧俏，高质量数据同样是抢手货。世超之前写过，这门生意在大洋彼岸都快干冒烟了，时薪高得吓人。

根子上还是人类积累的可用知识太少，大模型却是个无底洞。AI 要接着往上进化，总靠人拿小勺喂饭不是办法，终究得自己找活路。

怎么找？当年 AlphaGo 就做了个示范。

它后来能把人类棋手按在地上摩擦，不只靠背棋谱，还靠自己跟自己下、左右脑互搏的奇招，迭代速度才彻底拉满。大模型厂商眼馋这套玩法很久了，也想让 AI 自己生成数据、自己训练自己。

可问题在于，围棋规则清晰，谁赢谁输、目数多少，系统一算就知道，模拟起来很容易。

可换到现实世界的其他领域，AI自己根本分不清它吐出来的东西哪句靠谱、哪句是胡扯。

要是拿一堆掺了毒的假数据去搞“自进化”，用不了几轮，GPT就能给你练成会说话的汤姆猫。

这时候再看Lean这种形式化验证器，妥妥的天选之子。

它不用人类专家批卷子，就能全自动给出基本可靠、还能规模化的反馈。

AI写完一段证明扔进去，跑通了就是优质数据，没跑通也不白费，出错的数据还能当反例用，简直是为强化学习量身定做的。

有了Lean这头赛博永动驴，AI就能像当年下围棋那样，没日没夜地在数学世界里试错、拿反馈、刷经验，左脚踩右脚开启超级进化。

虽然还不至于直接实现RSI自进化，但起码也沾上了边儿。

前景有多诱人，看看大厂的动作就知道了。

OpenAI在猛攻，隔壁Anthropic的风声也不小，招了一堆人类数学家。

谷歌这边，早在2024年就拿Lean搭了个叫AlphaProof的系统做实验，做出了奥数银牌的水平，后来还在《Nature》上发了论文。

除此之外，治AI幻觉这事儿上，Lean也是一把好手。

Lean的创始人Leonardo de Moura提到过一个非常硬核的例子：让AI用Lean去重写底层的zlib压缩库。

zlib大伙儿可能没听过，你只需要知道它是互联网基础设施级别的东西就行了，咱用的图片、压缩包等等都跟它有关。

工程师们让Claude用Lean把它重构了一遍，顺手还用数学逻辑证明了这么个事儿：

“对于一定大小范围内的数据，不管用什么压缩级别，只要经过这套程序压缩再解压，都能原封不动地还原出来。”

这就相当给力了，因为它不是拿几十万个文件挨个测试，而是在数学上证明，只要符合这些条件，结果就不会出错。

以前AI拍着胸脯保证代码没问题，那可信不得，终归还得自己设计测试，拿各种数据反复折腾，才能多攒一点信心。

但现在，审查的换成了Lean这个不近人情的程序，结论就可以相当放心了。

不能说整个zlib库从此彻底没Bug，但这么一套走下来，AI胡编乱造的概率是切实降低了。

当然了，话说回来，Lean疗效虽牛，范围还是挺局限的，没法包治百病。

就比如它做题的时候严厉但死板，虽然能判断中间的推导过程合不合规矩，但却不管你一开始的“题目”写没写对。

用Lean给现实问题建模时，万一题意译偏了，或把本该证明的结论先当条件用了，只要往后能圆得过去，Lean一样会判定通过。

更无情的是，它完全不在乎证明的东西到底有没有价值。

AI完全可以利用几条公理，排列组合出几百万条绝对正确、Lean检查也全部通过的车轱辘定理，但这鸡毛意义没有。

好比一个学生本来就会解一元二次方程，如今天天自己编一万道题来解，正确率再高，数学能力恐怕也谈不上质变。

说到底，现实世界并非样样都能像数学那样，被整整齐齐地装进形式化语言。日常生活里绝大多数琐碎事，无论是写一篇逗大家一乐的文章，还是拟定一项复杂的社会政策，几乎都找不到统一量化的标尺。

连“对与错”本身，很多时候也是相对而言，里头满是模糊地带和利益权衡的泥潭。像 Lean 这种强调非黑即白的形式化验证工具，恐怕连落脚的地方都难找。

所以看完 OpenAI 这一轮操作，大家其实也不必过于焦虑。数学它到底拎不拎得清还没有定论，至于更唬人的 RSI，眼下不过是个苗头，算是人们对 AGI 的一种美好设想。

就像当年热力学规律还没摸清的时候，永动机也曾让无数聪明人前赴后继。可后来物理学告诉我们，这东西从根子上就走不通。

当然，RSI 不是永动机，也不违反什么已知的物理规律。

但这套左手生成、右手验证的飞轮一旦转起来，究竟是直接让 AI 智商原地起飞，还是没转几下就一头撞上理论天花板，目前谁也给不出准数。

退一万步说，就算 AI 再厉害，它干的也是生产的活儿，本质上解决的是“怎么做”的问题。至于一件事到底有没有价值、值不值得做、人类为什么要这么做？

放心，最终解释权还是归咱们人类。毕竟直立行走的人类可不管什么投入产出比，很多闲得发慌搞出来的大活儿，其实就只是闲得发慌而已。

美编：素描

图片、资料来源：

B站、Lean、Mathlib、Google、Science、Zlib，部分图源网络