人们终于意识到，柯洁其实是种处境。。。
十年前是围棋，后来轮到了程序员，最近被轰炸的又成了数学家们。
OpenAI 先是千禧年猜想起手，接着一口气放出七百多份手稿，给数学界搅了个天翻地覆。
最近更是直接给 ETH 假设，这位计算机算法的一大基石给端掉了，朝着那个最出名的 P=NP 猜想就杠上去了。
这可是数学，科学的王后啊，活跃着人类智商最高的一小撮儿人。
咱这 AI 大人又看到了啥，偏偏挑了这么个硬骨头来啃呢？
世超扒拉了一圈，你别说，可能还是数学家们自己做的嫁衣。
众所周知，数学这东西，特别是前沿的一些难题，就算有大佬证出来了，那也是相当难懂的，横七竖八的引用，光是审查证明本身都得费很大功夫。
而且数学家写证明，中间经常有各种省略和跳步，有时候一句 “ 显然可得 ” 就能直接跨过一大段推导。
显然不显然的先不说，可不可得恐怕都不一定。。。
于是计算机性能越来越给力后，计算机科学家、数学家们就开动脑筋，想办法让机器来负责这部分审查的工作，既能省事儿，还能专治这种 “ 显然可得 ”。
其中最核心的是一套叫 Lean 的数学证明系统，这玩意儿本质就是门编程语言，它能把数学命题和证明过程，变成机器能够理解、能够严格检查的形式，也就是代码。
诶，这不就对上了。编程？代码？那 AI 可太喜欢了。
本来数学就有一套严密的逻辑体系，现在连检查证明的程序都有了，这不纯纯瞌睡了送枕头么。
所以要说 AI 为什么卯上了数学，Lean 这类工具提供的验证能力，绝对是其中一块重要拼图。
说了这么多，那 Lean 到底有多牛批呢？
这么说吧，只要使用姿势正确，那凡是通过这个验证的，基本就能钉死证明过程没毛病。
因为哥们太铁了，根本不讲情面的，工作起来就是个细节怪。
比如已知 a+b = 10，要证个 b+a = 10。
这够显然了吧，诶，不中，你得把 “ 显然 ” 拆出来，告诉它为啥显然。
换成 Lean 的代码就是这样的：
其中，先讲清 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。
众所周知，现在的模型训练，除了算力很紧俏，高质量的数据也是顶级香饽饽。
世超之前就写过，这门儿生意在大洋彼岸都快干冒烟了，时薪高得吓死人。
时薪 2000 给 AI 打工，到底是谁在做啊？
归根结底，还是人类攒下的可用知识太少了，大模型又是个无底洞。AI 想继续往上进化，一直这么靠人类拿小勺喂饭肯定不是个事儿，还是得自谋出路才行。
咋谋呢？当年 AlphaGo 就打了个好样。
它后来之所以能把人类棋手按在地上摩擦，靠的不只是背棋谱，还有自己跟自己下棋，左右脑互搏的奇招，然后才把迭代速度彻底拉满。
大模型的厂商们眼馋这套玩法很久了，也想让 AI 自己生成数据、自己训练自己。
但问题是，围棋这玩意儿规则清晰，谁赢谁输、目数多少，系统一算便知，非常好模拟。
可一旦放到现实世界的其他领域，AI 自己吐出来的东西，哪儿正经哪儿扯淡，它自己根本分不清啊。
要是拿一堆掺了毒的假数据去搞 “ 自进化 ”，那用不了几轮，GPT 直接给你练成会说话的汤姆猫。
这时候再看 Lean 这种形式化验证器，不就妥妥的天选之子了。
它不依赖人类专家去批卷子，就能全自动给出基本可靠，还能规模化的反馈。
AI 写完一段证明扔进去，跑通了就是优质数据，没跑通也不是零蛋，出错数据还能拿来当反例，简直就是为强化学习量身定做的。
有了 Lean 这头赛博永动驴，AI 就可以像当年下围棋一样，没日没夜地在数学世界里试错、拿反馈、刷经验，左脚踩右脚开启超级进化。
虽然不至于直接实现 RSI 自进化吧，但起码也是沾上了边儿。
至于前景有多诱人，看看大厂的动作就知道了。
不光 OpenAI 在猛攻，隔壁 Anthropic 的风声也不小，招了一堆人类数学家。
还有咱的谷歌大善人，早在 2024 年就拿 Lean 搭了个叫 AlphaProof 的系统做实验，做出了奥数银牌的水平，后来还在《Nature》上发了论文。
除此之外，Lean 在治 AI 幻觉这事儿上，也是一把好手。
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 再牛批，它干的也是生产的活儿，本质上负责的还是 “ 怎么做 ” 的问题。
至于一件事儿到底有没有价值，值不值得去做，人类为什么要这么做？
放心，这事儿的最终解释权，还是归咱们人类所有。
毕竟双脚直立猿可不管你什么投入产出比，很多闲的蛋疼整出来的大活儿，其实就只是闲的蛋疼而已。。。
撰文：风华
