lean

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).