跳到正文
The Lumenary
九至十二年级Computation计划中

First steps in Lean

Stating and proving simple results in the Lean 4 proof assistant: propositions and proofs, rewriting, induction on natural numbers and reading Mathlib statements, with attention to what a machine check does and does not guarantee.

math.comp.intro-lean

显示到达此主题所需的全部内容

本主题的课程尚未编写。下面的提纲是课程地图的一部分，尚未经过审校。

前置知识

Propositional logic and truth tablesProof: direct, contrapositive, contradiction and inductionProgramming for mathematics

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.

通向

Formalising mathematics in Lean and Mathlib

可选发现

学习路径

延伸阅读