Why Lean Matters: Formal Verification Meets AI Code

The core signal. Formal verification is becoming practical for mathematics and software, with Lean at the center. Kevin Hartnett's book traces Lean from its creation by Leonardo de Moura at Microsoft Research to its adoption by mathematicians like Kevin Buzzard and fields medalists. The key tension: machine-checked proofs guarantee correctness of derivation, but cannot verify the definitions match human intent.

The proof crisis. Thomas Hales's proof of Kepler's conjecture was accepted only with 99% confidence because no one could manually verify the 1,767 computer programs. This drove Hales to formalize his proof in Lean, consuming 20 person-years. The story shows how traditional review breaks down for complex, computation-heavy proofs and why formalization is the only reliable path.

The library that grew. Mathlib, Lean's mathematical library, was built by a decentralized community starting with basic definitions like complex numbers. Buzzard treated it as an undergraduate to teach. The formalization of perfectoid spaces showed Lean could handle frontier math. This barn-raising effort now contains most of undergraduate and first-year graduate mathematics, plus spikes to research frontiers.

AI enters the ring. DeepMind's AlphaProof used Lean to achieve silver-medal performance at the 2024 International Mathematical Olympiad. OpenAI's models later resolved open Erdős problems, with results checked in Lean. But auto-formalization creates a spaghetti monster: AI generates Lean proofs that work but lack conceptual elegance, making them hard to maintain or understand.

The formalization gap. A checked proof can prove the wrong theorem if the formal definition misrepresents the human intention. Kevin Buzzard's team found errors in theorems by four Fields medalists in top journals — slips like missing conditions that experts implicitly assume. The trust moves from checking the proof to checking the specification. This mirrors the software challenge: verified code is useless if the spec is wrong.

What engineering leaders should watch. The bottleneck in AI-assisted development is shifting from generation to verification. Projects like Kim Morrison's Lean verification of zlib show AI can produce verified code, but only if specifications are comprehensive. Formal verification tools are maturing — Lean's kernel is small and auditable — but the hard work is now writing precise specs. Teams should budget for specification design and invest in verification pipelines to maintain trust as AI code volume grows.