Some content in this article was created with AI assistance. Please verify as needed.

如果只看 def、函数调用和模式匹配，Lean 很像一门语法稍显特殊的函数式语言。实际写起来，类型检查会计算表达式，递归函数可能要证明终止，tactic 生成的定理还要再交给 kernel 检查。普通语言的编译流程不足以解释这些现象。

Lean 用依赖类型统一描述程序与证明。语法本身不算难记，先要放下“类型只约束运行时数据”这一习惯。本篇整理后续内容所需的语言背景。

语言定位

编程语言与定理证明器

Lean 是基于依赖类型理论的交互式定理证明器，也是一门严格求值的纯函数式语言。普通函数、数学定义、证明以及编译期扩展都写在 Lean 中，并登记到同一个声明环境。区别在于声明的类型以及代码在哪个阶段执行。

作为编程语言，Lean 有代数数据类型、模式匹配、高阶函数、类型类、Monad、宏和原生代码编译器。它的表面结构与 Haskell、OCaml 有不少相似之处。作为定理证明器，Lean 把命题放在 Prop 中，把证明保存为相应类型的项。tactic 负责构造这种项，不负责改变内核的检查规则。

def 通常构造可执行数据，theorem 构造证明，二者都要经过 elaboration 和类型检查。Lean 的宏、elaborator 与 tactic 也使用 Lean 编写。阅读报错时需要分清这些代码所在的编译阶段。

工具链与生态

Lean 项目由 Leonardo de Moura 于 2013 年在 Microsoft Research 发起。Lean 4 重写了主要实现，并用 Lean 自身实现了大量组件。当前开发由 Lean FRO 和开源社区推进，源码采用 Apache 2.0 许可证。

Lean 4 并非 Lean 3 的语法更新版。宏系统、elaborator、类型类搜索、编译器和元编程接口均有较大变化。检索资料时应确认其版本；Lean 3 教程中的导入路径、tactic 名称和库 API 通常不能直接用于 Lean 4。

Lake 项目通过 lean-toolchain 固定 Lean 版本，mathlib 也与特定 Lean 版本配套。网页示例无法运行时，版本和导入模块比语法本身更值得先查。

Lean 的工具链和库可以分为三个层次：

层次 内容
Lean 核心与工具链 语言、内核、编译器、运行时、宏和元编程设施
Std 常用容器、算法、IO 接口和工程工具
mathlib 数学定义、定理、notation 和证明自动化

本系列前三篇语言笔记主要依赖 Lean 与 Std，证明和数学部分使用 mathlib。某个名称无法解析，往往只是没有导入定义它的模块。语言基础示例也不宜一律 import Mathlib，否则很难判断 notation 和 tactic 究竟来自核心、Std 还是 mathlib。

mathlib 收录定理，也规定了大量数学对象的建模方式、类型类层级、命名习惯和自动化接口。使用 mathlib，需要理解并沿用这些既有抽象。

类型、证明与计算

依赖类型

Python 和 MATLAB 的类型主要描述运行时值支持哪些操作。C++ 可以通过非类型模板参数把常量带入类型，例如 std::array<double, 3>，但模板参数和普通函数参数仍处在不同机制中。Lean 的依赖函数类型直接允许返回类型依赖普通参数：

1
2
3
#check Fin 5
#check Vector Nat 3
#check (fun n : Nat => Fin (n + 1))

Fin 5 表示小于 5 的自然数，Vector Nat 3 表示长度为 3 的自然数向量。这里的 5 和 3 是类型的一部分，而不是对象创建后才检查的字段。

传统接口可能分别接收数组和长度，并在函数内部核对二者。Lean 可以把长度放进类型，使不一致的调用无法通过 elaboration。C++ 的 std::array<T, N> 和 Haskell 配合 DataKinds、GADT 定义的定长向量也能表达类似约束；Lean 的区别在于值依赖是语言类型理论的基本组成，而不是模板系统或一组 GHC 扩展提供的附加层。

这不意味着条件越多、类型越复杂越好。外部输入仍然需要动态检查；当证明成本高于静态保证的收益时，返回 Option、Except 或使用布尔判断更直接。

Lean 采用 Curry–Howard 对应：命题是类型，证明是该类型的项。下面两个定义在语法结构上没有根本区别：

1
2
3
4
5
def double (n : Nat) : Nat :=
  n + n

theorem add_zero (n : Nat) : n + 0 = n :=
  rfl

第一个定义构造 Nat，第二个定理构造等式类型 n + 0 = n 的证明。rfl 是一个证明项，说明等式两侧经过定义归约后相同。

这不表示数学证明会像普通数据一样全部保留到运行时。Prop 中的证明通常可以被擦除，而且 Lean 对证明采用 proof irrelevance：只关心某个命题是否有证明，不区分证明对象的运行时内容。程序与证明共享类型系统，但编译器可以按用途处理它们。

依赖类型中，类型本身可以包含函数调用。内核比较两个类型时，可能需要展开定义、归约模式匹配或计算递归函数。这种“定义相等”比普通语言中的名称相同或结构相同更强。

例如，某个函数返回长度为 2 + 1 的向量，另一个位置要求长度为 3 的向量。只要这些表达式能归约到同一个结果，内核就可以把两种类型视为相同，而不需要额外证明。

内核不会任意调用数学定理改写类型。按照自然数加法的递归方向，n + 0 可以直接归约，而 0 + n 对变量 n 不能完成同样的计算，此时需要显式定理。因此，有些等式可由 rfl 证明，另一些数学上同样直接的等式却需要归纳或重写。

Elaboration

Lean 源码省略了大量信息。隐式参数、类型类实例、部分 coercion、notation 的展开结果以及 tactic 生成的证明项，都由 elaborator 补全。这个过程称为 elaboration。

大致流程如下：

1
2
3
4
5
6
7
源码
  ↓ parser / macro expansion
语法树
  ↓ elaboration / typeclass search / tactic execution
带完整类型信息的核心项
  ├─→ kernel 检查
  └─→ compiler 编译可执行部分

所以 Lean 中相当一部分报错既不是语法错误，也不是运行时异常，而是 elaborator 无法确定某个省略项。常见原因有：

  • 预期类型不足，无法确定重载字面量或运算符；
  • 隐式参数无法从其他参数反推；
  • 找不到需要的类型类实例；
  • notation 在当前作用域没有打开；
  • tactic 没能构造符合目标类型的证明项。

长错误信息通常由一个未解决的 metavariable 引起。先看第一个失败位置和当时的期望类型，后面的报错可能只是级联结果。

C++ 模板实例化和 Haskell 类型推断也会补全源码中没有明写的信息，但 Lean 的 elaborator 还会执行 tactic，并输出完整证明项。这个输出不是最终裁决：内核会重新检查它。把 elaborator 和 kernel 分开，有助于理解“自动化可以很复杂，但可信检查器仍然很小”这句话。

Lean 的普通函数是纯函数：相同输入给出相同输出，不能暗中修改全局状态、读取文件或打印终端。外部效果通过 IO α 等类型表示。

1
2
3
4
5
def pureMessage (name : String) : String :=
  "hello, " ++ name

def printMessage (name : String) : IO Unit :=
  IO.println (pureMessage name)

pureMessage 返回字符串，printMessage 返回一个描述 IO 计算的值。类型签名已经表明后者可能产生外部效果。

Python、MATLAB 和通常的 C++ 接口不会在返回类型中标明打印、文件访问或共享状态修改。Lean 与 Haskell 都把外部效果放入 IO，并用 Monad 和 do 语法组合计算。两者的明显区别是求值策略：Lean 严格求值，Haskell 默认惰性求值。写普通 Lean 程序时，参数求值顺序的直觉更接近 OCaml，而不是 Haskell。

纯函数也不意味着实现一定低效。Lean 4 使用引用计数和 functional-but-in-place 优化：当运行时确认对象没有共享别名时，可以在不改变纯函数语义的前提下复用存储。源码保持不可变接口，编译器仍有机会生成原地更新。

普通递归定义必须让 Lean 确认递归调用终止。这条限制不是一般函数式语言的性能检查，而是逻辑一致性所需的条件。

结构递归直接在构造器的较小字段上调用自身；其他递归可以提供递减度量和终止证明。只用于运行时的递归程序可以写成 partial def，但这种定义不能像全函数一样参与逻辑归约。

终止检查保证定义可以安全归约，也使相应的递归原理可用于证明。

Haskell 允许一般递归，并存在 undefined 这样的底值。因此，虽然 Curry–Howard 对应同样能解释不少 Haskell 类型技巧，普通 Haskell 程序不能直接当作由小内核检查的数学证明。Lean 为逻辑部分付出的主要代价，正是终止性和可计算性限制。

源码阅读

类型优先

Lean 声明最好从类型开始读。函数体说明如何构造结果，类型则先确定调用方式以及结果承担的约束：

  • 哪些参数由调用者显式提供；
  • 哪些参数放在 {} 中由 elaborator 推断；
  • 哪些 [] 参数需要类型类搜索；
  • 函数返回普通数据、带错误的数据，还是一个证明；
  • 结果是否依赖某个输入值。

例如：

1
#check @List.map

前缀 @ 使 Lean 显示通常隐藏的隐式参数。阅读陌生 API 时，可用 #check、编辑器悬停和定义跳转确认参数顺序。

代数数据类型规定值如何构造，模式匹配和递归原理规定值如何使用。阅读定义时可从两个方面分析：

  1. 这个类型有哪些构造器？
  2. 当前函数对每个构造器做什么？

同一套读法也适用于证明。构造 P ∧ Q 要给出 P 和 Q；使用 P ∨ Q 要处理两个构造分支。许多逻辑 tactic 展开后就是归纳类型的构造或模式匹配。

进入 by 块以后，InfoView 会显示局部变量、假设和当前目标。每条 tactic 都在修改这份证明状态：引入参数、拆解假设、应用定理，或者生成新的子目标。

1
2
3
4
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · exact hP
  · exact hQ

这里 constructor 选择 And.intro，产生两个子目标；两个 exact 分别提供构造器参数。对应的证明项可以直接写成：

1
2
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
  And.intro hP hQ

tactic 根据当前上下文生成证明项，结果仍由内核检查。它的报错通常可以还原为类型不匹配、参数缺失或目标形式不合适，而不是某种独立于 Lean 的“证明脚本错误”。

遇到一个目标时，可以依次判断：

  1. 两侧是否按定义计算后相同？尝试 rfl、dsimp 或展开定义；
  2. 是否需要已有等式或逻辑定理？使用 rw、exact、apply；
  3. 是否属于已知决策过程？使用 norm_num、ring、linarith、omega 等 tactic；
  4. 自动化失败后还剩什么数学事实没有提供？

自动化通常只处理特定的正规形式。先判断目标属于哪一类，再选 tactic，比逐个试名字更容易看出缺少的数学条件。

源码层次

Lean 文件的顶层由 command 组成，例如 def、theorem、inductive、structure、namespace 和 import。command 向环境加入声明，或改变后续源码的解释环境。

1
2
3
4
5
6
7
8
namespace Demo

def answer : Nat := 42

theorem answer_pos : 0 < answer := by
  decide

end Demo

42、0 < answer 和整个 by ... 都出现在 command 内部，但角色不同：

  • 42 是一个 term，其类型为 Nat；
  • 0 < answer 也是 term，其类型为 Prop；
  • by decide 是 tactic 语法，用来构造目标命题的证明项；
  • def 与 theorem 把构造出的项登记到环境中。

这里容易混淆的是运行阶段。by 中的 tactic 在 elaboration 时生成项，普通函数在编译后的程序中运行，宏则更早处理语法。C++ 也区分模板实例化、常量求值和运行时执行，Haskell 的 Template Haskell 也会在编译时运行 splice；Lean 额外要求逻辑声明最终落到内核可检查的项上。

Lean 和 mathlib 使用大量 Unicode notation。它们通常只是已有声明的表面写法：

表面写法 对应概念
α → β 函数类型
P ∧ Q And P Q
x ∈ s Membership.mem x s
a • x SMul.smul a x
V →ₗ[K] W LinearMap K V W

检索 API 时需要知道符号对应的声明名，实际代码则不必全部改写成长名称。编辑器悬停会显示类型和输入缩写，也可以从 notation 跳到底层声明。

同一个符号还可能由类型类决定含义。+ 可以表示自然数加法、整数加法、矩阵加法或用户自定义操作。elaborator 根据参数类型寻找 HAdd/Add 实例；若类型信息不足，报错往往表现为找不到实例，而不是“加号未定义”。

名称如何解释，取决于导入模块、已打开的 namespace 与 scoped notation，以及局部变量、实例和 option：

1
2
3
4
5
6
import Std

open List
open scoped BigOperators

set_option autoImplicit false

代码片段离开原文件后无法运行，常常是因为缺少顶部的 import、open 或 variable 声明。检查片段时要连同所在的 section 一起看。

namespace 主要影响名称，section 主要组织局部变量和 option，open 只影响名称解析，并不会像某些语言的模块导入那样加载文件。import 才建立模块依赖，并影响编译缓存。

下面的函数省略了自动隐式参数等信息：

1
def keep (x : α) : α := x

若启用了自动隐式参数，Lean 会引入类型参数 α；函数类型中的 universe、binder 信息和部分 coercion 也不会全部显示。使用：

1
2
#check @keep
#print keep

可以看到更多内容。需要进一步诊断时，还能临时设置 pretty-printer option：

1
2
set_option pp.explicit true in
#check @keep

完全展开的核心项很难直接阅读。排错时只显示与问题有关的部分，例如显式参数、universe 或 coercion 即可。

接口与程序设计

错误处理

以非零分母为例，约束可以放在三个位置：忽略失败情况，运行时检查，或由调用者提供证明。

1
2
3
4
5
6
7
8
def unsafeStyle (a b : Nat) : Nat :=
  a / b

def checkedStyle (a b : Nat) : Option Nat :=
  if b == 0 then none else some (a / b)

def provedStyle (a b : Nat) (_hb : b ≠ 0) : Nat :=
  a / b

第一种接口沿用 Nat 除法对零的既定定义，不报告错误；第二种把失败交给调用者处理；第三种要求调用者在调用点提供非零证明。

外部输入通常需要动态检查，适合返回 Option 或 Except。内部算法若已经维护非零不变量，证明参数可以消除重复检查。Nat 除法本来就对零有定义，第一种接口也并非非法，只是它没有报告这一输入。

是否把约束放进类型，取决于错误发生的位置和调用成本。依赖类型提供了选择，并不要求所有检查都变成证明参数。

#eval 在这里观察一个具体输入：

1
2
3
def twice (n : Nat) : Nat := n + n

#eval twice 21

全称性质要写进定理：

1
2
3
theorem twice_eq_two_mul (n : Nat) :
    twice n = 2 * n := by
  simp [twice, Nat.two_mul]

定理只覆盖陈述中写出的性质。元素保持、溢出模型或性能要求若没有进入陈述，Lean 不会自动补全。IO、性能和外部系统集成仍然更适合用测试检查。

Lean 数据默认不可变。更新结构体、数组或映射时，源码语义是构造一个新值：

1
2
3
4
5
6
structure Point where
  x : Int
  y : Int

def moveX (p : Point) (dx : Int) : Point :=
  { p with x := p.x + dx }

不可变语义不要求运行时完整复制所有数据。对象没有其他引用时，编译器可以复用存储。源码分析应以值语义为准，性能分析则还需考察容器接口、引用共享和编译结果。

局部算法需要命令式写法时，可以使用 let mut、循环和 do；共享可变状态则放入 IO.Ref 等效果类型。Lean 允许命令式表面语法，同时将状态范围和外部效果限制在类型或局部 elaboration 中。

面向对象代码常从类层级和动态分派出发。Lean 代码通常这样组织：

  • 用 structure 保存字段和不变量；
  • 用普通函数定义操作；
  • 用 typeclass 表示可自动搜索的规范接口；
  • 用结构体扩展组合已有字段；
  • 用归纳类型表示互斥的多种状态。

结构体扩展的语法有时类似继承，但不应直接套用对象生命周期、虚函数表和可变对象语义。Lean 的多态通常来自显式参数、隐式参数和类型类字典，而不是对象在运行时选择虚方法。

常见误区

证明中的 tactic 在 elaboration 阶段生成证明项，最终程序不会重新播放 tactic。搜索量大的 tactic 会拖慢编译；这与证明项在运行时是否被擦除是两个问题。

tactic 读取目标、创建 metavariable，操作的是 elaborator 状态，不是最终程序的业务状态。

simp、ring、linarith 和 omega 各自处理特定理论和正规形式。失败时，先检查目标的形式和前提是否落在 tactic 的适用范围内。

排查自动化失败时，应检查：

  • 当前目标属于等式重写、多项式、线性算术还是离散算术？
  • 关键事实是否藏在结构字段或定义中？
  • tactic 是否知道分母非零、变量非负或元素属于某集合？
  • 剩余目标是否已经超出该 tactic 的理论范围？

反复 unfold 会把结构展开成底层字段，同时丢掉 mathlib 已经提供的抽象接口。结果往往比原目标更难处理。

通常应先搜索对象的接口定理和外延定理。固定小维数计算可以展开到坐标；一般矩阵、线性映射和集合证明则宜保留在相应抽象层。仅在接口不足或需要核对具体定义时展开实现。

Lean 检查的是类型，而类型由作者编写。若需求只存在于注释中，内核看不到它；若定理陈述写错，Lean 可能严谨地证明一个无关命题。

定义和定理陈述决定了 Lean 实际检查什么。证明困难可能来自不便使用的定义；证明异常简单时，也要检查陈述是否漏掉边界条件或量词。

Bool 是可执行的两值数据，Prop 是命题所在的类型层级。布尔比较适合程序分支，命题关系适合假设、定理和改写。两者可以通过相应定理连接，但不会在所有场景下自动互换。

1
2
#check (3 == 4)  -- Bool
#check (3 = 4)   -- Prop

传统语言中，条件和断言往往都用布尔表达式表示；Lean 则要求明确区分“计算一个真假值”和“陈述一个需要证明的命题”。

同名定理可能移动模块、修改参数顺序或更换名称。网页搜索结果若来自 Lean 3、旧版 mathlib 或未导入的实验模块，直接复制往往失败。

排查时记录：

1
2
3
4
5
Lean 版本
mathlib commit
import 列表
完整错误信息
最小可复现代码

这些信息比单独给出目标状态更便于定位问题。Lake 已固定工具链时，应优先查阅与项目版本对应的文档和源码，而非为运行单个网络示例升级全局 Lean。

术语速查

术语 在 Lean 中的含义
term 具有某个类型的表达式；程序值和证明都属于 term
type 对项的分类，也可以包含值和计算
Prop 命题所在的 sort
proof term 类型为某个命题的项
kernel 检查核心项是否具有声明类型的可信组件
elaborator 补全隐式信息、解析重载并生成核心项的前端
metavariable elaboration 过程中尚待求解的占位项
tactic 根据局部上下文和目标构造证明项的程序
goal 尚未构造项的目标类型
hypothesis 局部上下文中已有的变量或证明
definitional equality 两个项通过允许的归约得到同一核心形式
propositional equality 需要一个等式证明项才能使用的相等关系
inductive type 由有限组构造器生成的类型
recursor 归纳类型自动生成的递归/归纳消去原理
typeclass 可以由实例搜索自动补全的结构参数
instance 提供某个 typeclass 结构的声明
coercion elaborator 在类型要求下插入的转换
universe 避免“所有类型的类型”自指矛盾的层级
IO α 执行外部效果后产生 α 的计算描述
noncomputable 允许定义依赖无法直接执行的经典构造
mathlib Lean 4 的主要数学库及其自动化生态

可信边界

Lean 采用小型可信内核检查完整项。parser、宏、elaborator、tactic 和外部自动化即使包含缺陷，通常也只能生成错误的项；只要内核拒绝这些项，就不会把错误结论加入环境。

小型内核并不意味着 Lean 项目自动获得绝对正确性。可信范围还包括：

  • Lean 内核实现及其基础公理；
  • 编译器、运行时和操作系统是否按预期执行程序；
  • 定理的形式化陈述是否准确表达原问题；
  • 项目是否额外引入了公理、sorry 或不安全接口。

对于纯数学定理，重点通常是内核检查的证明项和使用的公理。对于可执行程序，还要区分“在 Lean 中证明了函数的性质”和“编译后的机器程序是否忠实执行该函数”。两者相关，但可信边界并不完全相同。

Lean 中常见的计算方式包括：

方式 用途
内核归约 类型检查、定义相等、检查证明项
#reduce 按内核可见的归约规则显示结果
#eval 编译并执行可计算表达式
tactic 求值 在 elaboration 阶段运行证明自动化
最终可执行程序 通过 Lake/Lean 编译后由运行时执行

这些路径的性能和适用范围并不相同。数学实数 ℝ 适合证明，但不是机器浮点数，通常不能像 Float 一样直接执行。依赖经典选择得到的对象也可能需要标记为 noncomputable。讨论 Lean 中的“计算”时，应区分内核归约、编译执行与存在性证明。

Lean 只能保证已经形式化的性质。例如，一个排序函数若只声明 List α → List α，通过类型检查并不表示结果有序；必须在定理中明确陈述有序性和元素保持性质，再给出证明。

同样，证明了一个离散模型的定理，不自动说明模型忠实反映现实系统。形式化可以消除推导步骤中的歧义，却不能替代建模判断、数值误差分析或实验验证。

更强的类型并非唯一目标。过度依赖 subtype 和证明参数会增加调用负担。Lean 允许静态排除错误、返回可恢复错误或保留运行时检查；接口应根据错误代价和使用场景选择。

工具比较

C++ 模板元编程

C++ 模板元编程是理解 Lean 时很容易采用、也很容易用过头的类比。二者都能让编译器计算常量、根据类型选择实现，并在程序运行前拒绝某些调用。例如：

1
2
3
4
5
6
7
8
9
10
11
12
#include <array>
#include <cstddef>

template<class T, std::size_t N>
struct Vec {
    std::array<T, N> data;
};

template<class T>
concept Addable = requires (T a, T b) {
    a + b;
};

N 是非类型模板参数，Addable 则约束模板实参。这与 Vector α n、类型类参数确有相似之处，但实现位置不同。C++ 模板在一套独立的模板参数和实例化规则中工作；普通运行时参数不能直接决定函数返回类型。Lean 的 n : Nat 是普通项，同一个 Nat 及其递归函数既能出现在程序中，也能出现在类型中。

C++ 的 constexpr/consteval 负责常量求值，模板特化、SFINAE 和 concepts 负责选择或排除实例。Lean 中相近的工作分散在定义归约、elaboration、类型类搜索和 tactic 之间。名称相似并不表示检查目标相同：concept 通常检查表达式是否成立或是否合法，定理则要求一个具有目标命题类型的证明项。

static_assert 可以在编译期拒绝程序，却不会留下供小型证明内核独立检查的证明项。C++ 程序的可信边界仍是整个编译器和相关工具链；Lean 则让复杂 elaborator 生成核心项，再交给 kernel 复核。C++ 官方资料可参考 Templates FAQ 和 constexpr。

Haskell

如果只比较日常编程模型，Haskell 比 C++ 更接近 Lean。两者都有代数数据类型、模式匹配、参数多态、类型类、纯函数、IO、Monad 和 do 语法。下面这种 Haskell GADT 与 Lean 的索引归纳类型也很接近：

1
2
3
4
5
6
7
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Nat = Z | S Nat

data Vec a (n :: Nat) where
  Nil  :: Vec a 'Z
  Cons :: a -> Vec a n -> Vec a ('S n)

GHC 的 DataKinds 将数据构造器提升到 kind 层，type families 支持类型层函数。这些机制可以写出很强的类型级程序，但 term、type 与 kind 仍有明显的分层和提升规则。Lean 从一开始采用依赖类型，函数结果类型可以直接依赖参数，不需要先把一套数据声明提升到类型层。

求值策略是另一个直接影响代码习惯的差异。Haskell 默认惰性求值，Lean 严格求值。map、Monad 等接口看起来相似，但性能分析不能照搬 Haskell 的 thunk 模型。

两者在逻辑用途上的差异更大。Haskell 接受一般递归和底值，因此任意类型都可能由不终止计算或 undefined 占据。Lean 要把类型当作命题使用，就必须限制参与逻辑归约的递归定义。Haskell 的类型级编程可以编码和检查许多不变量，Lean 的 theorem/proof/kernel 则构成了明确的证明检查流程。

元编程也分属不同阶段。Haskell 的 Template Haskell 在编译期生成语法；Lean 的宏完成类似的语法变换，elaborator 和 tactic 还会读取期望类型与证明状态，最后生成内核项。

Python 与 MATLAB

Python 和 MATLAB 没有与上述机制直接对应的类型层。常用工作方式是运行样例、查看数组形状和数值结果，再通过测试固定行为。Lean 也有 #eval，但它只计算一个输入；定理中的量词才覆盖整个输入域。

对计算数学代码而言，两边通常需要同时保留。MATLAB、NumPy 或 C++ 负责浮点计算、性能实验和外部接口，Lean 适合描述离散模型、算法不变量与精确代数性质。数值稳定性、舍入误差和实现性能只有进入模型或定理后才属于 Lean 的检查范围。

计算机代数

MATLAB Symbolic Math Toolbox、Mathematica 和 SymPy 可以化简表达式、求积分或解方程。它们通常以算法结果为主要产物，用户信任实现或用其他方法复核结果。

Lean 的 tactic 可以调用计算和自动推理，但目标是构造可检查的证明项。例如 ring 把多项式等式归一化，并生成内核可验证的证明。若外部工具只返回答案，Lean 还需要证书、重放步骤或单独证明，才能把答案作为定理接受。

实际使用时，可以先用计算机代数系统探索结果，再把需要长期维护的结论及其前提写入 Lean。若外部计算能够输出证书，也可以在 Lean 中检查证书，而不必重做全部搜索。

测试与证明

测试检查选定输入上的行为，证明处理命题中量化的全部情况。性能、IO、随机性和外部系统集成仍然主要依靠测试；纯函数性质和结构不变量适合写成定理。即使定理已经证明，模型与外部实现之间仍需测试或代码审查连接。

学习资料

不必读完类型理论再开始写 Lean。先熟悉函数、归纳类型、模式匹配和递归，再补隐式参数、类型类、elaboration 与 IO。开始写证明以后，要尽早分清定义相等、等式改写和自动化决策过程；否则很容易把所有失败都归结为 tactic 不够强。

我更习惯保留一个小型实验文件，用 #check、#print 和编辑器悬停核对类型。等一个现象能够稳定复现，再到参考手册中查对应规则，比从头通读手册有效。

  • Lean 文档入口：官方整理的安装、教程、参考手册和学习资源。
  • Lean Language Reference：语言的详细参考手册，适合查询语法、命令、编译与运行时行为，不是入门教程。
  • Functional Programming in Lean：面向程序员的官方教材，从函数式编程、类型类、Monad、IO 讲到依赖类型。
  • Theorem Proving in Lean 4：介绍依赖类型理论、命题与证明、归纳、结构、类型类和 tactic。
  • Mathematics in Lean：以 mathlib 为基础的数学形式化教材，本系列 mathlib 部分的主要参考之一。
  • mathlib4 API 文档：按声明和模块查询 mathlib 定义、定理与实例。
  • Lean 4 源码 与 mathlib4 源码：遇到文档未覆盖的行为时，可以直接查看实现、测试和变更记录。
  • Natural Number Game：通过交互关卡练习基本证明。
  • Lean Zulip：Lean 与 mathlib 社区的主要讨论区，搜索报错和 API 用法时很有帮助。

几份教材的侧重点不同：Functional Programming in Lean 以语言和程序设计为主，Theorem Proving in Lean 4 讲解证明项与逻辑基础，Mathematics in Lean 侧重使用 mathlib 形式化数学。语言参考手册适合按主题查询具体规则。