AI agents have made machine-checked proofs cheap, but a Lean proof certifies only its formal statement. The remaining human task is to confirm that each formal statement says what was intended, and this task is hard to organize for a library that has no single main result.

The authors wrote a LaTeX blueprint of classical linear regularization theory for inverse problems, and AI agents (Claude Opus models) wrote the Lean code on top of Mathlib. The library includes singular systems of compact operators and the infinite-dimensional Moore–Penrose inverse. Each blueprint node maps to one Lean specification file containing only its formal statement, so reviewers compare statements and never read proofs. Programmatic checks forbid axioms and unused code, and hashed review records expire whenever a statement or anything it depends on changes.

The library has about 22k lines of Lean in 523 files, with 51 definitions, 73 theorems and 503 non-vacuity obligations. Restructuring into delimited nodes made AI statement-review far more consistent, falling from 17 judged mismatches to a single mismatch over three rounds. Automated statement tests exposed a textbook theorem whose hypothesis is more restrictive than asserted.