Definition
Plain language
A programming language for writing math proofs where the computer refuses to accept any step that doesn't logically follow.
As stated in the literature
A dependently-typed proof assistant whose compiler accepts only programs that constitute valid formal proofs; the verification substrate used by AlphaProof, the DeepMind Erdős work, and most current AI-driven formal mathematics.
Also called: Lean 4
Why it matters: It gives AI math systems an external, unforgeable judge of correctness, so claimed proofs can be checked rather than just trusted.
For example, a proof of the irrationality of sqrt(2) in Lean is only accepted if every algebraic step is justified by a previously proved lemma or axiom.
Heard on the show
“You make the AI write its proofs in Lean.”Episode 067 — An AI Just Solved a 1996 Erdős Problem—and the Simplest Agent Won