AI with Authority, from Application to Silicon
Not on the map. Why?
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.
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
3 of 29 references.
References · 3
- 2019The Lean mathematical librarycited by 134
- 2015A formal proof of the Kepler conjecturecited by 42
- 2026EconCSLib: AI-Assisted Lean Formalization for Economics & Computation researchcited by 7
Built on by
Not cited yet.