编辑“︁Lean形式化数学”︁

{{DISPLAYTITLE:Lean形式化数学}}

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

== 核心概念 ==

=== 什么是形式化数学？ ===
形式化数学是指用严格的逻辑语言（通常是基于类型论的证明辅助工具）描述数学对象和证明过程。其特点包括：
* '''机器可验证性'''：所有证明步骤必须通过计算机检查
* '''构造性'''：许多系统（如Lean）支持构造性数学（如直觉逻辑）
* '''可复用性'''：已证明的定理可以作为后续证明的基础

=== Lean的类型论基础 ===
Lean基于'''[[依值类型论]]'''（Dependent Type Theory），其中：
* 每个表达式都有类型，记作<code>x : T</code>
* 类型本身也是一等公民（类型可以有类型）
* 命题即类型（Curry-Howard对应）

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

== 基础语法 ==

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

<syntaxhighlight lang="lean">
-- 命题声明
theorem and_comm (p q : Prop) : p ∧ q → q ∧ p :=
-- 证明过程
λ h : p ∧ q, ⟨h.right, h.left⟩
</syntaxhighlight>

输出解释：
* 声明了一个关于逻辑与交换律的定理
* <code>λ h</code> 引入假设
* <code>⟨h.right, h.left⟩</code> 构造新证明

=== 常见数学结构 ===

<syntaxhighlight lang="lean">
-- 自然数定义
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)
</syntaxhighlight>

== 实际案例 ==

=== 斐波那契数列形式化 ===

<mermaid>
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)]
</mermaid>

对应Lean实现：

<syntaxhighlight lang="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
</syntaxhighlight>

=== 群论形式化 ===

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 证明策略 ==

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

{| class="wikitable"
! 策略 !! 描述 !! 示例
|-
| <code>intro</code> || 引入假设 || <code>intro h</code>
|-
| <code>apply</code> || 应用定理 || <code>apply and_comm</code>
|-
| <code>simp</code> || 简化表达式 || <code>simp [add_zero]</code>
|-
| <code>induction</code> || 归纳法 || <code>induction n</code>
|}

== 高级主题 ==

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

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

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

=== 范畴论形式化 ===

<syntaxhighlight lang="lean">
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
  -- 公理省略...
</syntaxhighlight>

== 学习建议 ==

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

{{重要提示|Lean形式化数学需要同时理解数学概念和编程实现，建议结合经典数学证明与形式化练习同步学习。}}

== 参见 ==
* [[定理证明]]
* [[依值类型论]]
* [[构造性数学]]

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean证明基础]]