First steps in Lean

前置知识

15 项必需的前置知识（一直追溯到底）

你将学会

• 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.

定义

• 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.

定理

• 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.

常见误解

• 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.

通向

可选发现

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

学习路径

• Computer science and formal methods

延伸阅读

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