ARTICLE · 1102028
AI,验证了人类最聪明的大脑
AI,验证了人类最聪明的大脑
数学界今天出了件大事。
一件听起来有点穿越的事。
庞加莱猜想，这个困扰了人类一百多年的数学难题，它的完整证明，第一次被机器完整验证了。
不是AI证明了它。
是AI和人类数学家一起，把整个证明过程写成了470万行代码，让证明助手Lean一行一行检查过了。
确认每一步都对，没有漏洞，没有错误。
其中270万行，是AI在最后两周写的。
说人话就是——人类最顶尖的智慧结晶，现在AI不仅能看懂，还能帮着查错、补全、验证。
而且效率高得吓人。 先说说庞加莱猜想是什么。
不用怕，我尽量讲人话。
1904年，法国数学家庞加莱提了一个问题：
「任何一个单连通的、封闭的三维流形，一定同胚于一个三维球面。」
翻译一下。
想象你手里有个气球，不管你怎么捏它、揉它、拉它，只要不把它撕破、不把它粘起来，它终归还是一个球。
二维的情况，我们早就知道是对的。
那三维呢？四维呢？更高维度呢？
这个看起来简单的问题，难住了人类整整一百年。
2000年，克莱数学研究所把它列为「千禧年七大数学难题」之一，谁解出来奖一百万美金。
七个难题，到今天只解开了一个——就是庞加莱猜想。
2003年，俄罗斯数学家佩雷尔曼用「里奇流」的方法证明了它。
然后他拒绝了奖金，隐居了。
这段故事本身就够传奇的了。
但今天这件事，是另一个层面的突破。
佩雷尔曼的证明，虽然数学界大体认可，但里面有很多「显而易见」「读者可自行验证」的地方。
这些地方，人类数学家靠直觉、靠经验、靠同行评议，觉得没问题。
但有没有可能，某个不起眼的角落里藏着一个漏洞？
有没有可能，某一步的推理其实是错的，只是大家都没看出来？
数学史上这种事不是没发生过。
很多被公认了几十年的证明，后来被发现有漏洞，有的甚至被推翻了。
人的脑子是有限的。
一个几百页的证明，要保证每一步都严丝合缝，太难了。
所以有了「形式化验证」这个方向。
就是把数学证明翻译成计算机能理解的代码，让机器一行一行去检查。
机器不会累，不会走神，不会因为「看起来对」就放过。
它只认逻辑。
但这件事说起来容易，做起来难如登天。
庞加莱猜想的证明涉及好几个数学分支——拓扑学、微分几何、偏微分方程……
要把整个证明完整形式化，相当于把一座大厦的每一块砖都拆下来，重新用机器能理解的语言码一遍。
工作量有多大？
470万行代码。
470万行是什么概念？
一个熟练的程序员，一辈子手写的代码可能也就几百万行。
而这是纯数学证明，每一行都要严谨，每一步都不能错。
换在以前，这件事可能要花几十年，甚至根本做不完。
但这次，团队用了AI。
丘成桐的弟子、资深的Ricci流研究者，加上一个刚毕业的本科生，四个人的团队。
前面积累了很久，最后两周，AI帮他们写了270万行。
你没看错。
270万行，两周。
这已经不是效率提升了，这是生产力的跃迁。
这代表什么？
首先，数学研究的方式，可能要变了。
以前，一个数学家一辈子能验证几个大定理？没几个。
现在有了AI，一个小团队，几周就能搞定一个。
以后的数学研究，可能不再是「我想到了一个证明」，而是「我想到了一个思路，AI帮我把细节补全、验证完毕」。
其次，数学的「可信度」会变得不一样。
以前一个证明对不对，靠业内大佬拍板。
大佬说对，大家就认。
但大佬也是人，也可能看错。
以后呢？证明过了Lean这一关，就是真的对。
机器说没问题，就是没问题。
数学可能会变得更「硬」，更不容置疑。
还有更长远的一件事。
如果AI连庞加莱猜想这么复杂的证明都能验证，那它离「自己发现新定理」还有多远？
现在的AI，更多是在辅助——人类给方向，AI补细节。
但总有一天，AI可能会自己提出猜想，自己找到证明路径，自己验证完毕。
到那时候，人类数学家的角色是什么？
是导师？是裁判？还是观众？
这个问题，现在可能还没有答案。
但方向已经很清楚了。
我想起之前看到的一个观点——
AI不会取代数学家，但会用AI的数学家，会取代不会用AI的数学家。
就像计算器出来的时候，有人担心数学家会失业。
结果呢？数学家没有失业，只是计算不再是他们工作的主要部分了。
他们把精力放在了更高级的思考上。
AI可能也是一样。
它不会让数学家消失，它会让数学家变得更厉害。
以前要花十年验证的东西，现在两周搞定。
省下来的时间，可以去想更难的问题。
庞加莱猜想只是一个开始。
千禧年还有六个难题没解决呢。
P=NP？霍奇猜想？黎曼假设？
说不定哪天，AI就帮人类把它们一个一个都攻破了。
到那时候，我们回头看今天。
会发现，2026年9月的这470万行代码，只是一个序幕。
参考资料：
新智元《丘成桐弟子带AI狂写470万行，庞加莱猜想证明首次被机器完整验证！》2026.09.29
克莱数学研究所「千禧年七大数学难题」官方介绍
维基百科「庞加莱猜想」「格里戈里·佩雷尔曼」词条
Lean证明助手官方文档
知乎《庞加莱猜想究竟有多难？》
36氪AI新闻周报「2026年9月第4周」
一件听起来有点穿越的事。
庞加莱猜想，这个困扰了人类一百多年的数学难题，它的完整证明，第一次被机器完整验证了。
不是AI证明了它。
是AI和人类数学家一起，把整个证明过程写成了470万行代码，让证明助手Lean一行一行检查过了。
确认每一步都对，没有漏洞，没有错误。
其中270万行，是AI在最后两周写的。
说人话就是——人类最顶尖的智慧结晶，现在AI不仅能看懂，还能帮着查错、补全、验证。
而且效率高得吓人。
不用怕，我尽量讲人话。
1904年，法国数学家庞加莱提了一个问题：
「任何一个单连通的、封闭的三维流形，一定同胚于一个三维球面。」
翻译一下。
想象你手里有个气球，不管你怎么捏它、揉它、拉它，只要不把它撕破、不把它粘起来，它终归还是一个球。
二维的情况，我们早就知道是对的。
那三维呢？四维呢？更高维度呢？
这个看起来简单的问题，难住了人类整整一百年。
2000年，克莱数学研究所把它列为「千禧年七大数学难题」之一，谁解出来奖一百万美金。
七个难题，到今天只解开了一个——就是庞加莱猜想。
2003年，俄罗斯数学家佩雷尔曼用「里奇流」的方法证明了它。
然后他拒绝了奖金，隐居了。
这段故事本身就够传奇的了。
但今天这件事，是另一个层面的突破。
佩雷尔曼的证明，虽然数学界大体认可，但里面有很多「显而易见」「读者可自行验证」的地方。
这些地方，人类数学家靠直觉、靠经验、靠同行评议，觉得没问题。
但有没有可能，某个不起眼的角落里藏着一个漏洞？
有没有可能，某一步的推理其实是错的，只是大家都没看出来？
数学史上这种事不是没发生过。
很多被公认了几十年的证明，后来被发现有漏洞，有的甚至被推翻了。
人的脑子是有限的。
一个几百页的证明，要保证每一步都严丝合缝，太难了。
所以有了「形式化验证」这个方向。
就是把数学证明翻译成计算机能理解的代码，让机器一行一行去检查。
机器不会累，不会走神，不会因为「看起来对」就放过。
它只认逻辑。
但这件事说起来容易，做起来难如登天。
庞加莱猜想的证明涉及好几个数学分支——拓扑学、微分几何、偏微分方程……
要把整个证明完整形式化，相当于把一座大厦的每一块砖都拆下来，重新用机器能理解的语言码一遍。
工作量有多大？
470万行代码。
470万行是什么概念？
一个熟练的程序员，一辈子手写的代码可能也就几百万行。
而这是纯数学证明，每一行都要严谨，每一步都不能错。
换在以前，这件事可能要花几十年，甚至根本做不完。
但这次，团队用了AI。
丘成桐的弟子、资深的Ricci流研究者，加上一个刚毕业的本科生，四个人的团队。
前面积累了很久，最后两周，AI帮他们写了270万行。
你没看错。
270万行，两周。
这已经不是效率提升了，这是生产力的跃迁。
这代表什么？
首先，数学研究的方式，可能要变了。
以前，一个数学家一辈子能验证几个大定理？没几个。
现在有了AI，一个小团队，几周就能搞定一个。
以后的数学研究，可能不再是「我想到了一个证明」，而是「我想到了一个思路，AI帮我把细节补全、验证完毕」。
其次，数学的「可信度」会变得不一样。
以前一个证明对不对，靠业内大佬拍板。
大佬说对，大家就认。
但大佬也是人，也可能看错。
以后呢？证明过了Lean这一关，就是真的对。
机器说没问题，就是没问题。
数学可能会变得更「硬」，更不容置疑。
还有更长远的一件事。
如果AI连庞加莱猜想这么复杂的证明都能验证，那它离「自己发现新定理」还有多远？
现在的AI，更多是在辅助——人类给方向，AI补细节。
但总有一天，AI可能会自己提出猜想，自己找到证明路径，自己验证完毕。
到那时候，人类数学家的角色是什么？
是导师？是裁判？还是观众？
这个问题，现在可能还没有答案。
但方向已经很清楚了。
我想起之前看到的一个观点——
AI不会取代数学家，但会用AI的数学家，会取代不会用AI的数学家。
就像计算器出来的时候，有人担心数学家会失业。
结果呢？数学家没有失业，只是计算不再是他们工作的主要部分了。
他们把精力放在了更高级的思考上。
AI可能也是一样。
它不会让数学家消失，它会让数学家变得更厉害。
以前要花十年验证的东西，现在两周搞定。
省下来的时间，可以去想更难的问题。
庞加莱猜想只是一个开始。
千禧年还有六个难题没解决呢。
P=NP？霍奇猜想？黎曼假设？
说不定哪天，AI就帮人类把它们一个一个都攻破了。
到那时候，我们回头看今天。
会发现，2026年9月的这470万行代码，只是一个序幕。
参考资料：
新智元《丘成桐弟子带AI狂写470万行，庞加莱猜想证明首次被机器完整验证！》2026.09.29
克莱数学研究所「千禧年七大数学难题」官方介绍
维基百科「庞加莱猜想」「格里戈里·佩雷尔曼」词条
Lean证明助手官方文档
知乎《庞加莱猜想究竟有多难？》
36氪AI新闻周报「2026年9月第4周」