Loading…
Glossary term
An interactive theorem prover in which mathematical proofs are written so a computer can check every step.
Lean is a programming language and interactive theorem prover. A mathematician writes a statement and a proof in Lean's formal language, and the system checks every logical step, accepting it only if it is entirely valid.
A growing library called mathlib collects formalized mathematics.
A tiny Lean 4 theorem
theorem add_comm_example (a b : Nat) : a + b = b + a :=
Nat.add_comm a bA Lean-checked proof is verified by machine, which is why AI math results are often accompanied by Lean formalizations, though the formal statement must still match the intended claim.