编辑“︁Lean数论基础”︁（章节）

= Lean数论基础 =

== 介绍 ==  
'''Lean数论基础'''是使用Lean定理证明器研究数论（Number Theory）的入门指南。数论是数学的一个分支，专注于研究整数的性质及其相互关系，而Lean作为一个交互式定理证明器，能够帮助用户形式化这些性质并进行严格的验证。本章节将介绍如何在Lean中定义和证明基本的数论概念，如整除性、素数、模运算等，适合初学者及需要了解形式化数学的程序员。

== 基本概念 ==  

=== 整除性与模运算 ===  
在数论中，'''整除性'''（Divisibility）是一个核心概念。若整数<math>a</math>能被整数<math>b</math>整除（记作<math>b \mid a</math>），则存在整数<math>k</math>使得<math>a = b \cdot k</math>。在Lean中，可以通过以下方式定义：

<syntaxhighlight lang="lean">
-- 定义整除性
def divides (a b : ℤ) : Prop := ∃ k, b = a * k

-- 示例：证明 2 整除 4
example : divides 2 4 :=
begin
  use 2,  -- 存在 k = 2 使得 4 = 2 * 2
  norm_num,
end
</syntaxhighlight>

'''模运算'''（Modular Arithmetic）是另一个重要概念，表示整数除法后的余数。在Lean中，可以使用`%`运算符或定义等价关系：

<syntaxhighlight lang="lean">
-- 计算 7 mod 3
#eval 7 % 3  -- 输出: 1

-- 定义模等价
def mod_equiv (a b n : ℤ) : Prop := n ∣ (a - b)
</syntaxhighlight>

=== 素数 ===  
'''素数'''（Prime Numbers）是大于1且只有1和自身两个正因数的自然数。Lean的标准库`mathlib`提供了素数的定义：

<syntaxhighlight lang="lean">
import data.nat.prime

-- 检查 5 是否为素数
#eval nat.prime 5  -- 输出: true

-- 证明 7 是素数
example : nat.prime 7 :=
begin
  norm_num,  -- 通过计算验证
end
</syntaxhighlight>

== 实际案例 ==  

=== 欧几里得算法 ===  
欧几里得算法（Euclidean Algorithm）用于计算两个数的最大公约数（GCD）。以下是Lean中的实现：

<syntaxhighlight lang="lean">
import data.nat.gcd

-- 计算 gcd(12, 8)
#eval nat.gcd 12 8  -- 输出: 4

-- 证明 gcd(a, b) 整除 a 和 b
example (a b : ℕ) : nat.gcd a b ∣ a ∧ nat.gcd a b ∣ b :=
begin
  exact ⟨nat.gcd_dvd_left a b, nat.gcd_dvd_right a b⟩,
end
</syntaxhighlight>

=== 费马小定理 ===  
'''费马小定理'''（Fermat's Little Theorem）是数论中的一个经典结果，指出若<math>p</math>是素数且<math>a</math>不被<math>p</math>整除，则<math>a^{p-1} \equiv 1 \mod p</math>。以下是形式化证明的框架：

<syntaxhighlight lang="lean">
import data.nat.prime
import data.zmod.basic

-- 费马小定理的陈述
theorem fermat_little (p : ℕ) (hp : nat.prime p) (a : ℤ) (hpa : ¬(p ∣ a)) :
  a^(p-1) ≡ 1 [ZMOD p] :=
begin
  -- 此处省略详细证明，实际需调用 mathlib 中的相关引理
  sorry,
end
</syntaxhighlight>

== 图表与可视化 ==  

=== 模运算的循环性 ===  
模运算具有周期性，可以用图表展示<math>\mathbb{Z}/5\mathbb{Z}</math>的加法结构：

<mermaid>
graph LR
    0 --> 1
    1 --> 2
    2 --> 3
    3 --> 4
    4 --> 0
</mermaid>

== 总结 ==  
Lean为形式化数论提供了强大的工具，从基本的整除性到高级定理如费马小定理均可严谨表达。通过结合数学定义与交互式证明，用户可以深入理解数论概念并验证其正确性。  

== 下一步学习建议 ==  
* 探索`mathlib`中更高级的数论内容，如二次剩余或中国剩余定理。  
* 尝试形式化其他经典定理，如威尔逊定理或欧拉定理。

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