358年没人能推翻的定理，129页纸的人类证明，如今被AI改写成1300万行机器可验证代码。2026年9月4日，Anthropic宣布Claude用11天完成费马大定理的首个端到端Lean形式化证明，证明代码同步开源。数学界等了几十年的里程碑，这次由一个模型交付。
11天到底做了什么
费马大定理是数学史上最著名的难题之一。皮埃尔·德·费马在1637年写下这条猜想，此后358年间无数数学家折戟。1995年，安德鲁·怀尔斯拿出129页的完整证明，人工审稿就耗费了数月。
Anthropic的项目目标是明确的：把怀尔斯的既有证明逐行改写成Lean 4代码，交给计算机逐步检查，做到端到端、可机器验证。Claude自主运行11天，写下约1300万行Lean代码，人类只提供了少量高层指导。
需要划清一条边界：Claude没有提出新的证明路线，它做的是验证工程的极限挑战。把一个依赖代数几何、椭圆曲线、模形式的巨型证明完整数字化，此前数学界估算是数年到数十年的工作量。11天跑完，这是AI在长程任务上的能力标尺。
为什么这件事比跑分重要
大模型评测分数看腻了，形式化证明是少数无法造假的战场。Lean编译器不会给面子，每一行代码要么通过检查，要么报错。1300万行代码全部通过，意味着证明的每一步逻辑都经得起机器复核。
对数学界，这件事的分量在工具层面。形式化验证长期卡在人力成本上：一个重要定理的形式化往往需要团队数年。Lean社区耕耘十年，累计形式化的数学库仍只覆盖一小部分主流成果。AI把形式化速度拉高几个数量级后，数学知识的机器可验证化有望从奢侈品变成基础设施。
对AI行业，这是长时自主任务的又一实锤。2026年模型竞赛的关键词已经换成”能连续干多久”。OpenAI的Codex上云后主打常驻工作流，Anthropic此前展示过Claude连续工作14小时的编程能力。这次是11天的数学工程，赛道从写代码扩展到了科研级任务。
另一场实验：950个Agent扫了19亿蛋白质
同月，Anthropic的生物学团队交出另一份成果。949个Claude Agent会话组成集群，在21.5小时的自主运行中消耗约2.156亿Token，扫描约19亿个蛋白质集群、提取20万个逆转录酶候选。过程中一个Agent在原始DNA序列旁发现了串联重复序列，随后被确认为新型酶系统ART，结构与CRISPR类似。最终报告压缩成19份交人类评审。
这项工作的意义在于流程：AI负责海量筛选和初步判断，人类只在关键节点介入。预印本已发布，这是”大模型+湿实验室”路线交出的第一个硬成果。
冷静看边界
两个案例都不是”AI取代科学家”。费马大定理项目站在怀尔斯证明的肩膀上，ART系统的功能至今没有完全确定。OpenAI智能体集群9月给出的Navier-Stokes奇点解也因署名争议发酵，说明AI深度参与科研后，学术规范还没跟上。
真实的变化在协作结构。数学家验证一个证明要数月，Lean编译器几分钟；Agent筛20亿蛋白质，人类学者一辈子读不完这个量。AI承担的是”算力和耐心的部分”，判断力和问题定义仍握在人类手里。
给从业者的三个判断
一，长时自主Agent已进入实用区间。11天、1300万行、零人工逐行干预，这套工程能力会很快复制到软件、法律、金融审计等重验证场景。
二，形式化验证是下一个确定性机会。Lean、Coq相关人才稀缺，AI大幅降低门槛后，可验证软件的需求会先行爆发。
三，关注”AI产出+机器验证”的组合拳。单纯让AI生成内容已不值钱，让生成结果自带可验证性，才是2026年之后科研和工程的主流工作流。
费马大定理被改写成代码只用了11天。下一个358年的难题，等待时间可能会短得多。
苏公网安备32010502011527号
发表回复