What is Lean?

Lean 4 is a programming language and proof assistant. This lesson builds the mental model you need before writing real code.

Three Roles in One Tool

Lean is simultaneously a compiler, an interactive proof assistant, and a library ecosystem. You can define programs, prove properties about them, and reuse thousands of verified results from the Lean community.

Why Engineers Care

Lean allows you to express guarantees directly in types. That means fewer runtime checks and more compile-time certainty.

1-- A type can express a contract
2structure User where
3  name : String
4  age : Nat
5
6-- A function can promise more than its inputs
7-- (we will learn how to prove such promises later)
8-- def sortedInsert : SortedList α → α → SortedList α

Why Mathematicians Care

Lean turns a proof into executable code. Every proof is checked by a small trusted kernel, making it extremely hard to miss a logical gap.