形式化证明

三百年的悬案，300页的天书 1637年，费马在书页边上写下一句批注：“我发现了一个绝妙的证明，但这里空白太小写不下。“这个关于"当n>2时，a^n+b^n=c^n没有正整数解"的命题，从此困住了数学界358年。 1994年，怀尔斯用椭圆曲线和模形式的现代工具完成了人类证明，写满了100多页的天书级论文，全世界能完全读懂的人不超过两位数。但这份证明有一个软肋：它依赖大量人脑推演，从未被计算机完整形式化验证过。 2026年9月，Anthropic的Claude把这件事做完了——而且是基本自主地，跑了11天。 11天意味着什么 Claude这次完成的，是首个端到端的计算机验证形式化证明：从理解怀尔斯证明的整体结构，到把每一个逻辑环节翻译成Lean定理证明器能检查的形式，再到修补翻译过程中暴露的漏洞——全程由模型主导，人类只在关键节点介入。 11天的无人值守运行，背后是一套严格的长程自主科研（long-horizon autonomous research）能力： 自我分解：把300页证明拆成成百上千个待证子目标； 失败回溯：某一步卡住时，不是死磕，而是回退、换路径； 资源调度：在多个Lean会话之间分配算力，优先攻克关键路径； 自我校对：把已验证的部分当作新的引理库，复用到后续步骤。 数据来源：Anthropic形式化证明技术报告，2026年9月 这与Navier-Stokes那篇形成了有趣的对照：OpenAI用的是"一万个智能体并发"的暴力集群路线，Anthropic走的是"单个系统长时间自主"的深度路线。两条路在同一个月里各自抵达了形式化证明的里程碑——这不是巧合，而是说明AI科研的两条工程范式已经同时成熟。 为什么"形式化"比"写出证明"更重要 怀尔斯的证明是人写的，人相信它，是因为同行评审——几十个顶尖数学家花了几年，互相挑错、互相补漏。但人会累、会漏看、会在长达300页的推导里悄悄放过一个隐藏假设。 形式化证明不同。Lean会逐行检查：每一个引理是否真的被前置条件支撑，每一个定理的调用是否合法。它不懂"这看起来对”，它只认逻辑链条。 Claude把费马大定理做成形式化证明，等于给这座1994年建成的理论大厦做了一次全结构探伤。结果是：结构成立。这给整个数论的现代体系吃了一颗定心丸。 对"AI会不会取代数学家"的再思考 这次工作也给"AI替代论"泼了一盆冷水，同时加了一把火： 火：那些已经被人想清楚、但极其繁琐的证明工程，AI现在能独立干完。怀尔斯证明的形式化，过去估计要一个团队干五年，Claude用11天跑完了。 冷水：AI并没有提出怀尔斯的核心洞察——椭圆曲线与模形式的联系。那个跨越世纪的灵感，仍然是人脑的产物。 更准确的说法是：AI接管了证明的"施工”，但"设计图"仍然由人绘制。 数学家的价值正在从"推细节"转向"选问题、搭框架、判断方向"。 行业影响与展望 形式化证明一旦便宜到这个程度，受益的不只是数学：编译器验证、芯片设计正确性、密码学协议安全性，这些原本依赖昂贵人工审计的领域，都会被AI形式化工具重塑。 Anthropic这次11天自主科研，也给"AI Agent做长任务"树立了新标杆。过去的Agent演示多是几分钟、几十分钟的网页操作；能连续11天朝一个科研目标推进、自我纠错、最终产出可验证成果，这是从"工具"到"研究员"的关键一跃。 guijiagi.com会持续跟踪这条线：当AI能独立完成一项需要世界顶尖水平的科研时，“科研生产力"的定价逻辑就要重写了。