跳到主要内容

Lean 数学定理形式化

介绍​

Lean 是一种交互式定理证明器，专为形式化数学和编程语言设计。它允许用户以严格的逻辑形式表达数学定理，并通过计算机验证其正确性。对于初学者来说，Lean 提供了一个强大的工具来学习和实践数学证明，同时培养编程技能。

在本教程中，我们将逐步介绍如何使用 Lean 形式化数学定理，并通过实际案例展示其应用。

什么是数学定理形式化？​

数学定理形式化是指将数学定理和证明过程转化为计算机可以理解和验证的形式。通过形式化，我们可以确保定理的正确性，并避免人为错误。

Lean 使用一种称为 依赖类型理论 的逻辑系统，允许用户定义数学对象、陈述定理并编写证明。

安装 Lean​

在开始之前，您需要安装 Lean 和其配套工具。以下是安装步骤：

  1. 访问 Lean 官方网站 并按照说明安装 Lean。
  2. 安装 Visual Studio Code 并添加 Lean 扩展，以便在 IDE 中编写和验证代码。

第一个例子：形式化加法交换律​

让我们从一个简单的例子开始：形式化加法的交换律。加法交换律指出，对于任意两个自然数 a 和 b，有 a + b = b + a。

lean
import tactic

-- 定义加法交换律
theorem add_comm (a b : ℕ) : a + b = b + a :=
begin
  induction a with d hd,
  { simp, },
  { simp [hd], }
end

代码解释​

  1. import tactic：导入 Lean 的战术库，它提供了许多自动化工具来简化证明。
  2. theorem add_comm (a b : ℕ) : a + b = b + a :=：定义一个名为 add_comm 的定理，它接受两个自然数 a 和 b，并声明 a + b = b + a。
  3. begin ... end：开始证明过程。
  4. induction a with d hd：对 a 进行数学归纳。d 是归纳假设中的变量，hd 是归纳假设。
  5. { simp, }：使用 simp 战术简化当前目标。
  6. { simp [hd], }：使用归纳假设 hd 进一步简化目标。

运行结果​

当您在 Lean 中运行此代码时，Lean 会验证证明的正确性。如果证明通过，您将看到一条成功消息。

实际案例：形式化费马小定理​

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

让我们尝试在 Lean 中形式化这个定理。

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

-- 定义费马小定理
theorem fermat_little_theorem (p : ℕ) (hp : nat.prime p) (a : ℤ) (hpa : ¬ p ∣ a) :
  a^(p-1) ≡ 1 [ZMOD p] :=
begin
  -- 证明过程略
  sorry
end
备注

注意：由于费马小定理的证明较为复杂，这里我们使用 sorry 占位符表示未完成的证明。在实际应用中，您需要编写完整的证明。

代码解释​

  1. import data.nat.modeq 和 import data.nat.prime：导入数论相关的库。
  2. theorem fermat_little_theorem ...：定义费马小定理，接受一个质数 p 和一个整数 a，并声明 a^(p-1) ≡ 1 mod p。
  3. sorry：表示未完成的证明。

总结​

通过本教程，您已经了解了如何使用 Lean 形式化数学定理。我们从简单的加法交换律开始，逐步介绍了 Lean 的基本语法和证明方法。虽然形式化复杂的定理（如费马小定理）可能需要更多的时间和经验，但 Lean 提供了一个强大的工具来帮助您学习和实践数学证明。

附加资源​

练习​

  1. 尝试形式化乘法交换律 a * b = b * a。
  2. 研究并尝试形式化另一个简单的数学定理，如分配律 a * (b + c) = a * b + a * c。
  3. 挑战：尝试完成费马小定理的完整证明。

祝您在 Lean 的学习之旅中取得成功！