# AI with Authority, from Application to Silicon

arXiv: https://arxiv.org/abs/2608.21356 · HTML: https://mlsanity.com/paper/2608.21356/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 29 references that are in the map.
- First posted on arXiv 21 Aug 2026.

## Builds on (most cited first, 3 of 3)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research](https://mlsanity.com/paper/2606.13306/) (2026)

## Abstract (arXiv)

For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productivity --- it is the incorruptible referee that lets one person safely direct autonomous machine work at scale. In five weeks, one researcher on consumer AI subscriptions directed a small fleet of AI agents from application code, through a verified compiler and executive, to a RISC-V processor taped out on a community silicon shuttle; no proof passed through human review, and no RTL was written by a human. The working discipline --- the Salt method --- rests on a proof kernel no hallucinated proof can pass: mathematical claims travel between agents as kernel-checked artifacts, and human attention is reserved for statements, designs, and rulings. Verification is stated link by link, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary. We publish the complete accounting: theorem provenance, a pre-registered token meter, floor-bounded human time, and an error ledger whose catch numbering runs to #256 --- a monotone counter over the mathematics campaign's append-only flags ledger, maintained 2026-07-07 to 2026-07-20 (one number, #79, was never assigned; later catches are recorded un-numbered) --- against zero incorrect proofs reaching the record.