Lean 4 is simultaneously a dependently-typed functional programming language and an interactive proof assistant. You write programs and proofs in the same language. The Lean kernel checks every proof mechanically — if it compiles without sorry, it is correct.

Mathlib is the community-maintained library of formalised mathematics written in Lean 4. It contains over 9,150 modules covering algebra, analysis, topology, number theory, category theory, and more. Most users write import Mathlib to access all of it at once.

Lean 4 is the language and proof engine. Mathlib is the mathematical content built on top. You can use Lean without Mathlib for pure logic and computation, but most mathematical work imports Mathlib for its tactics, type class instances, and theorems.

In Lean, every mathematical statement is a type, and every proof is a term of that type. Writing theorem h : 1 + 1 = 2 declares a type; the proof body constructs a term inhabiting it. The kernel verifies the term fits the type.

In VS Code: Ctrl+Shift+P (or Cmd+Shift+P on Mac) → type Lean 4: Open Infoview. The panel updates live as you move your cursor through a file or proof.

Hypotheses above the line, goal below. The ⊢ symbol means “goal to prove”.

h : n > 0
⊢ n + 1 > 0

h is a hypothesis; the goal is to prove n + 1 > 0.

• ■ Red — error. Lean cannot type-check this expression.
• ■ Yellow — warning. Usually sorry or an unused variable.
• ■ Blue / spinning — elaboration in progress. Wait.
• ■ No squiggle — clean. Proof or definition accepted.

• Ctrl+Shift+P — Command Palette (all Lean commands)
• Ctrl+Space — trigger autocomplete / suggestions
• F12 — go to definition of any identifier
• Shift+F12 — find all references
• Ctrl+. — quick fix / code actions
• Hover any identifier — shows its type inline

• \forall → ∀   \exists → ∃
• \to → →   \iff → ↔
• \and → ∧   \or → ∨
• \not → ¬   \ne → ≠
• \langle \rangle → ⟨⟩

• \N → ℕ   \Z → ℤ
• \Q → ℚ   \R → ℝ
• \C → ℂ

• \in → ∈   \notin → ∉
• \sub → ⊆   \subs → ⊂
• \union → ∪   \inter → ∩
• \empty → ∅
• \le → ≤   \ge → ≥

• \sum → ∑   \prod → ∏
• \int → ∫   \partial → ∂
• \circ → ∘   \cdot → ·
• \times → ×   \otimes → ⊗
• \norm → ‖   \mapsto → ↦

• \alpha α   \beta β   \gamma γ
• \delta δ   \epsilon ε   \theta θ
• \lambda λ   \mu μ   \nu ν
• \pi π   \sigma σ   \phi φ
• \omega ω   \Omega Ω

• \lfloor \rfloor → ⌊⌋
• \lceil \rceil → ⌈⌉
• \gets → ←   \comp → ∘
• \^2 → ²   \_1 → ₁

• -- text — single-line comment
• /- text -/ — block comment
• /-- text -/ — doc comment (shown on hover)
• /-! text -/ — module-level doc comment

Show the type of any expression. The most-used command — use it constantly. #check Nat.add_comm shows the full statement of that lemma.

Show the fully explicit type with all implicit arguments visible. Essential for understanding exactly what arguments a function expects.

Evaluate any computable expression and print the result. #eval Nat.gcd 12 8 prints 4.

Print the full definition, type, and implementation of a declaration. Use it to understand how Mathlib defines things internally.

List all axioms a declaration depends on. Verify that no sorry or native_decide crept into a proof you care about.

In tactic mode, search the environment for a term that closes the current goal. Comprehensive but slow — the best first thing to try when completely stuck.

Find lemmas whose conclusion matches the current goal shape. More targeted than exact? — use when you know the shape but not the lemma name.

Run simp and report exactly which lemmas it used. Lets you replace a bare simp with a precise simp only [...] for long-term stability.

Every value in Lean has a type. 2 : Nat, true : Bool, (1 + 1 = 2) : Prop. Use #check to see any type instantly. Types themselves have types: Nat : Type.

• Nat — natural numbers ℕ (non-negative)
• Int — integers ℤ (positive and negative)
• Bool — true / false (computable)
• String — text
• Prop — the type of mathematical statements
• Type — the type of types

#eval 2 + 2          -- 4
#eval "hello".length -- 5
#check Nat.succ      -- Nat → Nat
#eval List.range 5   -- [0,1,2,3,4]

Lean uses space for application: f x y not f(x,y). Parentheses only group: f (g x). Left-associative: f x y = (f x) y.

Tell Lean the expected type with (expr : Type). Useful when inference picks the wrong type: (0 : Int) vs (0 : Nat) are different values.

fun x => x + 1 maps Nat to Nat. fun x y => x * y is two-argument. These are first-class values you can pass around.

Load the entire Mathlib library. Every tactic, theorem, and type class instance becomes available. Place at the very top of any file that uses Mathlib.

An anonymous theorem statement. The proof is checked but not added to the environment. Use for practice and exploration without polluting the namespace.

The proposition — the type of the proof we are building. In Lean, = is a Prop. We are claiming this equality holds and must construct a proof.

Enter tactic mode. The := means “is defined as” and by opens a tactic block where commands manipulate the proof state step by step.

A tactic that normalises numeric expressions. It knows 1 + 1 = 2 directly — one of the most useful one-liners for any concrete numeric goal.

After this runs, the Infoview shows No goals — proof complete. If goals remain, a tactic did not fully close what it was given.

Named proof of P. Convention: major results. Identical to lemma to the kernel — distinction is purely human.

Named proof, convention for auxiliary helper facts. Use lemma for intermediate steps and theorem for the main result.

Anonymous proof — checked but not added to the environment. Essential for exploration and tests. No namespace pollution.

Define a named value of type T. Semireducible by default. The workhorse for all non-propositional definitions.

Like def but marked @[reducible] — unfolds eagerly in unification. Use for type synonyms where Lean should see through the name automatically.

For definitions that depend on Classical.choice or non-constructive axioms. Cannot be #eval’d but perfectly usable in proofs.

A record type with named fields. Auto-generates projections, the constructor Name.mk, and extensionality infrastructure.

A type class. Fields become the interface; use instance to provide implementations. The foundation of Lean’s algebraic hierarchy.

An inductive type. Auto-generates the recursor Name.rec, casesOn, and recOn. The basis for Nat, List, Or.

Registers a type class instance for synthesis. Lean finds instances automatically by type. Equivalent to @[instance] def.

private: visible only in the current file. protected: must use full qualified name even after open.

A definition without a verified termination proof. Use for IO, parsers, and cases where proving termination is genuinely hard.

Opens a named scope. All declarations inside are prefixed Name.. Namespaces can be reopened anywhere — Mathlib uses this extensively.

An anonymous scope for grouping variable and open commands. Does not prefix names. Variables and opens declared inside no longer apply after end.

Brings all non-protected names from Name into scope without qualification. Scoped to the nearest enclosing section or namespace.

Opens a namespace for a single expression or tactic block only. The cleanest way to use a namespace without polluting the surrounding scope.

Activates only the scoped notations of Name. Classic: open scoped BigOperators to enable ∑ and ∏ notation.

Declares a parameter auto-added to subsequent declarations that mention it. () explicit, {} implicit, [] typeclass instance.

Declares universe-level variables for universe-polymorphic definitions. Lean’s type theory is stratified: Type 0 : Type 1 : …

Provides the well-founded termination measure for a recursive definition. Lean checks this measure strictly decreases on every recursive call.

Assumes the next hypothesis from a → or ∀ in the goal, naming it h. intros introduces all available hypotheses at once.

Like intro but with immediate pattern-matching. ⟨a, b⟩ for conjunctions, h | k for disjunctions, ⟨a, rfl⟩ to substitute equalities on arrival.

Close the goal if e has exactly the goal’s type. The most direct closer — if you know the term, use it.

Close a = a by reflexivity. Works when both sides are definitionally equal — Lean verifies by computation.

Close the goal if it exactly matches any hypothesis in context. Lean searches all hypotheses automatically.

Tries rfl, assumption, decide, and True.intro in sequence. A lightweight closer for genuinely trivial goals.

Close when context contains contradictory hypotheses (e.g. h : P and h’ : ¬P). Searches automatically.

Succeeds only if no goals remain. A sentinel to confirm a proof is complete — a failing done means you missed a goal.

If h : A → B and the goal is B, the new goal becomes A. Backward reasoning — reduce the goal to something you know.

Build a proof term with holes ?_. Each hole becomes a new sub-goal. More controlled than apply when you want to specify partial structure explicitly.

Split P ∧ Q or P ↔ Q into two sub-goals. Also works on any inductive type with a single constructor.

Choose a branch of P ∨ Q. After left the goal becomes P; after right it becomes Q.

Provide the witness for ∃ x, P x. After use e the goal becomes P e. Accepts multiple arguments for nested existentials.

Case-split on an inductive hypothesis or value h. Produces one goal per constructor.

Recursive deconstruction: ⟨a, b⟩ for products, h | k for sums, ⟨a, rfl⟩ to substitute. The richest destructuring tactic.

obtain ⟨a, ha⟩ := h destructs h : ∃ x, P x into witness a and proof ha.

Prove by induction on x. One goal per constructor with the induction hypothesis (IH) available.

Use a custom recursor r instead of the default. Useful for strong induction and domain-specific induction principles.

Prove an intermediate claim P and name it h. The primary way to break long proofs into readable labelled steps.

Declare it suffices to prove P. The by ... closes the original goal using h. Then you prove P.

Chained equalities or inequalities with justifications at each step:
calc a = b := h1
     _ ≤ c := h2

Move h back into the goal as ∀ or →. The inverse of intro. Useful to generalise before induction.

Replace all occurrences of expression e with a fresh variable x. Makes a goal induction-ready.

When h : x = e, substitute x everywhere in the goal and context, then remove both.

Apply hypothesis h to arguments a b in place. Replaces h with the specialised version.

Remove hypothesis h from context when it is no longer needed.

Admit any goal as true. Emits a yellow warning. Invaluable for top-down proof development — sketch structure first, fill sorrys second.

Rewrite left-to-right using h : a = b. Use rw [←h] for right-to-left. Use at hyp to rewrite in a hypothesis instead of the goal.

Chain multiple rewrites in sequence. Order matters — each rewrite happens after the previous transformation.

Simplify using all @[simp]-tagged lemmas. Closes many goals but is non-deterministic — avoid bare simp in finished proofs; use simp only.

Run simp restricted to listed lemmas only. More predictable, faster, and stable across Mathlib updates. The standard for polished proofs.

Like rw but works under binders (∀, fun, ∃). The correct tool when rw fails because the pattern appears inside a lambda.

Apply simp to the goal and all hypotheses simultaneously until fixpoint. Powerful but slow — use for hard goals or as a last resort.

Rewrite only the nth occurrence of the pattern. Essential when the same expression appears multiple times.

unfold: unfold definition of f once. delta: force-unfold even @[irreducible] definitions. Use sparingly — prefer lemmas about f.

Focused rewriting inside a specific sub-term. Enter with conv =>, navigate with lhs / rhs / ext x, then rw or simp at that exact position.

You have an equality h : a = b and want to replace a specific occurrence. Fails under binders — use simp_rw if the pattern appears inside a fun or ∀.

In finished proofs, always use simp only with an explicit list. Use bare simp only during exploration. Run simp? to discover the right list.

The goal matches the conclusion of a known lemma. Use apply? to find h. Use exact when no new premises arise. Use refine to fill sub-goals manually.

Goal involves ℕ or ℤ with addition, subtraction, mul by literals, mod, or div. Faster than linarith for discrete arithmetic.

Goal is a linear inequality over an ordered field (ℝ, ℚ). Add hints when needed: linarith [sq_nonneg x, h1].

Goal involves concrete numbers: 2^8 = 256, Nat.Prime 97. Much faster and more reliable than decide for numeric goals.

Goal is a polynomial identity in a ring. For fractions: first field_simp to clear denominators, then ring.

You have no idea where to start. Let Lean search everything. Slow but comprehensive. Try apply? as a faster targeted alternative.

A type class is an interface (like Add, Ring, MetricSpace). An instance provides the implementation for a specific type. Lean finds instances automatically through instance synthesis — you write [Ring R] and Lean finds the right implementation silently.

• Semigroup → Monoid → Group → CommGroup
• Semiring → Ring → CommRing
• CommRing + IsDomain → integral domain
• DivisionRing → Field → LinearOrderedField
• Module R M → Algebra R A

• Preorder → PartialOrder → LinearOrder
• SemilatticeSup / SemilatticeInf → Lattice
• Lattice → CompleteLattice
• OrderedAddCommMonoid → OrderedField
• LinearOrderedField (ℝ, ℚ, etc.)

• TopologicalSpace → T0, T1, T2Space
• MetricSpace → NormedAddCommGroup
• NormedSpace → InnerProductSpace
• CompleteSpace (Banach / Hilbert)
• MeasurableSpace → MeasureSpace

#check (inferInstance : Ring ℤ)
#check (inferInstance : Field ℝ)
example : CommRing ℤ := inferInstance

instance : Add MyType where
  add x y := ...

instance : Ring MyType :=
  { add := ..., mul := ..., ... }

Enable with open scoped BigOperators. Then write ∑ i ∈ s, f i and ∏ i ∈ s, f i. Key file: Mathlib.Algebra.BigOperators.Group.Finset.

|x| for ordered groups. ‖x‖ (type \norm) for normed spaces. Key lemmas: abs_add, abs_mul, norm_add_le, norm_sub_le.

Finset.sum, Finset.prod, Finset.card. Filter: Finset.filter. Image: Finset.image. Key: Mathlib.Data.Finset.Basic.

Filter.Tendsto f (nhds a) (nhds b) means f(x) → b as x → a. ContinuousAt f a is syntactic sugar. Key: Mathlib.Topology.Basic.

HasDerivAt f f’ x: f has derivative f’ at x. deriv f x returns it (0 if not differentiable). fderiv for Fréchet derivatives.

open MeasureTheory. Write ∫ x, f x ∂μ for integrals. Key: Mathlib.MeasureTheory.Measure.MeasureSpace.

Module R M, Submodule R M, LinearMap R M N, LinearEquiv R M N. Basis: Basis ι R M. Key: Mathlib.LinearAlgebra.Basic.

Lean inserts coercions automatically: ℕ→ℤ→ℚ→ℝ. Use push_cast to move casts inward, norm_cast to normalise, @[norm_cast] on your own cast lemmas.