The Proof in the Code

Why it’s on the list: Kevin Hartnett’s inside history of Lean, the proof assistant that machine-checks mathematics — begun as a tool for formally verifying software, adopted by mathematicians as proofs grew too long to trust by hand, and now the substrate AI systems use to produce verifiable proofs.

Where I heard about it

• Paras Chopra on X (Oct 10, 2026) — “as niche as it can get,” and inspiring for showing how a single person’s humble v0.1 can compound into a community that changes history within a decade.

Connections

• This book is as niche… (tweet) — the recommendation.
• Terence Tao — the mathematician most associated with Lean formalization projects.