形式化证明

10 月 6 日，OpenAI 在官方博客发布《Sharing AI progress in mathematics》，把内部前沿模型在开放数学问题上的新成果，连同 Lean 形式化证明脚本一并放上 GitHub。第三方计数口径不一，Unite.AI 称约 722 份手稿，Implicator 记录约 372 项结果；发布当天 OpenAI 还撤回了其中 3 份因符号错误的手稿，修订 14 份。这件事的意义不在「机器又算对了几道题」，而在它悄悄移动了知识权威的位置。 过去我们凭什么相信一份证明 数学史很长一段时间里，知识的传递靠的是证言与声望。审稿人是某位教授，期刊是某个学会，读者凭作者的职位和领域口碑决定「要不要信」。一个结论哪怕写在论文里，别人也得花几周甚至几个月去啃，绝大多数人选择直接接受同行评议这个「制度性信任」。这是一种典型的认知外包：我们不亲自核查，而是信任核查者。 Lean 改变了这件事的受力方向。证明被翻译成机器可逐行检查的代码，编译器不认识作者，不在乎你是不是院士，它只做一件事：这一步逻辑推导是否合法。人不再需要「相信」模型，也不再需要「相信」某个审稿人，只需要跑一遍类型检查。 信任的底座从人迁到了机器 这带来一个温和却深远的后果：在可形式化的领域，知识的最后一公里校验，从社会过程变成了工程过程。 过去是「同行评议通过，所以为真」；现在是「类型检查通过，所以为真」。 过去错误可能潜伏多年才被发现；这次 OpenAI 自己撤回 3 份，恰恰说明形式化让错误暴露得更快。 过去「复现」是对实验科学的要求；现在「复算」成了对数学的默认配置。 需要保留的冷静是：并非所有数学都能立刻形式化，直觉、猜想、框架性理解仍然是人的领地。Lean 验证的是「结论对不对」，不是「这个结论为什么重要」。 这对硅基与碳基关系的暗示 当一份知识的可信性由一段人人可跑的代码背书，碳基与硅基之间第一次有了一种双方都无法作弊的共同语言。人类不必再争论模型是不是「真懂」，模型也不必借人类的权威来背书自己。能被审计的，才配叫进展；能被检查的信任，才是下一个时代的认知底座。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：可验证证明与认知信任 💬 更多交流内容，请点击本站论坛交流区：silicon-agi.com

三百年的悬案，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能独立完成一项需要世界顶尖水平的科研时，“科研生产力"的定价逻辑就要重写了。 💬 更多交流内容，请点击本站论坛交流区：silicon-agi.com