Lean数论基础

Lean数论基础

介绍

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

基本概念

整除性与模运算

在数论中，整除性（Divisibility）是一个核心概念。若整数$a$能被整数$b$整除（记作$b\mid a$），则存在整数$k$使得$a=b\cdot k$。在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

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

-- 计算 7 mod 3
#eval 7 % 3  -- 输出: 1

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

素数

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

import data.nat.prime

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

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

实际案例

欧几里得算法

欧几里得算法（Euclidean Algorithm）用于计算两个数的最大公约数（GCD）。以下是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

费马小定理

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

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

图表与可视化

模运算的循环性

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

graph LR 0 --> 1 1 --> 2 2 --> 3 3 --> 4 4 --> 0

总结

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

下一步学习建议

• 探索`mathlib`中更高级的数论内容，如二次剩余或中国剩余定理。
• 尝试形式化其他经典定理，如威尔逊定理或欧拉定理。