Lean Theorem Prover
Definition
Lean is an interactive theorem prover and functional programming language for writing machine-checked definitions, proofs, tactics, and formalized mathematics. Lean proofs may be written as direct proof terms or through tactics that elaborate into proof terms checked by the kernel.
Why It Matters
Lean is a practical bridge from Higher-Order Logic, type theory, and constructive proof ideas into executable formal verification work. It matters for Formal Methods because it can make mathematical claims, algorithms, and proof obligations precise enough for a machine to check.
Formalism / Key Objects
- Propositions are represented as types, and proofs are terms inhabiting those proposition-types.
- A direct proof-term style can construct conjunctions explicitly, for example:
And.intro (And.right h) (And.left h)- Tactic scripts are an interactive surface language that manipulates goals and hypotheses, but the resulting proof must still elaborate to a kernel-checkable term.
inductivedeclarations introduce datatypes and propositions with constructors and recursors.structuredeclarations package fields into named records, which are heavily used in mathematical hierarchy design.- Type-class instance arguments such as
[Group G]let Lean infer algebraic structure from context. - Lean metaprogramming and tactic writing use Lean itself to build proof automation.
- Lean Proof Terms and Tactics records the proof-judgment and proof-term schema behind this workflow.
Connections
- Higher-Order Logic and dependent type theory provide the conceptual background for Lean’s typed terms and proof objects.
- Intuitionistic Logic is relevant through Curry-Howard-style proof interpretation, though Lean can also use classical axioms when imported.
- Second-Order Logic is adjacent but not identical: Lean’s type-theoretic foundation is richer than a bare second-order language.
- Formal Methods can use Lean for mechanized theorem proving, verified algorithms, and formalized mathematical infrastructure.
Common Confusions
- Lean is not only a tactic language; tactics are one interface for constructing proof terms.
- Mathlib-style formalization requires understanding both mathematics and Lean’s type-class/structure conventions.
- Lean metaprogramming is a different skill from using Lean to prove mathematics, even though both happen inside the same ecosystem.