Examples
Complete Lean examples
Eight files accompany the tutorial. A separate RecordedAxiom.lean source study brings the collection to nine downloads.
Four source studies and the quantifier proof supplement appear in full below. All files use Lean 4.28.0 with its standard implicit Init import; they need no mathlib.
The tutorial example notes link to all eight tutorial files and explain their expected results. The notes for the five files below cover the source studies and proof supplement on this page.
These files contain Lean source, not captured editor histories or recorded reader outcomes.
From Lean source to a reader view
For each x, there is a y
example : Prop := ∀ x : Nat, ∃ y : Nat, y = x
Download QuantifierForallExists.lean
For each x, y is introduced inside x’s scope. The choice of y may depend on x.
One y for every x
example : Prop := ∃ y : Nat, ∀ x : Nat, y = x
Download QuantifierExistsForall.lean
Here y is introduced before x. The same y is required to work for every x.
A choice for each natural number
example : Prop := ∀ x : Nat, ∃ y : Nat, y = x
For every natural number x, there exists a natural number y equal to x. The existential quantifier lies inside the universal quantifier’s scope, so a witness for y may depend on x.
The declaration example : Prop := … forms this proposition. It supplies neither a proof nor a witness. The proof supplement shows that choosing x itself works for every x.
One choice for every natural number
example : Prop := ∃ y : Nat, ∀ x : Nat, y = x
Here one natural number y must equal every natural number x. Applying that requirement to 0 and 1 would give 0 = 1, so the proposition is false.
Lean accepts this file because the expression forms a proposition. The file supplies no proof, witness, or refutation. The proof supplement supplies the refutation separately.
Lesson 1 follows both statements in binder order. Lesson 2 explains the difference between forming a proposition and proving it.
A law belonging to its owner
structure Rotor where
Carrier : Type
turn : Carrier → Carrier
fixed : ∀ x, turn x = x
example (owner : Rotor) (unused : Nat) : Rotor := owner
A Rotor contains a type, a function on that type, and a law saying that the function fixes each element. The example takes owner : Rotor as a parameter and returns it. That assumed owner already carries its law in owner.fixed; the example does not construct a Rotor or independently establish its law.
The initial guided view refuses a reading of the selected structure value in this example. Source inspection follows a distinct route: catalogue the fields, project fixed, inspect its type, read the universal layer, then enter its body. Inspecting the equality inside the law does not produce a separately specialized proof of that equality.
The deliberately unused parameter remains part of the context. Its presence does not show that the returned value depends on it. Lean’s unused-variable warning is a diagnostic, not a rejected kernel outcome. The reference explains these distinctions.
An unfinished proof and its dependency
theorem claimed : 2 + 2 = 5 := sorry
example : 2 + 2 = 5 := claimed
Read the placeholder dependency
This file deliberately leaves a proof unfinished with sorry. Lean accepts the declarations and warns that a declaration uses sorry. The placeholder introduces a dependency on sorryAx; referring to claimed in the second declaration retains that dependency.
Accepted typing here is relative to an environment containing the placeholder dependency. Neither declaration independently establishes the false equation 2 + 2 = 5. Read the typing outcome together with its axiom audit; an empty audit for a different formation check cannot replace it.
Lesson 5 examines accepted typing, axiom dependencies, and diagnostics using Evidence.lean.
Proof supplement: prove one order, refute the other
theorem each_has_equal : ∀ x : Nat, ∃ y : Nat, y = x := by
intro x
exact ⟨x, rfl⟩
theorem no_one_equals_all : ¬ (∃ y : Nat, ∀ x : Nat, y = x) := by
intro h
obtain ⟨y, hy⟩ := h
have impossible : (0 : Nat) = 1 := (hy 0).symm.trans (hy 1)
exact Nat.noConfusion impossible
#print axioms each_has_equal
#print axioms no_one_equals_all
This supplement contains two proofs, separate from the source files that form the propositions. each_has_equal chooses x as the witness for each x. no_one_equals_all derives the impossible equality 0 = 1 from the claim that one number equals every number.
Both theorems have been independently checked with Lean 4.28.0 and have no axiom dependencies.
To check a downloaded file with that toolchain, run lean FileName.lean in its directory, replacing FileName.lean with its name. The quantifier files check without the warnings deliberately illustrated by RotorLaw.lean and RecordedAxiom.lean.