AI with Authority：一个人、五个 Agent、五周，从应用代码到硅片流片

一个四十年的闭环

Jason Hickey 1985 年在 Bellcore 设计 ATM 交换结构，1990 年发了自路由交换网络的定理，1992 年决定转去做 AI——因为软件是瓶颈。AI 那个年代不行，他转去 Cornell 和 Caltech 做形式化验证系统 MetaPRL，一等就是三十年。

2026 年，这两条线终于合拢了。他一个人，用消费级 Anthropic 订阅，指挥五个 AI agent 座位，在五周内完成了：Lean 4 内核级数学形式化（Siegel–Walfisz、Bombieri–Vinogradov、Chen 定理等数论经典结果）+ 经过验证的编译器 + 一颗提交到 Tiny Tapeout 社区流片 shuttle 的 RISC-V 处理器。没有人审阅过任何证明，没有人写过任何 RTL。

Salt 方法：形式验证作为「不可腐蚀的裁判」

这篇论文的核心不是数学成果（作者坦承没有新数学），也不是芯片（还没有实物），而是方法论——Salt 方法。

传统上机器验证是成本项，只有里程碑级项目才负担得起。Hickey 的发现是：在 AI 速度下，机器验证不仅经济，而且是必须的。没有裁判，AI 舰队产出的东西你根本不敢信。

Salt 方法的信条：真理只由机器检查，内核无法检查的用结构化对抗，人类注意力是最稀缺资源。

Figure 1 | Salt 方法概览：六条必须不变量（R1–R6）和六条参考配置建议（A1–A6）。核心信条——真理由机器检查，内核无法覆盖的用对抗，人类只做声明和裁决。

六条必须不变量（R1–R6）+ 六条参考配置建议（A1–A6）。关键设计：

• 内核裁判：所有数学声明经 Lean 4 内核检查，proof kernel 是唯一仲裁者（de Bruijn 准则）。信任基于内核和声明本身，而非产出模型的流利程度。
• 结构化对抗：设计在执行前必须经过「反驳者」agent 的攻击；每个落地结果由未参与产出的第二个 agent 独立见证。
• 人类只做三件事：声明（statement）、设计（design）、裁决（ruling）。系统把一切不可逆操作压缩成一个「准备好的点击」然后停下来。
• 预算硬约束：每个任务先分类定价，预算耗尽必须停止并报告失败，不允许死磨。
• 只追加账本：所有决策、错误、撤回记录为 first-class 数据，错误在源头修正而非下游修补。

五座位舰队架构

Figure 2 | 配置与产物。一个人指挥五个 Agent 座位共享仓库和只追加消息总线，内核作为不可腐蚀的裁判居于其下。每个目标返回五个制品。

五个长驻 agent 座位——协调器、数学、编译器、硅片、证据——共享一个代码仓库和一条只追加消息总线，由一个人指挥。

每个 objective 返回五个制品：实现 P、规约 S、内核检查的证明 ⊢P∈S、对抗性测试 T(P)、证书。人类审查的是 S（规约），永远不审查 P（实现）。

硬件验证链有四段链接：Lean 内核检查（spec→design artifacts）→ SAT 等价性检查（artifacts→Verilog，Verilog→netlist）→ 综合比较。三段链接由三个不同 agent 构建，期间发生了两次分歧，在字节级别对齐——分歧记录在账本中。作者认为这种不均匀性本身是一个发现：它精确映射了小团队在 2026 年验证硬件的边界在哪里。

验证链：从 Lean 内核到硅片边界

Figure 3 | 验证脊椎——一条保管链。从 Lean 4 内核到硅片边界的 SAT 等价性检查，每个链接都有命名的检查器。不同链接由不同 agent 构建。

Figure 4 | 提交流片的设计几何。三组 MAC 岛与各自的序列化器物理交织。上图按功能着色，下图按来源着色——内核生成 vs agent 编写 RTL vs 工具插入。

数学战役：从孪生素数猜想到方法自身的边界

原始目标是孪生素数猜想。结果：猜想仍是定义，不是定理，每个条件结果都明确命名了其假设。但战役过程中形式化了一整套经典数论支柱：

• Siegel–Walfisz 定理
• 大筛不等式
• Bombieri–Vinogradov 定理
• Chen 定理
• Vinogradov 均值定理
• Kloosterman 和的 Weil 界

Figure 5 | 锻造时间线。37 天连续提交，零沉默日。蓝色为数学仓库（2087 次提交），橙色为系统仓库（1379 次提交）。里程碑定理在对应日期标注。产出 Lean 4 代码量为 mathlib 的 29.3%。

更微妙的是：语料库在内核中证明了方法自身的边界——证明了 Maynard 类中没有任何权重能跨过孪生门（M₂ ≤ 2log2 < 2），把一个民间障碍转化成了内核对象。一个能机器检查自身方法边界的研究程序，据作者所知前所未有。

经济学数据

Figure 6 | 经济学面板。(a) 预注册计量窗口：37h21m 人类时间 vs 116h40m 墙钟时间。(b) 沉默窗口分布：43% 提交发生在 ≥1 小时无人值守窗口。

注意：人类时间经过交叉审计，排除了 11 小时 50 分钟的「机器冒充人类」流量（协调 agent 通过终端注入发送指令，在记录层与人类键盘输入不可区分）。因为更小的人类数字更利好论文论点，所以排除是「自利方向」，必须由机器证明——这是学术诚实性的标杆操作。

为什么这很重要

这篇论文回答了一个当前 AI 研究的核心问题：AI 生成的数学/代码能不能信？

答案不是「看模型的解释有多流利」，而是用不可腐蚀的裁判让它变得可以信。Lean 内核检查过的证明，正确性不依赖于任何模型。审查坍缩为两个问题：它检查了吗？声明是预期的那个吗？

Hickey 40 年前想造的那台机器——AI 开发软件——终于被造出来了。但它不是「让 AI 直接写代码」，而是「让 AI 在严格裁判下工作，把人类注意力解放到只做声明和设计层面」。

一个人的五周产出（37 小时人类时间），在形式验证覆盖下，达到了传统上需要专家团队数年才能达到的验证级别——从应用代码到硅片流片的全栈。这改变了机器验证的经济学：从成本项变成了生产力的基础设施。