不再是人脑的天下！Lean 机器验证落地，AI 开启全自动数学时代

你敢信吗？刚出炉的2026年菲尔兹奖，已经被网友盖章是“最后一届全靠人类成果获奖”的菲尔兹奖了。新晋得奖的顶级数学家公开放话，两年内AI做数学会比人类数学家更强，说完直接官宣加入OpenAI。这阵仗放在几年前想都不敢想，AI赢个棋破个游戏纪录也就算了，现在居然要碰人类智慧王冠上最亮的那颗明珠——数学了。

这几年AI数学能力的进步，其实一直都有迹可循。从高考数学拿高分，搞定几何证明题，甚至帮大学生应付数学作业，再摸到国际数学奥赛金牌的水平，步子迈得比所有人预想的都快。直到最近一两个月，AI直接摸到了人类能力的边界，连费马大定理、黎曼猜想这些名垂数学史的大问题，都开始有AI的身影了。

Anthropic的研究版Claude，已经把黎曼ζ函数非平凡零点位于临界线的渐近比例下界，从原来的约41.6%提高到了67.2%，还给出了符合要求的Lean形式化证明。OpenAI的GPT-6 Astra在和孪生素数猜想密切相关的有界素数间隔问题上，直接把业界保持的上界从240降到了186，相关论文和Lean代码都已经公开。Claude还花了大约11天，大体自主完成了费马大定理的首个完整计算机核验证明，填上了费马当年那个“页边太窄写不下”的三百年大坑。

除了大公司的成果，独立研究者也跟上了进度。知乎用户子鱼用GPT搭配相关工具，完成了陈景润“1+2”结论的形式化，大概率是历史上首个完成这项工作的成果，目前还在推进更近期的研究。就2026年这大半年，AI在数学上的突破一茬接一茬，各种知名猜想相关的新进展列都列不完。从头到尾，Lean和形式化这两个概念出现得最多，它们就是给AI数学成果保驾护航的核心校验工具。

大语言模型大家都熟，最让人头疼的问题就是幻觉，很容易一本正经说瞎话。它生成内容的逻辑本来就是预测下一个字符，没法天生保证每一步推导都符合逻辑，哪怕看起来天衣无缝，也可能藏着错误。放到编程领域，有编译器帮着查错，测试能揪出逻辑问题，AI改起来也快，Lean其实就是数学领域的“编译器”。

Lean项目2013年在微软研究院启动，第二年就放出了第一个公开版本，它既是一门函数式编程语言，也是一个交互式定理证明器。它能把人类数学论文里的定义、公理、引理和每一步逻辑推导，全翻译成机器能读懂的内容，这个转换过程就叫形式化。等整个定理都完成形式化，检查每一步逻辑对不对的工作，就可以直接交给计算机，省了顶级数学家大把啃复杂论文的精力。

现在不管是OpenAI、Anthropic这类头部AI公司，还是不少独立数学工作者，都在摸索AI出证明、机器做验证、AI自动修正的工作流程，已经能批量产出数学突破了。大模型搭配Lean这套组合，直接给数学研究换了一套玩法，算得上是实打实的范式转换。人类最顶尖的数学家早就察觉到了这个风向，比如陶哲轩，对AI的看法这两年变化特别大。

2024年的时候，陶哲轩还说AI更像一个平庸但不至于没用的研究生。到2026年春天，他已经承认AI能帮着查文献、写代码、试计算、筛掉走不通的方向，实际研究里节省的时间已经比浪费的多。但他也提出了一个很值得深思的问题，点出了AI做数学最核心的争议。

陶哲轩把数学研究比作徒步去山里找瀑布，人类自己一步步探路，会迷路会绕弯，还能在路上发现从没见过的新景观。AI就像一架现成的直升机，直接把人送到瀑布门口，速度快得离谱，但人类根本记不住来路，也错过路上所有意外的惊喜。那些走错的路、试错磨出来的新工具新概念，往往才是数学研究最值钱的部分，比最后那个答案重要太多。

之前陶哲轩拿悬而未决的纳维-斯托克斯问题举例，说要是AI靠超大算力闷头算出了证明，最后只给人类扔一个最终结果，那就算解决了问题，其实也没给数学界增加多少对应的价值。这话一出网上立马传疯了，好多人说陶哲轩已经偷偷看过AI搞定这个问题的证明，吓得他赶紧出来澄清，这只是假设性的举例，目前根本没有任何重大新进展。这件事本身就很说明问题，现在大家都默认，AI哪天拿下任何一个顶级难题，都不会让人觉得奇怪。

过去大家讨论AI能不能做真正的科学研究，总喜欢提“爱因斯坦测试”，就是只给AI一百多年前爱因斯坦能拿到的所有资料，看它能不能不靠提示，自己独立提出广义相对论。大家都觉得，能做到这一步，AI才算真的有原创的科学创造力，而这在之前还只是个遥不可及的思想实验。放到2026年的今天，这个曾经遥远的设想，居然已经慢慢露出了现实的轮廓。

现在AI在数学领域，早就不是帮着算算数、整理已有结论的工具了。它已经能独立找到反例，刷新人类保持了几十年的纪录，就算冲击顶级猜想失败，也能顺手带出来一个人类从没发现过的新结果。曾经我们还在没完没了讨论AI能不能做出真正的科学发现，现在这个问题已经一点点变成了现实，进步的速度，比绝大多数人预想的都要快得多。

参考资料：人民日报 人工智能赋能基础学科发展