Lean实数[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

Lean实数是Lean定理证明器中对实数（Real Numbers）的形式化实现。在数学基础中，实数包含所有有理数和无理数，构成连续统的核心结构。Lean通过其数学库（如mathlib）提供了严格的实数定义和完备的操作体系，使程序员和数学家能够以形式化方式验证实数相关定理。

在Lean中，实数被构造为柯西序列（Cauchy sequences）或戴德金分割（Dedekind cuts）的等价类，这保证了其逻辑严密性。对于程序员而言，Lean实数不仅支持常规算术运算，还提供分析学工具（如极限、导数、积分）。

定义与构造[编辑 | 编辑源代码]

Lean中实数的核心定义基于以下结构（来自mathlib）：

import data.real.basic

-- ℝ 是Lean中实数的类型
def sample_real : ℝ := 3.1415926535

关键构造原理：

公理化定义：满足实数公理（有序域完备性）。
计算实现：依赖底层类型系统，支持精确计算与符号运算。

等价构造对比[编辑 | 编辑源代码]

基本操作[编辑 | 编辑源代码]

算术运算[编辑 | 编辑源代码]

-- 加法示例
example : ℝ := 2 + 2  -- 结果为 4

-- 乘法与平方根
example : ℝ := √2 * √2  -- 结果为 2

不等式与绝对值[编辑 | 编辑源代码]

lemma abs_property (x : ℝ) : |x| ≥ 0 :=
abs_nonneg x

分析学应用[编辑 | 编辑源代码]

极限与连续性[编辑 | 编辑源代码]

Lean可形式化验证极限定义： $\lim_{x \to a} f (x) = L ⟺ \forall ϵ > 0, \exists δ > 0, | x - a | < δ ⟹ | f (x) - L | < ϵ$

对应代码：

import analysis.calculus.limits

example (f : ℝ → ℝ) (a L : ℝ) :
  tendsto f (𝓝 a) (𝓝 L) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |f x - L| < ε :=
metric.tendsto_nhds_nhds

微分与积分[编辑 | 编辑源代码]

import analysis.calculus.deriv

-- 导数计算
example : deriv (λ x, x^2) = λ x, 2 * x :=
by { apply deriv_pow, norm_num }

实际案例[编辑 | 编辑源代码]

验证平方根性质[编辑 | 编辑源代码]

证明√2是无理数：

import data.real.irrational

theorem sqrt_two_irrational : irrational (√2) :=
irrational_sqrt_two

工程近似计算[编辑 | 编辑源代码]

使用泰勒级数近似e的数值：

import analysis.special_functions.exp

-- e ≈ 2.718281828459045
example : ℝ := real.exp 1

常见问题[编辑 | 编辑源代码]

精度处理[编辑 | 编辑源代码]

Lean区分精确实数与浮点近似：

-- 精确计算
example : (√2)^2 = 2 := by simp

-- 浮点近似（需转换）
example : float.sqrt 2.0 ^ 2 ≈ 2.0 :=
by { norm_num, apply float.sqrt_approx }

计算效率[编辑 | 编辑源代码]

符号运算（如√2）保持精确性，而数值方法（如牛顿迭代）需显式声明近似需求。

扩展阅读[编辑 | 编辑源代码]

实数完备性定理（Bolzano-Weierstrass、Heine-Borel等）
Lean中的拓扑空间形式化
非标准分析（hyperreals）的替代实现

总结[编辑 | 编辑源代码]

Lean实数系统为形式化数学提供了可靠基础，其特点包括：

严格性：基于公理化集合论或类型论
可操作性：与编程语言无缝集成
可扩展性：支持高阶分析学构造

通过结合数学理论与计算实践，Lean使实数操作既可用于教育演示，也能胜任前沿研究验证。