AI开始“卷”数学：Lean成了大模型的新考场，但离RSI还很远
人们曾把柯洁视为AI冲击人类的样本；如今，数学家也被推到相似的处境。OpenAI近期在数学形式化方向密集动作，引发外界对ETH、P=NP等经典难题的新一轮讨论。但真正值得关注的，不是某个猜想是否被“端掉”，而是数学正在变成AI可自动验证、可规模化训练的新基础设施。
十年前，AI在围棋盘上让职业棋手感到压力；后来，程序员开始习惯Copilot写代码；现在，轮到数学界感受“柯洁式处境”。OpenAI一边放出大量数学相关手稿，一边把讨论推向更高难度的经典猜想。表面看是大模型在秀智商，往深处看，是数学界自己先造好了“自动裁判”。
数学难，不只难在证明，还难在审查。前沿证明引用多、跳步多，一句“显然可得”可能跨过大段推导。于是数学家开始用Lean把命题和证明写成机器能理解、能严格检查的代码。Lean本质是编程语言，数学命题被翻译成代码后，AI就有了熟悉的入口。
更关键的是Mathlib。这个“数学开源武器库”积累超两百万行形式化内容，覆盖代数、微积分、数论、拓扑等。前人证明过的定理可调用，AI不必每次从零推导。验证器加知识库，构成了数学AI的基础设施。
Lean有多严格？已知a+b=10，要证b+a=10，也得明确a、b是自然数，调用加法交换律，再用链式推导一步步走完。它把证明和检查拆开，最终拍板的是短小内核，降低出Bug风险。商业上，这意味着“自动裁判”成了稀缺资产：谁能掌握高质量形式化数据和验证工具，谁就多一层训练护城河。
大厂盯上数学，不只是秀肌肉。大模型高质量数据越来越紧俏，数学规则清晰、反馈明确，天然适合强化学习。AI生成证明，Lean判对错；跑通是优质数据，没跑通也能当反例。这类似AlphaGo自我对弈：不靠人类喂棋谱，而靠系统内反馈加速迭代。所谓RSI自进化，目前仍是苗头，但方向足够诱人。
动作已经密集起来。OpenAI在数学方向连续出手；Anthropic被曝招募数学家；Google早在2024年就用Lean搭AlphaProof做实验，达到奥数银牌水平，并在Nature发表论文。竞争正从模型参数，延伸到验证器、形式化数据和训练闭环。
Lean还被用来治AI幻觉。Lean创始人提到一个硬核案例：让Claude用Lean重写底层zlib压缩库，并证明在一定数据大小和压缩级别下，压缩再解压能原样还原。这不是拿几十万个文件逐个测试，而是用数学证明覆盖条件。AI胡编乱造的概率会降低，但不能说整个库从此无Bug。
局限同样明显。Lean只验证推导是否合规，不管题目有没有翻译对。若把题意写歪，或把待证结论提前塞进条件，只要后面能圆回来，它也可能打勾。它更不关心证明有没有价值：AI可以用公理排列组合出大量正确但无意义的“车轱辘定理”。现实世界的模糊地带、利益权衡和“对错”的相对性，也很难整齐塞进形式化语言。
所以，OpenAI这波操作不必让人立刻焦虑。数学能否被AI彻底拎清尚无定论，RSI更像人们对AGI的美好设想，而非已兑现的路线图。即便飞轮转起来，AI擅长的仍是“怎么做”；一件事值不值得做、为什么做，最终解释权还在人类手里。对产业来说，Lean和Mathlib代表的验证基础设施，值得提前下注；对普通人来说，先别急着把自己代入柯洁，故事才刚开场。
