Lean 4

Dependent types, propositions as types, formal verification

Vector n α Fin n Prove 2+2=4 Dependent function Type classes Inductive proof

Lean 4 Editor

Type Checker Output

Select an example to begin.

Lean 4 Key Ideas

Propositions as types: P : Prop means P is a type; a proof of P is a term of type P
Curry-Howard: → is function type, ∧ is product, ∨ is sum, ∀ is dependent Π-type
Universe hierarchy: Type 0 : Type 1 : Type 2 ... avoids Russell's paradox
Dependent type: type that depends on a value — e.g. Vector n α depends on n : Nat
Tactic mode: by intro h; exact h — like Coq but with Lean 4 syntax