3个关键步骤：用Lean 4实现数学定理的形式化证明

在数学研究和教育中，定理证明的严谨性至关重要。Lean 4作为新一代定理证明器，为数学形式化提供了强大支持。本文将通过三个核心步骤，展示如何使用Lean 4进行数学定理的形式化证明，从基础概念到实际应用，帮助读者掌握这一重要技能。无论是学生、研究人员还是数学爱好者，都能通过本文了解Lean 4定理证明的基本方法，体验数学形式化方法带来的严谨与乐趣。

如何构建数学命题的形式化描述？

数学命题的形式化是证明的第一步，也是最关键的一步。在Lean 4中，我们需要将自然语言描述的数学命题转化为精确的形式化语言。以"√2是无理数"这一经典命题为例，我们来看看如何进行形式化描述。

首先，我们需要定义实数和无理数的概念。在Lean 4的标准库中，实数系统已经被定义，我们可以直接使用。无理数则可以定义为不能表示为两个整数之比的实数。

// 步骤1: 导入实数相关库
import Mathlib.Data.Real.Basic

// 步骤2: 定义无理数概念
def Irrational (x : ℝ) : Prop := 
  ¬∃ (a b : ℤ), b ≠ 0 ∧ x = a / b

这段代码中，我们首先导入了实数相关的基础库，然后定义了一个谓词Irrational，它表示一个实数x是无理数，当且仅当不存在整数a和非零整数b，使得x等于a除以b。

接下来，我们可以形式化"√2是无理数"这一命题：

// 步骤3: 形式化目标命题
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) := by
  sorry  -- 这里将填入证明内容

这里，theorem关键字用于声明一个定理，sqrt_two_irrational是定理的名称，: Irrational (Real.sqrt 2)表示定理的类型，即"√2是无理数"这一命题。by sorry表示我们暂时还没有完成证明，这是Lean 4中常用的占位符。

通过这样的形式化过程，我们将自然语言的数学命题转化为了Lean 4能够理解和处理的精确表述，为后续的证明奠定了基础。

如何将自然语言证明转化为Lean代码？

将自然语言证明转化为Lean代码是形式化证明的核心环节。这一过程需要我们深入理解数学证明的逻辑结构，并将其逐步转化为Lean 4的证明策略和战术。下面，我们以"√2是无理数"的证明为例，展示完整的形式化证明工作流。

首先，我们回顾一下"√2是无理数"的经典证明思路：假设√2是有理数，那么它可以表示为两个互质整数a和b的比值，即√2 = a/b。两边平方得到2 = a²/b²，从而a² = 2b²。这意味着a²是偶数，因此a也是偶数。设a = 2k，代入上式得到(2k)² = 2b²，即4k² = 2b²，化简得2k² = b²，因此b²也是偶数，b也是偶数。这与a和b互质矛盾，因此假设不成立，√2是无理数。

现在，我们将这个自然语言证明转化为Lean 4代码：

// 步骤1: 导入所需库
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.NormNum

// 步骤2: 定义无理数概念
def Irrational (x : ℝ) : Prop := 
  ¬∃ (a b : ℤ), b ≠ 0 ∧ x = a / b

// 步骤3: 证明辅助引理：若a²是偶数，则a是偶数
lemma even_square_implies_even (a : ℤ) : Even (a * a) → Even a := by
  intro h
  cases' h with k hk
  have : a * a = 2 * k := hk
  norm_num at this  -- 使用自动化战术化简
  cases a with
  | ofNat n => 
    induction n with
    | zero => exact Even.zero
    | succ n ih =>
      have : (n + 1) * (n + 1) = 2 * k := this
      norm_num at this
      cases n % 2 with
      | zero => exact Even.ofNat (n + 1)
      | succ m => exfalso; norm_num at this
  | negSucc n =>
    have : (-n - 1) * (-n - 1) = 2 * k := this
    norm_num at this
    exact Even.neg (even_square_implies_even (n + 1) (Even.ofNat _))

// 步骤4: 证明√2是无理数
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) := by
  intro h  -- 假设√2是有理数，即存在a, b使得√2 = a/b且b ≠ 0
  cases h with | exists a b hb =>
    have hb' : b ≠ 0 := hb.1
    have eq : Real.sqrt 2 = a / b := hb.2
    have eq_sq : 2 = (a / b) ^ 2 := by rw [eq]; exact sq_sqrt (by norm_num)
    have : a^2 = 2 * b^2 := by 
      rw [pow_div, eq_sq]
      field_simp [hb']
      ring
    have even_a_sq : Even (a^2) := by
      rw [this]
      exact Even.mul 2 (b^2)
    have even_a : Even a := even_square_implies_even a even_a_sq
    cases even_a with | exists k hk =>
      have a_eq : a = 2 * k := hk
      rw [a_eq] at this
      have : 4 * k^2 = 2 * b^2 := this
      have : 2 * k^2 = b^2 := by simp [this]
      have even_b_sq : Even (b^2) := by
        rw [this]
        exact Even.mul 2 (k^2)
      have even_b : Even b := even_square_implies_even b even_b_sq
      cases even_b with | exists m hm =>
        have b_eq : b = 2 * m := hm
        have : a = 2 * k ∧ b = 2 * m := ⟨a_eq, b_eq⟩
        have gcd_ab : gcd a b = 2 * gcd k m := by
          rw [a_eq, b_eq]
          exact gcd_mul_left 2 k (2 * m)
        have gcd_pos : 2 * gcd k m > 0 := by
          apply mul_pos
          exact zero_lt_two
          exact gcd_nonneg k m
        have : gcd a b = 1 := by
          apply Int.gcd_eq_one_of_coprime
          sorry  -- 这里需要补充a和b互质的证明
        linarith  -- 得出矛盾，证明完成

这个证明过程展示了从自然语言到形式化代码的完整转化。我们首先定义了必要的辅助引理，然后逐步应用逻辑推理和数学运算，最终得出矛盾，从而证明了命题。在实际的证明过程中，我们可以使用Lean 4提供的各种自动化战术，如norm_num、ring、linarith等，来简化证明步骤。

这张流程图展示了形式化证明的一般工作流程，从命题形式化到证明构造，再到验证和优化。通过遵循这一流程，我们可以系统地构建复杂的数学证明。

如何解决形式化证明中的常见错误？

在形式化证明过程中，初学者常常会遇到各种错误和困难。了解这些常见问题及其解决方案，可以帮助我们更高效地进行证明。下面我们介绍几个典型的错误案例及应对方法。

错误1：类型不匹配

问题描述：在证明过程中，经常会遇到类型不匹配的错误，例如将整数和实数混淆使用。

示例代码：

def add_five (x : ℕ) : ℕ := x + 5

theorem test : add_five 3 = 8.0 := by rw [add_five]; rfl

错误分析：这里add_five函数的返回类型是自然数ℕ，而右边的8.0是实数ℝ，类型不匹配。

解决方案：确保参与运算的变量和常量具有相同的类型。如果需要在不同类型之间转换，可以使用相应的转换函数，如Nat.toReal将自然数转换为实数。

修正代码：

def add_five (x : ℕ) : ℕ := x + 5

theorem test : add_five 3 = 8 := by rw [add_five]; rfl

错误2：假设引入不当

问题描述：在使用intro战术引入假设时，如果引入的假设与后续证明无关，会导致证明目标变得复杂。

示例代码：

theorem example_error : ∀ x y : ℕ, x + y = y + x := by
  intro x y z  -- 错误地引入了多余的变量z
  sorry

错误分析：这里定理只涉及两个变量x和y，但intro x y z引入了三个变量，导致后续证明中出现未使用的变量z。

解决方案：仔细分析定理的结构，只引入必要的假设和变量。

修正代码：

theorem example_fixed : ∀ x y : ℕ, x + y = y + x := by
  intro x y  -- 只引入必要的变量x和y
  induction x with
  | zero => rw [Nat.zero_add, Nat.add_zero]
  | succ x ih => rw [Nat.succ_add, Nat.add_succ, ih]

错误3：忽略必要的前提条件

问题描述：在证明中忽略了定理所需的前提条件，导致证明无法完成或得出错误结论。

示例代码：

theorem divisible_by_two (n : ℕ) : Even n := by
  sorry  -- 没有考虑n是否为偶数的前提条件

错误分析：这个定理声称所有自然数都是偶数，显然是错误的。问题在于没有添加必要的前提条件。

解决方案：明确声明定理的前提条件，并在证明中使用这些条件。

修正代码：

theorem divisible_by_two (n : ℕ) (h : Even n) : ∃ k : ℕ, n = 2 * k := by
  cases h with | exists k hk => exact ⟨k, hk⟩

通过识别和解决这些常见错误，我们可以提高形式化证明的效率和正确性。在实际证明过程中，还需要不断积累经验，熟悉Lean 4的各种战术和库函数，才能更顺利地完成复杂的证明任务。

如何应用形式化证明解决复杂数学问题？

掌握了形式化证明的基本方法后，我们可以将其应用于更复杂的数学问题。下面介绍几个进阶应用案例，并提供相应的练习命题，帮助读者进一步提升技能。

案例1：数列极限的形式化证明

数列极限是数学分析中的重要概念。在Lean 4中，我们可以使用过滤器（Filter）来定义数列的极限：

import Mathlib.Data.Real.Basic
import Mathlib.Topology.Filter.Basic

def seq_limit (a : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - l| < ε

theorem limit_sq (a : ℕ → ℝ) (l : ℝ) (h : seq_limit a l) :
  seq_limit (fun n => (a n)^2) (l^2) := by
  intro ε ε_pos
  have : 2 * |l| + 1 > 0 := by linarith
  let δ := min (ε / (2 * |l| + 1)) 1
  have δ_pos : δ > 0 := by
    apply min_pos
    · apply div_pos ε_pos (by linarith)
    · exact one_pos
  cases h δ δ_pos with | exists N hN =>
    use N
    intro n n_ge_N
    have : |a n - l| < δ := hN n n_ge_N
    have : |a n| < |l| + δ := by
      calc |a n| = |l + (a n - l)| ≤ |l| + |a n - l| := abs_add l (a n - l)
              _ < |l| + δ := by linarith [this]
    calc |(a n)^2 - l^2| = |a n - l| * |a n + l| := abs_mul (a n - l) (a n + l)
                        _ ≤ |a n - l| * (|a n| + |l|) := by apply mul_le_mul_of_nonneg_left (abs_add (a n) l) (abs_nonneg (a n - l))
                        _ < δ * (|a n| + |l|) := by linarith [this]
                        _ < δ * (|l| + δ + |l|) := by linarith [this]
                        _ = δ * (2 * |l| + δ) := by ring
                        _ ≤ δ * (2 * |l| + 1) := by
                          apply mul_le_mul_right (le_add_right (2 * |l|) δ) (δ_pos.le)
                          exact δ ≤ 1
                        _ < (ε / (2 * |l| + 1)) * (2 * |l| + 1) := by linarith [δ ≤ ε / (2 * |l| + 1)]
                        _ = ε := by ring

这个定理证明了如果数列a的极限是l，那么数列a的平方的极限是l的平方。证明过程中使用了极限的定义和绝对值不等式的性质，展示了如何将分析学中的标准证明转化为形式化代码。

案例2：连续函数的性质证明

连续性是数学分析中的核心概念。在Lean 4中，我们可以使用极限来定义函数的连续性，并证明连续函数的各种性质：

import Mathlib.Data.Real.Basic
import Mathlib.Topology.ContinuousFunctions.Basic

def continuous_at (f : ℝ → ℝ) (x : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ y, |y - x| < δ → |f y - f x| < ε

theorem continuous_add (f g : ℝ → ℝ) (x : ℝ)
  (hf : continuous_at f x) (hg : continuous_at g x) :
  continuous_at (fun y => f y + g y) x := by
  intro ε ε_pos
  cases hf (ε / 2) (div_pos ε_pos two_pos) with | exists δf hf' =>
  cases hg (ε / 2) (div_pos ε_pos two_pos) with | exists δg hg' =>
  let δ := min δf δg
  have δ_pos : δ > 0 := min_pos hf'.1 hg'.1
  use δ
  intro y hy
  have : |f y - f x| < ε / 2 := hf' y (le_of_lt (min_le_left δf δg) hy)
  have : |g y - g x| < ε / 2 := hg' y (le_of_lt (min_le_right δf δg) hy)
  calc |(f y + g y) - (f x + g x)| = |(f y - f x) + (g y - g x)|
                              ≤ |f y - f x| + |g y - g x| := abs_add (f y - f x) (g y - g x)
                              < ε / 2 + ε / 2 := by linarith
                              = ε := by ring

这个定理证明了两个连续函数的和仍然是连续函数。证明过程中使用了连续性的定义和三角不等式，展示了如何组合多个函数的性质来证明复合函数的性质。

练习命题

以下是三个难度递进的练习命题，读者可以尝试使用Lean 4进行形式化证明：

1. 基础题：证明对于所有自然数n，1 + 2 + ... + n = n(n + 1)/2。

   • 提示路径：使用数学归纳法，先证明n=0的情况，再假设n=k时成立，证明n=k+1时也成立。

2. 中级题：证明闭区间套定理：如果{[a_n, b_n]}是一系列闭区间，满足a_n ≤ a_{n+1} ≤ b_{n+1} ≤ b_n，且lim_{n→∞} (b_n - a_n) = 0，则存在唯一的实数c属于所有闭区间。

   • 提示路径：首先证明数列{a_n}单调递增有上界，数列{b_n}单调递减有下界，因此两者都有极限。然后证明这两个极限相等，记为c，最后证明c属于所有闭区间。

3. 高级题：证明微积分基本定理：如果函数f在闭区间[a, b]上连续，且F是f的一个原函数，则∫ₐᵇ f(x) dx = F(b) - F(a)。

   • 提示路径：使用定积分的定义和连续函数的性质，构造黎曼和并证明其极限等于F(b) - F(a)。

通过这些练习，读者可以逐步提升形式化证明的能力，掌握更复杂的数学概念和证明技巧。

交互式学习资源

为了帮助读者更好地学习和掌握Lean 4的形式化证明，以下提供一些官方学习资源：

• 官方文档：包含详细的教程和参考资料，从基础语法到高级证明技巧都有覆盖。
• 示例库：提供了大量的形式化证明示例，涵盖数学的各个领域，读者可以通过学习这些示例来掌握证明方法。
• 社区论坛：可以在论坛上提问、分享证明经验，与其他Lean用户交流学习心得。

通过这些资源，读者可以系统地学习Lean 4的形式化证明技术，不断提升自己的数学形式化能力。无论是学术研究还是实际应用，掌握形式化证明都将为您带来巨大的价值。

总之，形式化数学证明是一项强大的技能，它不仅能够确保数学命题的绝对正确性，还能培养严谨的逻辑思维能力。通过本文介绍的三个关键步骤，从命题形式化到证明构造，再到错误处理和进阶应用，读者可以逐步掌握Lean 4的形式化证明技术。希望本文能够帮助您开启数学形式化之旅，探索数学世界的无限可能。