权威AI，从应用到芯片

六十年来，机器验证一直是一项主要的成本开销，只有特殊的工件才能负担得起。在这里，我们报告生成式人工智能颠倒了这种关系：在人工智能的速度下，机器验证不仅经济，而且对生产力至关重要——它是一个廉洁的裁判，可以让一个人安全地指导大规模的自主机器工作。五周内，一位消费者人工智能订阅研究人员指导一小群人工智能代理从应用程序代码，通过经过验证的编译器和执行程序，到在社区硅航天飞机上流片的 RISC-V 处理器；没有证据经过人工审查，也没有 RTL 是由人工编写的。工作原理——Salt 方法——依赖于一个证明内核，任何幻觉证明都无法通过：数学主张作为内核检查的工件在代理之间传播，而人类的注意力则保留在陈述、设计和裁决上。从 Lean 4 内核到硅边界处 SAT 检查的等效性，验证是逐个链接进行说明的。我们发布了完整的会计：定理出处、预先注册的词元计、有底限的人类时间，以及一个错误分类账，其捕获编号运行到#256——数学运动的仅附加标志分类账上的单调计数器，维护于2026年7月7日至2026年7月20日（一个数字#79从未被分配；后来的捕获记录为未编号的）——反对零个错误证明达到记录。