Lean形式化数学

Lean形式化数学是使用Lean定理证明器将数学定理和证明过程转化为计算机可验证的代码形式的过程。它结合了数学逻辑、类型论和函数式编程，为数学研究提供了严格的验证工具。本章将介绍Lean形式化数学的基本原理、核心语法和实际应用。

核心概念

什么是形式化数学？

形式化数学是指用严格的逻辑语言（通常是基于类型论的证明辅助工具）描述数学对象和证明过程。其特点包括：

• 机器可验证性：所有证明步骤必须通过计算机检查
• 构造性：许多系统（如Lean）支持构造性数学（如直觉逻辑）
• 可复用性：已证明的定理可以作为后续证明的基础

Lean的类型论基础

Lean基于依值类型论（Dependent Type Theory），其中：

• 每个表达式都有类型，记作x : T
• 类型本身也是一等公民（类型可以有类型）
• 命题即类型（Curry-Howard对应）

数学公式示例： $\prod _{x:A}B(x)$ 表示依赖乘积类型（即对于所有x属于A，存在B(x)类型）

基础语法

命题与证明

在Lean中，命题被表示为类型，证明则是该类型的项：

-- 命题声明
theorem and_comm (p q : Prop) : p ∧ q → q ∧ p :=
-- 证明过程
λ h : p ∧ q, ⟨h.right, h.left⟩

输出解释：

• 声明了一个关于逻辑与交换律的定理
• λ h 引入假设
• ⟨h.right, h.left⟩ 构造新证明

常见数学结构

-- 自然数定义
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

-- 加法定义
def add : Nat → Nat → Nat
  | m, Nat.zero   => m
  | m, Nat.succ n => Nat.succ (add m n)

实际案例

斐波那契数列形式化

graph TD A[定义Fib函数] --> B[基础情况] A --> C[递归情况] B --> D[Fib 0 = 0] B --> E[Fib 1 = 1] C --> F[Fib n = Fib (n-1) + Fib (n-2)]

对应Lean实现：

def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | (n+2) => fib (n+1) + fib n

-- 性质证明
theorem fib_pos (n : Nat) : 0 < fib (n+1) := by
  induction n with
  | zero => simp [fib]
  | succ n ih => simp [fib]; linarith

群论形式化

class Group (G : Type) where
  mul : G → G → G
  one : G
  inv : G → G
  mul_assoc : ∀ x y z, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x, mul x one = x
  one_mul : ∀ x, mul one x = x
  mul_left_inv : ∀ x, mul (inv x) x = one

证明策略

Lean提供多种自动化证明策略：

策略	描述	示例
intro	引入假设	intro h
apply	应用定理	apply and_comm
simp	简化表达式	simp [add_zero]
induction	归纳法	induction n

高级主题

元编程

Lean允许在语言内进行元编程：

-- 定义符号宏
macro "∅" : term => `(∅)
macro "ℝ" : term => `(Real)

-- 生成重复定理
#check show_term by
  repeat' (apply And.intro; try assumption)

范畴论形式化

structure Category where
  Obj : Type u
  Hom : Obj → Obj → Type v
  id : ∀ X : Obj, Hom X X
  comp : ∀ {X Y Z}, Hom X Y → Hom Y Z → Hom X Z
  -- 公理省略...

学习建议

• 从基础命题逻辑开始，逐步过渡到代数结构
• 善用Lean库（Mathlib）中的现有定义
• 使用#check和#eval命令交互式学习
• 参考标准数学教材的对应形式化版本

参见

• 定理证明
• 依值类型论
• 构造性数学