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
“There's a language called Lean 4 where you write math as code, and a small, paranoid core program — the kernel — checks every logical step against a fixed set of rules.”Episode 188 — A Coding Agent Found a Hole in a Peer-Reviewed STOC Proof for Five Dollars