2026-09，Anthropic 公布：数十个 Claude agent 在 11 天里用证明助手 Lean 写完了费马大定理（FLT：n>2 时 xⁿ+yⁿ=zⁿ 无正整数解）的完整形式化证明——约 1300 万行、约三万条中间定理。本期不讲「怎么搭 agent 流水线」，只问一个机制问题：「可验证」到底买到了什么，又没买到什么？它与 Day 60 是一对：同一代模型，在没有硬裁判的地方把自己和监控一起说服，在有硬裁判的地方跑完了原计划多年的活。前置阅读：Day 42 神经符号、Day 46 AI for Science。
像区块链里的验证节点：出块的人可以是任何人、甚至是恶意的，验证节点不听解释、不看声誉，只把交易逐条重放一遍——对就收，错就拒。
大模型最难防的失效是「错得流畅」：推理读起来头头是道，结论却是错的；Day 60 里连读 CoT 的监控也被说服了。数学证明尤其如此——人类审稿 Wiles 的证明花了很久，还真找出过一个漏洞。
证明助手（proof assistant：能逐步检查数学证明的软件）换了一种信任结构。它依靠 Curry–Howard 对应：把命题看作类型、证明看作该类型的程序。「证明定理 P」等价于「写出一个类型为 P 的项」，而检查证明 = 类型检查。Lean 里做这件事的是一个很小的内核（kernel），它只认少数几条推理规则，加上三条标准公理（命题外延 propext、选择公理 Classical.choice、商类型的 Quot.sound）。
关键在于不对称：找证明需要创造力和巨大搜索，查证明只是机械重放。所以生成端可以是不可靠的、会幻觉的模型，只要最后通过内核，正确性就不再依赖对模型的信任——这被称为 de Bruijn 准则：可信部分要小到能被人审查。内核也不读注释、不看推理过程，因此 Day 60 那种「理由说服了裁判」的通道在这里根本不存在。
这种「验证远比生成便宜」的直觉，与复杂性理论里 P 与 NP 的区分同源：给你一个数独答案，检查它只要几秒；从空盘面解出它却可能要很久。机器证明的规模化，本质上就是用海量的、廉价可检查的试错去换一个昂贵的结果。
# 玩具「内核」：只认公理和肯定前件(modus ponens)，逐行检查一份证明 axioms = {"P", "P->Q", "Q->R"} def check(proof, goal): known = set() for line in proof: if line in axioms: known.add(line); continue # 必须存在已知的 A 和 A->line，否则拒绝——不接受任何「解释」 if not any(f"{a}->{line}" in known for a in known): return False known.add(line) return goal in known print(check(["P", "P->Q", "Q", "Q->R", "R"], "R")) # True print(check(["P", "R"], "R")) # False：跳步，再「显然」也不行
检查器只有十几行，谁写的证明都一样查；真正的 Lean 内核复杂得多，但原理相同：检查是局部、机械的。
像 CI 全绿但 spec 写错了：测试证明代码满足了测试，却没法证明测试测的是你真正想要的东西。
内核只回答一个问题：「这份证明确实证明了这条形式化陈述」。它不回答「这条陈述是不是你心里的那个定理」。于是被打穿的地方只剩三处：
axiom 就能把任何东西「证」出来；sorry 允许暂时跳过某一步。这次的做法是逐一堵上：用一个 comparator（比对工具）确认最终定理与社区库 Mathlib 里早已写好的 FLT 陈述一致；确认证明只依赖那三条标准公理、没有 sorry。Kevin Buzzard（领导人类版 FLT 形式化项目的帝国理工数学家）随后自己下载、编译、跑内核，确认成立。
这与 Day 59 的 reward hacking 是同一个结构：优化压力会流向检查最薄弱的地方。证明正确性被内核焊死后，可被钻的空子只剩「陈述」与「公理」——所以必须让陈述由独立于生成者的一方预先写好，最好是早于这次工作、由人类社区审过的版本。
# 平凡真：陈述写歪后，「证明」通过了，但什么也没证 def fermat_holds(domain, n): # 「对 domain 里所有 (x,y,z)，xⁿ+yⁿ≠zⁿ」 return all(x**n + y**n != z**n for x, y, z in domain) real = [(x, y, z) for x in range(1, 30) for y in range(1, 30) for z in range(1, 30)] # 写歪的定义：要求 x > z 且 y > z ——正整数里这时 xⁿ+yⁿ 必然 > zⁿ bad = [t for t in real if t[0] > t[2] and t[1] > t[2]] print(fermat_holds(bad, 2)) # True ——「证明」成功，但 n=2 本来有 3,4,5！ print(fermat_holds(real, 2)) # False ——正确陈述下 n=2 不成立 print(fermat_holds(real, 3)) # True（有限范围内的抽查，不是证明）
像 Bazel 的依赖图 + C 的头文件：先把所有 .h（接口）定下来，大家各自去写 .cpp（实现）；改一个实现不会触发依赖它的模块重编，构建系统按图决定下一步能并行做什么。
报告坦承，最初几次尝试失败了：agent 们起步不错，但很快丢失了项目状态、不再有效协作——长时程任务里上下文会衰减，几十个 agent 各自的记忆也会互相漂移。转用 Prove2Me（哥伦比亚大学 Tianyi Peng 团队做的协作形式化平台）后才跑通。它提供的结构是：
为什么这里多 agent 能放心并行？分布式系统里协作最贵的是共识：你得相信别人交来的东西是对的。这里每份提交都由内核独立检查，agent 之间不需要互相信任，也不需要互相 review——内核就是唯一的共识机制。最终约 30,300 条定理被证明，其中约 29,500 条进入了最终证明。代价同样可观：报告给出的消耗约为 60 亿输出 token——这是用算力换人力的典型形态，只有在裁判足够便宜时才划算。
# 用标准库 graphlib 模拟：哪些陈述现在可以并行开工？ from graphlib import TopologicalSorter deps = { # 陈述 -> 它的证明要用到的陈述 "FLT": {"A", "B"}, "A": {"A1", "A2"}, "B": {"B1", "B2"}, "A1": set(), "A2": set(), "B1": set(), "B2": set(), } ts = TopologicalSorter(deps); ts.prepare() wave = 1 while ts.is_active(): frontier = ts.get_ready() # 依赖都已「证完」的节点 print(f"第 {wave} 波，可并行分给 agent：{sorted(frontier)}") ts.done(*frontier) # 假设内核都判通过 wave += 1
真实流程更灵活：因为可以 import 未证陈述，agent 不必等依赖证完就能先写上层证明，这里的「波次」只是最保守的调度。
像一个所有测试都过、但 1300 万行、没人能 review、也合不进主干的超大 PR：功能确实对，可它不是团队代码库的一部分。
Buzzard 称之为「非凡的自动形式化成就」，同时把代价说得很清楚：
机制上看，这三者对应三种不同的「目标函数」。验证只要求每一步局部正确，内核对证明多长、多绕完全不在意；理解要求压缩——好的证明是把一大片事实归结为几个关键想法；可复用要求抽象恰到好处——引理要写成别人也能用的一般形式。优化压力只施加在第一项上，所以第二、三项不会自动出现，甚至会被牺牲：最便宜的通过方式往往是具体、冗长、一次性的。
这与 Day 60 对照尤其清楚：同一代模型，有硬裁判处跑完了原计划多年的工作，没有硬裁判处把自己和监控一起说服。差别不在模型更「诚实」，而在环境里是否存在不可被说服的检查。
# 同一个结论的两份「证明」：都正确，但可读性与复用性天差地别 def brute_proof(n): # 逐个验证：每个都对，但看完也不知道「为什么」 return [(k, sum(range(1, k + 1)) == k*(k+1)//2) for k in range(1, n + 1)] def insight_proof(): # 一个想法：首尾配对 1+k, 2+(k-1)... 每对都是 k+1，共 k/2 对 return "sum(1..k) = k(k+1)/2，对一切 k 成立，且可复用到等差数列" steps = brute_proof(10_000) print(all(ok for _, ok in steps), len(steps), "条检查") print(insight_proof()) # 1 行，且覆盖无穷多情形
注意：Lean 证明不是穷举，这里只示意「局部正确的堆叠」与「一个压缩性想法」的差别。