–
Lean 4 is simultaneously an interactive theorem prover, a dependently typed functional programming language, and a compiler toolchain. The official reference describes Lean as an interactive theorem prover based on dependent type theory; the Lean 4 system paper describes it as an extensible theorem prover and efficient functional programming language; the repository itself is explicitly “the repository for Lean 4” and links the theorem-proving tutorial, functional-programming book, and language reference as first-class documentation. citeturn6view0turn22view1turn5view0turn0search0
The core idea is propositions-as-types and proofs-as-programs. A proposition is a term of type Prop; a proof of proposition p is just a term t : p. Implication is a function type, so a proof of p → q → p is literally a function that takes a proof of p, a proof of q, and returns the first one. Lean’s proof language is not a separate logic bolted onto programming syntax; it is the same dependent type theory used for ordinary definitions. citeturn8view0turn19view0
example (p q : Prop) : p → q → p :=
fun hp hq => hp
To work effectively, separate five layers in your head. Computation is reduction or evaluation of terms. Type checking verifies that a term inhabits a type, using definitional equality. Elaboration turns surface syntax into core terms, filling in omitted arguments, expanding macros, inserting coercions, and running type-class search. Tactics are proof-state programs that construct proof terms. Kernel verification is the final trusted check that the elaborated proof term obeys the core rules of the type theory. Lean’s reference is explicit that elaboration transforms user-facing syntax into a simpler core theory, tactics construct proof terms behind the scenes, and the kernel checks those terms. citeturn22view0turn6view1turn19view0
The small trusted kernel matters because most of the pleasant tooling is not trusted. Macros, elaborators, tactics, the equation compiler, and recursive-definition machinery can all be buggy; the design goal is that bugs there should cause rejected proofs or confusing diagnostics, not accepted false theorems. The reference and system paper both emphasise a minimal kernel and independent validation paths, and the theorem-proving text notes that pattern matching and recursive proofs are compiled down to primitive recursors outside the trusted code base and then checked by the kernel. citeturn6view0turn19view0turn10search5turn10search6
Lean programs are built from def, inductive, structure, class, instance, match, let, lambdas, and namespaces. Definition-like commands include def, example, theorem, and opaque; they elaborate a term against a signature, and—except for example, which is discarded—save the resulting core expression in the environment. Inductive types are Lean’s primary mechanism for introducing data; structures are a special case of inductive types with exactly one constructor. citeturn9view4turn2search7turn13view0
def inc (n : Nat) : Nat := n + 1
def head? {α : Type} : List α → Option α
| [] => none
| x :: _ => some x
def sum : List Nat → Nat
| [] => 0
| x :: xs => x + sum xs
def mapOption {α β : Type} (f : α → β) : Option α → Option β
| none => none
| some x => some (f x)
def compose {α β γ : Type} (f : β → γ) (g : α → β) : α → γ :=
fun x =>
let y := g x
f y
If you know Python, the largest shift is that Lean is expression-oriented, immutable by default, and total by default. If you know Scala or an ML-family language, Lean’s inductive declarations feel closer to algebraic data types or enum/sealed-sum encodings than to OO classes. Pattern matching is the standard way to consume inductive data, and recursive functions are expected to be structurally recursive unless you provide a termination argument. Lean also enforces exhaustiveness of match, which rules out silent fall-through partial functions. citeturn13view0turn13view1turn21view0
inductive Tree (α : Type) where
| leaf
| node (left : Tree α) (value : α) (right : Tree α)
structure User where
name : String
retries : Nat
def defaultUser : User :=
{ name := "alice", retries := 3 }
class Size (α : Type) where
size : α → Nat
instance : Size User where
size u := u.retries
def retryBudget {α : Type} [Size α] (x : α) : Nat :=
Size.size x
structure gives you product types with generated projections; class participates in type-class inference; instance declarations are syntactically almost the same as definitions. In practice, class plus instance is Lean’s ad-hoc polymorphism mechanism, roughly analogous to Scala type classes or given/implicit search, not Python duck typing. The reference explains that type classes are collections of overloaded operations, instance declarations are definition-like, and instance synthesis fills square-bracket parameters. citeturn6view4turn6view5turn9view1turn9view2turn18search5
def id' {α : Type} (x : α) : α := x
def three : Nat := id' 3
def greet : String := id' (α := String) "lean"
Implicit arguments are written with {...}; instance-implicit arguments are written with [...]; named arguments use x := ... syntax at call sites. The elaborator creates metavariables for omitted implicit arguments and schedules instance-implicit arguments for type-class synthesis. This means you should read a signature like def f {α} [C α] (x : α) := ... as “α will be inferred; evidence for C α will be synthesised”. citeturn6view7turn6view8
Lean organises APIs with namespaces and source-file imports. A source file is the smallest compilation unit; imports use dotted module names derived from paths; importing a file does not automatically open its namespaces. Namespaces are hierarchical and are the primary organisation mechanism for APIs. citeturn24view0turn24view1turn6view12
import MyLib.Data.Util
namespace Demo
def value : Nat := 42
end Demo
A theorem statement is a type to inhabit. The local context contains variables and hypotheses already available; the current goal is the target type still to be constructed. In tactic mode, Lean shows a proof state: an ordered sequence of goals, each consisting of a context plus a target. example checks a theorem or term and discards it; theorem stores it in the environment for later use. citeturn19view0turn9view4
example : 2 + 2 = 4 := by
rfl
example (p q : Prop) : p → q → p := by
intro hp hq
exact hp
example (p q : Prop) : p ∧ q → q ∧ p := by
intro hpq
cases hpq with
| intro hp hq =>
exact And.intro hq hp
example : ∀ n : Nat, n = n := by
intro n
rfl
example (x y z : Nat) (h₁ : x = y) (h₂ : y = z) : x = z := by
calc
x = y := h₁
_ = z := h₂
The core tactics you need first are small and compositional. rfl closes reflexive goals. exact e closes a goal if e already has the target type. apply e matches the goal against the conclusion of e and creates subgoals for its premises. intro moves a binder or implication premise from the goal into the context. cases performs case analysis on an inductive hypothesis. induction applies an induction principle and gives you induction hypotheses. rw rewrites using equalities. simp simplifies using [simp] lemmas, supplied rules, and optionally hypotheses. calc is stepwise transitive reasoning. citeturn25view0turn20view0turn25view4turn25view1turn25view2turn25view3
Tactic mode and term mode are interchangeable views of the same result. Term mode writes the proof term directly, often with fun, match, have, and show; tactic mode is imperative proof-state manipulation that constructs that term. The reference is explicit that tactics are a special-purpose proof language and that each goal corresponds to an incomplete portion of a proof term. For short structural proofs, term mode is often clearer; for case splits and induction, tactic mode is usually faster to write and easier to debug. citeturn19view0turn8view1
example (p q : Prop) : p → q → p :=
fun hp hq => hp
theorem zero_add' (n : Nat) : 0 + n = n := by
induction n with
| zero =>
rfl
| succ n ih =>
rw [Nat.add_succ, ih]
Lean has a hierarchy of universes. Prop is Sort 0; data lives in Type u, notation for Sort (u + 1). The important operational distinction is not merely “logic versus data”, but also that propositions are proof-irrelevant and run-time irrelevant: any two proofs of the same proposition are interchangeable, and proofs are erased from compiled code. Also, all function types in the core language are dependent; ordinary arrows are just the special case where the result type does not mention the argument. citeturn9view3turn6view2turn6view3turn8view0
That is why the same syntax works for programs and proofs. Nat → Nat is an ordinary function type; (n : Nat) → Fin (n + 1) is a dependent function type whose codomain depends on the input value. Dependent pairs (Sigma, written Σ) package a value together with indexed data; subtypes package a value together with a proof of a predicate, and the proof component is erased at run time. You do not need dependent pairs immediately, but you should recognise them when a value determines the type of accompanying data. citeturn23search0turn23search1
Elaboration handles many conveniences that are not part of the kernel’s core theory: implicit parameters, named arguments, type-class synthesis, notation, and coercions. Coercions are inserted when the elaborator has constructed a term of one type in a context expecting another and can synthesise a suitable CoeT chain. Notation is likewise surface syntax translated during elaboration. This is why “what Lean parses” and “what the kernel checks” are related but distinct questions. citeturn6view6turn6view7turn6view8turn3search2turn22view0
When Lean rejects code or a proof, the failure is usually in one of four buckets. A type mismatch/application type mismatch usually means unification could not make inferred and expected types definitionally equal. Don’t know how to synthesise implicit argument means ordinary implicit inference lacked enough information. Failed to synthesise instance means instance search for a square-bracket parameter failed. Failed to infer structural recursion / termination means the recursive-definition checker could not justify the recursion pattern. These are different failure modes and need different fixes. citeturn26search3turn18search5turn18search1turn21view0turn21view2
For proofs, read the goal state literally. Everything above ⊢ is in scope; everything after ⊢ is the type you still need to build. From there, the default workflow is: introduce binders with intro; normalise with simp; rewrite with rw; split cases with cases; use induction when the object was defined inductively; and use exact or apply when you already know the relevant lemma or constructor. Lean also ships search-oriented helpers such as exact?, apply?, and rw?, and the community recommends API docs and Loogle for declaration search. citeturn19view0turn20view0turn11search2turn17view1
In practice, simp plus rewriting is the centre of day-to-day proof automation. simp uses lemmas tagged [simp] and optional local rules; rw applies specific equalities in a controlled order. Most beginner proofs become much shorter once the right helper lemma is stated, marked for simplification where appropriate, or passed explicitly to simp [lemma₁, lemma₂]. This is the standard Lean style because it scales from tiny toy proofs to library developments. citeturn20view0turn6view10turn15search9
Mathlib changes practical Lean development from “prove everything from first principles” to “assemble the right existing abstractions and lemmas”. The community site describes Mathlib as a unified, community-driven library of formalised mathematics that also contains definitions useful for programming, and the documentation stack includes searchable API docs for Mathlib, Std, Batteries, and even core Lean/compiler modules. Real Lean work therefore depends as much on library navigation as on raw tactic knowledge. citeturn17view0turn17view1turn17view2
For functional programming, keep executable code in Type, specifications in Prop, and do not mix them prematurely. Lean’s default is total code: match must be exhaustive, and recursive definitions must be justified by structural or other accepted termination arguments. For lightweight feedback, #eval compiles and evaluates expressions; example declarations are good for tiny executable fragments or proof obligations that you want checked but not named. Then prove semantic properties separately with theorem. citeturn13view1turn21view0turn21view1turn26search3turn6view2
The most common failure mode for experienced engineers is assuming Lean will “obviously” perform a semantic transformation that is not definitional equality. If two terms only become equal after a theorem is applied, you need rw, simp, change, or a helper lemma; the kernel will not guess that for you. The next most common mistake is hiding information from elaboration: omitted types, an unsolved implicit parameter, or a missing instance looks like a logic failure but is often just an elaboration failure. When in doubt, make arguments explicit, state one helper lemma, and rerun. citeturn18search4turn20view0turn18search5turn18search1
After this introduction, the most useful next texts are the official Theorem Proving in Lean 4 for proof language and foundations, Functional Programming in Lean for programming idioms, and Mathematics in Lean once you start using Mathlib seriously. Keep the language reference and API docs open while you work; for non-trivial developments, they are not optional. citeturn17view1turn5view0turn17view0
The shortest path from “I can read Lean” to “I can write small programs and proofs” is to alternate between a definition and a property of that definition. The sequence below goes from plain functions, to reflexive computation proofs, to rewriting from a hypothesis, to induction on naturals, to a custom datatype and an induction proof over it. The tactics used are the standard ones introduced above: rfl, rw, induction, simp, and exact. citeturn25view0turn20view0turn25view2turn25view1
def double (n : Nat) : Nat := n + n
def headOr {α : Type} (fallback : α) : List α → α
| [] => fallback
| x :: _ => x
example : double 3 = 6 := by
rfl
example (a b c : Nat) (h : a = b) : a + c = b + c := by
rw [h]
theorem zero_add' (n : Nat) : 0 + n = n := by
induction n with
| zero =>
rfl
| succ n ih =>
rw [Nat.add_succ, ih]
inductive Tree (α : Type) where
| leaf
| node (left : Tree α) (value : α) (right : Tree α)
def mirror {α : Type} : Tree α → Tree α
| .leaf => .leaf
| .node l x r => .node (mirror r) x (mirror l)
theorem mirror_mirror {α : Type} (t : Tree α) : mirror (mirror t) = t := by
induction t with
| leaf =>
rfl
| node l x r ihL ihR =>
simp [mirror, ihL, ihR]
Read what is going on operationally. double 3 = 6 is closed by computation, so rfl works. The second theorem works because rw [h] rewrites the goal using a hypothesis in the local context. zero_add' is not definitionally true by reduction on the second argument of addition, so it needs induction. mirror_mirror is the canonical custom-datatype pattern: define a structurally recursive function, then prove its involutive property by induction with one induction hypothesis per recursive field. citeturn6view10turn20view0turn25view2
Use this as the minimal recall set while writing your first files. The syntax items below correspond directly to Lean’s definition, function, inductive-type, namespace, implicit-argument, and function-application machinery. citeturn9view4turn13view0turn24view1turn6view7turn6view8
def f (x : α) : β := term — define a function or constant. citeturn9view4inductive T where | c1 ... | c2 ... — define a sum type or recursive datatype. citeturn10search10turn13view0structure S where field₁ : A ... — define a record/product type with projections. citeturn6view4class C (α : Type) where ... / instance : C T where ... — define and populate a type class. citeturn6view5turn9view1match x with | ... => ... — case analysis and data destruction. citeturn13view0fun x => body — lambda abstraction; proofs of implications and ∀ often look like this. citeturn8view1turn18search5{α : Type} — implicit argument; [C α] — instance-implicit argument. citeturn6view7turn6view8(α := Nat) — pass a named implicit argument explicitly. citeturn6view8namespace N ... end N — qualify related declarations under N. citeturn24view1import A.B.C — import a module by dotted name. citeturn24view0For proofs, the following tactics are the smallest useful set. Their intended use is standardised in the reference manual and theorem-proving tutorial. citeturn19view0turn20view0turn25view0turn25view1turn25view2turn25view3turn25view4
rfl — close a reflexive goal, often after computation. citeturn25view0intro x — move one binder or premise into context. citeturn25view4exact t — finish the goal with a term already of the right type. citeturn20view0apply f — reduce the goal to the premises of f. citeturn20view0rw [h, ← lemma] — rewrite using equalities. citeturn20view0simp [defs, lemmas] — simplify using [simp] rules and supplied facts. citeturn20view0cases h — split by constructors of an inductive hypothesis. citeturn25view1induction n with | ... — prove by induction, receiving induction hypotheses. citeturn25view2calc ... — write chained equational or transitive reasoning. citeturn25view3exact?, apply?, rw? — interactive search aids; use the suggestion, do not leave them in the final proof. citeturn11search2When diagnostics appear, parse them mechanically. “Application type mismatch” suggests failed unification; “don’t know how to synthesise implicit argument” suggests insufficient type information; “failed to synthesise instance” means missing type-class evidence; “failed to infer structural recursion” means Lean could not justify termination from the syntax of the recursive calls. citeturn26search3turn18search5turn18search1turn21view0