First steps in Lean

Builds on

Required prerequisites, all the way down: 15

You will learn to

• Write and check short Lean proofs of propositional tautologies and simple equalities using rfl, rw and simp.
• Prove a statement about natural numbers by induction in Lean, such as 0 + n = n.
• Read a Mathlib theorem statement, and distinguish applying a library theorem from proving a result independently.

Definition

• A proof assistant is a program that checks proofs written in a formal language.
• In Lean, a proposition is a type and a proof of it is a term of that type.
• A tactic is a command that builds part of a proof, such as rw (rewrite) or induction.

Theorem

• A Lean proof that compiles without sorry and without added axioms has been checked by Lean's kernel relative to Lean's logic.
• A formal proof is only as meaningful as its formal statement: a mis-stated theorem can be proved correctly.
• For Lean's natural numbers, n + 0 = n holds by definition (rfl), while 0 + n = n needs a proof by induction.

Common misconceptions

• Believing a machine-checked proof guarantees that the statement says what was intended.
• Thinking a proof containing sorry is finished.
• Confusing the use of a Mathlib lemma with proving the result from more basic facts.

Leads to

Optional discoveries

• Type theory and propositions as types Lean's logic is a dependent type theory in which propositions are types and proofs are terms.

Learning pathways

• Computer science and formal methods

Further reading

• Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4
• Jeremy Avigad and Patrick Massot, Mathematics in Lean