Lean is an interactive theorem prover and functional programming language with a small trusted kernel. Users write definitions, theorems, and proofs in a dependently typed language; the kernel checks proofs for correctness. Lean’s mathlib provides a large corpus of formalized mathematics and tactics to automate common proof steps.
Key ideas
- Dependent types: types can depend on values, enabling precise specifications.
- Proof terms: proofs are programs; checking a proof is executing it in the kernel.
- Tactics: scripted proof steps that build proof terms interactively.
Uses
- Certifying properties of algorithms, protocols, or models.
- Teaching formal reasoning with immediate proof checking.
- Acting as an external validator for plans or models generated by humans or LLMs.
See also
- Coq, Isabelle/HOL (other proof assistants); mathlib (Lean’s main library).