一组数字先摆在这儿：11天，约1300万行代码，约30300个定理，约60亿个输出Token。
这是Anthropic在当地时间9月4日公布的一份成绩单——Claude完成了费马大定理的首个端到端、可由计算机完整检查的形式化证明。9月5日，凤凰网科技、36氪、量子位等媒体跟进报道，这条消息也挂上了知乎热榜。很多人第一反应是"AI证明了费马大定理？"，但我把几篇报道对照着看完之后，发现真正值得咂摸的不是这句话，而是另一件事。
先说清楚：Claude没有"证明"费马大定理
费马大定理本身早就被证明了。1637年，法国数学家费马在书页空白处写下那个著名的论断：当整数n大于2时，方程xⁿ+yⁿ=zⁿ没有正整数解，还补了一句"我确信已发现了一种美妙的证法，可惜这里空白的地方太小，写不下"。这个命题折磨了数学家350多年，直到1993年英国数学家怀尔斯第一次公开宣布证明，随后审查发现存在关键缺口，他又和理查德·泰勒花了大约一年修补，才在1994年真正完成——一份长达129页的证明。
Claude这次做的，不是重新发现这条证明路线，而是另一件工程量同样惊人、但长期没人愿意干的活：形式化。
什么叫形式化？人类写的数学证明是给同行看的，满纸都是"易证""显然可得"，读者脑子里自动补全跳过的步骤。但Lean这种证明助手不吃这套——它是一台"超级严格的编译器"，每一步推导都必须明明白白写出来，逐行接受计算机检查。把129页"写给人看"的证明翻译成"写给机器查"的形式，还要补上所有被省略的环节，Anthropic此前预计这项工程需要数年。
Claude用了11天。
真正的分水岭：AI开始接管"没人想干的活"
据量子位、智东西的报道，这次不是一个Claude在战斗，而是数十个Claude智能体并行协作，项目由Anthropic研究员彭天翼发起——他本科毕业于清华姚班，博士毕业于麻省理工，现在是哥伦比亚大学商学院助理教授。团队用有向无环图记录定理之间的依赖关系，让多个智能体分头去啃概念定义、中间定理和复杂命题。最终产出的代码量超过Lean核心数学库Mathlib的5倍，是迄今规模最大的Lean证明项目，整个证明只用了Lean的3条标准公理。
我觉得这件事比"AI更聪明了"重要得多，原因有两层。
第一层，这是验证，不是生成。生成内容的AI已经满天飞了，写文案、画图、编代码，产出快但真伪要靠人把关。而这次Claude干的是反方向的事：把人类产出的东西，转化成机器能百分之百核验的形式。Google DeepMind AGI Economics负责人Alex Imas的评价很到位：这是他见过对数学领域最重要的AI成果之一，自动化形式化本身就是加速数学进展的能力。换句话说，AI的价值正在从"帮你写"扩展到"帮你确认写得对"。
第二层，它暴露了人机协作里最贵的成本——"显然"的鸿沟。人跟人沟通可以靠默契跳步，人跟机器协作一步都不能省。数学界如此，日常工作也一样：你给AI一句"帮我写个方案"，它给你一份看着没毛病的文档，但里面多少环节是它替你"显然"掉的，只有让它逐条列出来检查时才知道。
一个你今天就能做的实验
不需要懂Lean，也不需要会证明定理，这个思路普通人马上能用：让AI当你的核验员，而不是写手。
做法很朴素：把一份你已经完成的文档——周报、报价单、活动方案都行——发给AI，要求它"不要改写，只逐条列出这份材料里所有没有依据的断言、前后矛盾的地方和缺失的前提"。你会发现，让它从零生成一份新东西，它擅长；让它对着一份现成的东西挑毛病、补漏洞，它同样擅长，而且后者往往才是你真正缺的那道工序。做完一轮核验，再把挑出的问题逐条修掉——这比反复让它重写，产出质量高得多。
AI接管不了你对结果的最终判断，但它完全能接管"把每一步摊开检查"这种枯燥又容易出错的活。350年的数学悬案都能被拆成1300万行逐行验证，你手头那份文档的逻辑漏洞，没理由揪不出来。
💬 评论