跳到主要内容

Lean 形式化数学

介绍​

Lean是一种交互式定理证明器，专门用于形式化数学和编程验证。形式化数学是指将数学定理和证明过程用严格的逻辑语言表达出来，以便计算机能够理解和验证。Lean的核心目标是帮助数学家、计算机科学家和程序员以更严谨的方式构建和验证数学理论。

通过Lean，你可以将数学定理转化为代码，并使用Lean的证明引擎来验证这些定理的正确性。这种方式不仅提高了数学研究的严谨性，还为数学教育提供了新的工具和方法。

Lean 的基本概念​

命题与证明​

在Lean中，数学命题被表示为类型（Type），而证明则是该类型的项（Term）。例如，命题“1 + 1 = 2”在Lean中可以表示为：

lean
example : 1 + 1 = 2 :=
begin
  refl
end

在这个例子中，example 是一个命题，1 + 1 = 2 是命题的内容，refl 是证明该命题的项。refl 是“自反性”（reflexivity）的缩写，表示等式两边的值是相等的。

类型系统​

Lean的类型系统是其核心之一。每个表达式都有一个类型，类型可以是简单的（如自然数 ℕ）或复杂的（如函数类型 ℕ → ℕ）。Lean的类型系统基于依赖类型（Dependent Types），这意味着类型可以依赖于值。

例如，定义一个函数 add，它将两个自然数相加：

lean
def add : ℕ → ℕ → ℕ :=
λ n m, n + m

在这个定义中，ℕ → ℕ → ℕ 表示 add 是一个接受两个自然数并返回一个自然数的函数。

定理与证明​

在Lean中，定理是通过构造一个类型为命题的项来证明的。例如，证明“对于所有自然数 n，n + 0 = n”：

lean
theorem add_zero : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  induction n with d hd,
  { refl },
  { simp [hd] }
end

在这个证明中，intro 用于引入变量 n，induction 用于对 n 进行归纳，refl 和 simp 用于简化等式。

实际案例：证明费马小定理​

费马小定理是数论中的一个重要定理，它指出：如果 p 是一个素数，且 a 是一个不被 p 整除的整数，那么 a^(p-1) ≡ 1 mod p。

我们可以使用Lean来形式化并证明这个定理。首先，我们需要定义素数和模运算的概念：

lean
import data.nat.prime
import data.nat.modeq

open nat

theorem fermat_little_theorem (p : ℕ) (hp : prime p) (a : ℤ) (hpa : ¬ p ∣ a) :
  a^(p-1) ≡ 1 [ZMOD p] :=
begin
  -- 证明过程省略
end

在这个例子中，我们使用了Lean的标准库中的 data.nat.prime 和 data.nat.modeq 模块来定义素数和模运算。fermat_little_theorem 是费马小定理的形式化表述，hp 是 p 为素数的假设，hpa 是 a 不被 p 整除的假设。

总结​

Lean形式化数学是一种强大的工具，它允许你将数学定理转化为代码，并通过计算机验证其正确性。通过学习Lean，你不仅可以提高数学研究的严谨性，还可以探索数学与计算机科学的交叉领域。

附加资源与练习​

  • Lean官方文档: https://leanprover.github.io/
  • 《Theorem Proving in Lean》: 一本详细介绍Lean的书籍，适合初学者。
  • 练习: 尝试在Lean中证明“对于所有自然数 n，0 + n = n”。
提示

如果你对Lean的形式化数学感兴趣，建议从简单的命题和证明开始，逐步深入到更复杂的数学定理。