形式化数值分析：用 Lean 4 与智能代理构建可靠数值计算基石

1. 从“差不多就行”到“绝对精确”：为什么我们需要形式化数值分析？

在数值计算的世界里，我们早已习惯了“近似”和“误差”。无论是用牛顿法求解方程的根，还是用龙格-库塔法模拟物理系统，我们得到的永远是一个带有舍入误差的数值解。我们依赖教科书上的收敛性证明，相信只要步长足够小、迭代次数足够多，结果就会“足够接近”真实值。但“足够接近”是多近？证明中的假设条件在浮点运算的现实中是否依然成立？一个微小的舍入误差是否会在迭代中被无限放大？这些问题，在传统的数值分析教学和工程实践中，常常被一个模糊的“数值实验验证”所掩盖。

直到你遇到一个真正棘手的问题：一个复杂的偏微分方程求解器，在某个特定参数下，结果突然变得荒谬；或者一个看似收敛的优化算法，在换了硬件或编译器后，给出了截然不同的答案。这时你才会意识到，我们对于数值算法“正确性”的信心，很大程度上建立在沙土之上。这正是“形式化数值分析”要解决的核心问题：将数值算法的数学理论，用计算机能够严格检查的逻辑语言重新表述和证明，确保从前提条件到最终结论的每一步都无懈可击。

最近，随着交互式定理证明器Lean 4及其庞大的数学库mathlib生态的成熟，这个曾经只存在于理论计算机科学实验室里的想法，正迅速变得触手可及。Lean 4 不仅仅是一个编程语言，它更是一个“证明助理”。你可以在其中定义数学对象（如实数、矩阵、函数），陈述定理（如“牛顿法在满足 Lipschitz 条件下局部二次收敛”），并一步步地构造出机器可验证的证明。mathlib 则包含了从基础算术到高等数学的巨量已形式化的知识，为形式化数值分析提供了坚实的地基。

然而，将一整本数值分析教材形式化，是一个浩如烟海的工程。手动完成所有证明，即使对于专家也耗时费力。于是，一个更激动人心的方向出现了：构建智能代理（Agent）流水线，让机器辅助甚至主导部分形式化工作。这不仅仅是“自动证明”，而是构建一个系统，能够理解自然语言描述的数学命题，将其转化为形式化猜想，搜索已有的数学知识库（mathlib），尝试组合出证明，并对生成的形式化代码进行质量审计。这超越了传统“内核接受”的范畴——内核只保证证明逻辑无矛盾，而质量审计则要确保代码的可读性、可维护性、与数学直觉的一致性，以及在整个知识体系中的优雅整合。

本文就将围绕这个前沿命题展开。我会结合 Lean 4/mathlib 的最新生态（包括安装工具elan和构建工具lake），探讨如何构建这样一个面向数值分析领域的智能形式化流水线。我们将超越“玩具示例”，深入其核心架构、面临的挑战以及我实践中摸索出的“避坑指南”。无论你是数值计算工程师、数学研究者，还是对形式化方法感兴趣的程序员，这篇文章都将为你展示一条通往更可靠数值计算的切实路径。

2. 基石搭建：Lean 4、mathlib 与数值分析形式化的起点

在构想任何自动化流水线之前，我们必须先站稳脚跟，理解手动形式化一个数值算法是怎样的过程，以及现有的工具链能提供什么。这就像你要训练一个AI来写诗，自己总得先精通格律。

2.1 Lean 4 与 mathlib 生态初探

首先，你需要一个可工作的环境。我强烈建议使用elan来管理 Lean 版本，用lake来管理项目依赖。这能避免无数版本冲突的噩梦。

# 安装 elan（Lean 版本管理器） curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh # 创建一个新项目 lake new my_numerics_project cd my_numerics_project # 在 lakefile.lean 中添加 mathlib 依赖 # 然后构建项目 lake build

现在，假设我们要形式化一个最简单的算法：计算平方根的巴比伦方法（即牛顿法特例）。在MyNumericsProject/目录下创建一个新文件Babylonian.lean。我们的目标是形式化以下命题：“对于任意正实数a和初始猜测x0 > 0，由迭代x_{n+1} = (x_n + a / x_n) / 2定义的序列收敛到sqrt(a)，并且是二次收敛的。”

在 mathlib 中，实数、极限、收敛性都已有了完善的定义。我们首先引入必要的库：

import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.Calculus.MeanValue import Mathlib.Topology.Instances.Real

然后，我们开始定义迭代函数和序列：

noncomputable section variable (a : ℝ) (ha : a > 0) (x0 : ℝ) (hx0 : x0 > 0) /-- 巴比伦方法（牛顿法求平方根）的迭代函数。 -/ def babylonian_iter (x : ℝ) : ℝ := (x + a / x) / 2 /-- 由初始值 `x0` 生成的迭代序列。 -/ def babylonian_seq : ℕ → ℝ := λ n => Nat.recOn n x0 (λ _ x_prev => babylonian_iter a x_prev)

这里已经遇到了第一个形式化与编程的思维差异：在 Lean 中，我们需要明确区分“可计算”和“不可计算”的定义。因为我们的序列涉及除法（实数除法不是对所有输入都终止的算法），所以需要用noncomputable section声明。def关键字在这里更像是数学中的“定义”，而非编程中的“函数实现”。

2.2 证明收敛性：与“直觉证明”的搏斗

接下来是重头戏：证明序列单调递减且有下界（从而收敛），且极限满足x^2 = a。在纸笔证明中，我们可能会这样写：

1. 由 AM-GM 不等式，x_{n+1} = (x_n + a/x_n)/2 ≥ sqrt(a)，所以序列有下界sqrt(a)。
2. 计算x_{n+1} - sqrt(a)与x_n - sqrt(a)的关系，证明其平方后快速减小。

但在 Lean 中，每一步都需要引用已有的定理或进行严格的推导。例如，证明有下界：

theorem babylonian_seq_ge_sqrt (n : ℕ) : Real.sqrt a ≤ babylonian_seq a x0 n := by induction' n with k IH · -- 基础情况 n=0，需证明 sqrt(a) ≤ x0。这不一定成立！我们的前提只有 x0 > 0。 -- 啊哈，第一个“坑”！纸笔证明中我们常默认 x0 是任意正数，但这里“有下界”的结论实际上要求 x0 ≥ sqrt(a) 时才成立。 -- 我们需要修正前提条件，或者分情况讨论。这揭示了形式化如何迫使你澄清模糊的假设。 rcases em' (x0 ≥ Real.sqrt a) with (h | h) · exact h · -- 如果 x0 < sqrt(a)，那么第一次迭代后 x1 就会大于 sqrt(a) have h1 : babylonian_iter a x0 ≥ Real.sqrt a := by apply (le_div_iff ?_).mp ?_ -- 这里开始应用 AM-GM 不等式 -- ... 详细的证明步骤省略，可能需要10-20行 exact h1 · -- 归纳步骤，利用迭代函数的性质 dsimp [babylonian_seq] have : babylonian_iter a (babylonian_seq a x0 k) ≥ Real.sqrt a := by apply babylonian_iter_ge_sqrt a ha -- 这需要我们先证明关于迭代函数的引理 exact this

这个过程极其繁琐，但意义重大。它暴露了教科书证明中经常省略的细节：初始值的条件。许多数值分析定理都带有“当初始猜测足够接近真解时”的前提，形式化要求你必须精确量化这个“足够接近”。

2.3 形式化数值分析的独特挑战

从这个小例子，我们可以总结出手动形式化数值分析的几个核心挑战，这些也正是自动化流水线需要攻克的难关：

1. 实数与浮点数的鸿沟：mathlib 中的ℝ是完美的数学实数。但实际计算是在浮点数Float或Double中进行的。形式化数值分析最终需要搭建一座桥梁，证明在考虑舍入误差的浮点运算下，算法依然满足某种精度要求。这需要导入 IEEE 754 标准的形式化模型，工作量巨大。
2. 算法终止性与复杂性：牛顿法可能不收敛（例如初始值选得不好）。形式化中，我们通常先证明“如果收敛，则极限是根”，再在附加条件（如凸性）下证明收敛。对于自动化代理来说，它需要能识别这些不同的证明目标和所需的前提条件。
3. 大量不等式演算：数值分析的本质是“逼近”，证明中充斥着ε-δ语言和各种不等式（柯西-施瓦茨、Holder、三角不等式等）。自动化工具需要强大的不等式自动证明或化简能力。

尽管艰难，但每完成一个定理的形式化，它就变成了 mathlib 中一块永久的、可被百分百信赖的砖石。接下来，我们将探讨如何用智能代理来加速这块砖石的烧制过程。

3. 智能代理流水线蓝图：超越“证明搜索”的自动化

当我们谈论“自动形式化”时，最简单的想法是：给机器一个自然语言命题，它直接输出 Lean 代码。这目前还属于科幻范畴。更现实的路径是构建一个多智能体协作的流水线，将大问题分解为多个可处理的子任务。下图展示了一个我设想中的管道架构：

自然语言描述/教科书片段 ↓ [理解与解析代理] ↓ 生成形式化猜想草图 (含占位符) ↓ [策略规划代理] ↓ 生成战术脚本蓝图 (Tactic Sketch) ↓ [证明搜索与填充代理] ↓ 调用外部证明器 (如 `linarith`, `nlinarith`, `ring`)、检索 mathlib ↓ [代码生成与合成代理] ↓ 输出初步的 Lean 证明代码 ↓ ↓←←←←←←←←←←←←←←←←←←←← ↓ ↑ [质量审计与重构代理] ↑ ↓ (风格检查、引理命名、结构优化) ↑ ↓ ↑ →→→→→→→→→→→→→→→→→→→→→→↑ (迭代修正) ↓ 可提交至 mathlib 的高质量代码

这个流水线的核心思想是分工与迭代。每个代理负责一个专业领域，并且后置的审计代理会对前置的输出进行批评和修正，形成一个闭环。

3.1 代理一：理解与解析——从自然语言到形式化草图

这个代理的任务是最难的。它需要理解“序列{x_n}二次收敛到L”这样的语句。目前，基于大语言模型（LLM）的方法是主流。我们可以用大量(自然语言陈述，形式化陈述)的对子来微调一个模型。

例如，训练数据可能包含：

• 输入：“函数 f 在点 c 可微。”
• 输出：DifferentiableAt ℝ f c

对于数值分析，我们需要注入专业术语：

• 输入：“迭代格式x_{k+1} = x_k - f(x_k)/f'(x_k)。”
• 输出：def newton_iter (f f' : ℝ → ℝ) (x : ℝ) : ℝ := x - f x / f' x

这个代理的输出不应是完整的、正确的代码，而是一个带有占位符和待证明子目标的草图。例如，对于“牛顿法二次收敛”，它可能输出：

theorem newton_quadratic_convergence (f f' : ℝ → ℝ) (c : ℝ) (hf : HasDerivAt f (f' c) c) (hf' : f' c ≠ 0) : ∃ (δ : ℝ) (hδ : δ > 0) (K : ℝ) (hK : K > 0), ∀ (x : ℝ), |x - c| < δ → let x_next := newton_iter f f' x in |x_next - c| ≤ K * |x - c| ^ 2 := by -- 这里需要证明存在这样的 δ 和 K -- 提示：使用泰勒公式展开 f 在 c 点附近 sorry

输出中的sorry就是占位符，标记了需要后续代理填补的证明缺口。同时，注释给出了证明策略的提示，这可以来自训练数据中人工提供的证明思路。

3.2 代理二：策略规划与证明搜索——填补sorry缺口

这个代理接收带有sorry的草图。它的核心是一个强化学习环境。状态（State）是当前的证明目标（Goal），动作（Action）是可能应用的 Lean 战术（Tactic），如intro h,apply TheoremName,use 0.5,linarith等。

代理的目标是找到一系列战术，将当前目标分解为已知公理或已证明引理。它需要访问两个关键资源：

1. mathlib 检索系统：一个向量数据库，存储了所有 mathlib 定理的名称、类型和文档字符串。给定当前目标⊢ |x_next - c| ≤ K * |x - c| ^ 2，代理应能检索到相关的定理，如abs_mul,abs_pow,Real.taylor_theorem等。
2. 外部证明器：Lean 本身内置了一些决策过程，如linarith（线性算术）、nlinarith（非线性算术）、ring（环运算）。代理可以调用它们来自动关闭一些简单的代数不等式子目标。

这个代理的训练是极其耗资源的，需要在海量的、随机生成的数学命题及其证明上进行训练。OpenAI 的GPT-f和 Google 的DeepMind在 Isabelle 和 Lean 上做过类似探索。一个实用的技巧是分层规划：先让代理用“大纲模式”规划证明步骤（例如：1. 应用泰勒定理；2. 将高阶项表示为余项；3. 估计余项的界），然后再用具体的战术去填充每一步。

3.3 代理三：代码生成与质量审计——从“正确”到“优美”

即使前两个代理合作产出了一个能通过 Lean 内核检查的证明，这段代码也可能是一团糟：变量命名随意、证明步骤冗长重复、没有使用 mathlib 中现成的组合型定理（如calc块或field_simp）。这就是质量审计代理的用武之地。

这个代理更像一个形式化代码的静态分析器与重构引擎。它的检查清单包括：

1. 风格一致性：变量名是否遵循 mathlib 惯例（如h表示假设，hx表示关于x的假设）？定理名是否清晰描述了其内容（newton_quadratic_convergence就比theorem_1好）？
2. 证明结构化：是否可以将一长串rewrite和apply替换为一个清晰的calc块？是否可以将某个通用子证明提取为独立的lemma，以提高可复用性？
3. 性能与可读性：是否使用了simp过度导致性能下降？是否存在可以合并的重复子目标？
4. 数学正确性：虽然内核接受了，但证明逻辑是否与数学家的直觉一致？是否存在更优雅、更直接的证法？例如，证明二次收敛时，是否清晰地分离了“存在收敛域”和“在域内估计误差”这两个逻辑部分？

审计代理可以基于规则，也可以基于学习。例如，它可以被训练来区分“专家编写的证明”和“新手或机器生成的证明”，然后尝试将后者向前者的风格转换。它还可以调用一个“证明压缩”算法，尝试寻找更短的等效证明。

注意：质量审计是当前研究的前沿，也是区分“能用的原型”和“实用的工具”的关键。一个只会生成冗长、晦涩代码的自动化系统，不会被数学社区所接受。

4. 实战演练：构建一个简易的“收敛性证明”辅助代理

理论说再多，不如动手试。我们不可能在本文内实现完整的流水线，但可以构建一个极度简化的、针对特定模式（“证明序列单调有界故收敛”）的辅助代理。这个代理将结合规则引擎和 LLM 的提示工程。

场景：我们已经手动形式化了序列{x_n}的定义，并证明了它单调递减且有下界。现在需要写出最终的收敛性证明。在 mathlib 中，这对应定理Monotone.isLUB_of_tendsto或tendsto_of_monotone_and_bounded。新手可能会找不到这个定理。

我们的简易代理工作流：

1. 用户输入：当前证明目标为⊢ ∃ L, Tendsto babylonian_seq atTop (𝓝 L)，并且我们有已知假设h_mono : Monotone babylonian_seq和h_bdd : BddBelow (Set.range babylonian_seq)。
2. 规则匹配：代理内部有一个规则库，将目标模式(∃ L, Tendsto ... atTop (𝓝 L))与已知假设模式(Monotone ...)、(BddBelow ...)进行匹配。
3. 定理检索：匹配成功后，代理从预加载的 mathlib 定理索引中，搜索同时包含关键词Monotone、BddBelow、Tendsto的定理。它会找到Monotone.isLUB_of_tendsto。
4. 代码生成与提示：代理不会直接写出完整代码，而是生成一个高度提示性的代码块给用户：

-- 智能代理提示：根据您已证明的单调性和有界性，可以考虑使用以下定理： -- `Monotone.isLUB_of_tendsto` : 若函数单调且在区间上有界，则其极限等于上确界/下确界。 -- 您的目标是证明极限存在。一个典型的证明结构如下： theorem babylonian_seq_converges : ∃ L, Tendsto (babylonian_seq a x0) atTop (𝓝 L) := by have h_lub : ∃ L, IsLUB (Set.range (babylonian_seq a x0)) L := by apply h_bdd.isLUB_of_monotone? -- 这里需要找到一个连接‘BddBelow’和‘IsLUB’的引理，可能是 `bdd_below.is_lub_of_monotone`？请检查 mathlib。 exact h_mono rcases h_lub with ⟨L, hL⟩ use L -- 现在需要从 `IsLUB ... L` 和单调性推出 `Tendsto ... (𝓝 L)` -- 定理 `Monotone.tendsto_atTop_isLUB` 可能正是您需要的。 exact h_mono.tendsto_atTop_isLUB hL

注意，代理在注释中使用了问号和“请检查 mathlib”的表述。这是因为 mathlib 的 API 可能会变动，规则库可能不完全准确。它扮演的是一个“超级智能的代码补全和文档提示”角色，而非全自动证明器。

这个简易代理可以通过扩展规则库来覆盖更多模式，例如“柯西序列收敛”、“压缩映射原理”等。虽然简单，但它已经能显著减少开发者在庞大的 mathlib API 中搜寻的时间。

5. 质量审计的深层挑战：当“正确”不等于“好”

让我们回到文章标题中的“Quality Audit Beyond Kernel Acceptance”。内核接受只意味着逻辑无误，但距离一篇优秀的、可融入 mathlib 的形式化作品，还差得很远。以下是我在尝试贡献代码时，从社区评审中学到的几条“血泪教训”，也是自动化审计需要学习的标准：

5.1 命名与可发现性

一个糟糕的定理名就像一本没有索引的书。假设你证明了“牛顿法在单根附近局部二次收敛”。

• 差命名：theorem newton_convergence_1 (f : ℝ → ℝ) ...
• 好命名：theorem has_deriv_at.newton_iterate_quadratic_convergence。 为什么好？它使用了“点标记”命名法。在 Lean 中，如果你有假设h : HasDerivAt f f' c，你可以直接写h.newton_iterate_quadratic_convergence来调用这个定理，上下文非常清晰。审计代理需要学习这种命名约定。

5.2 证明的结构与“洞见”的保留

机器生成的证明往往是“暴力”的：它可能通过大量繁琐的代数变形，绕了一个大圈子最终证出结论。而数学家的证明通常有清晰的“洞见”（insight），比如“这里的关键是注意到这个表达式可以配方”。例如，证明x_{n+1} - sqrt(a) = (x_n - sqrt(a))^2 / (2*x_n)。

机器可能生成的冗长证明：

have H : babylonian_iter a x - Real.sqrt a = (x - Real.sqrt a)^2 / (2 * x) := by field_simp [babylonian_iter] ring -- ... 一大堆 ring_nf, ring_exp 的操作

人工优化后的证明：

have H : babylonian_iter a x - √a = (x - √a)^2 / (2*x) := by dsimp [babylonian_iter] field_simp (hx : x ≠ 0) ring

区别在于，人工证明通过field_simp (hx : x ≠ 0)明确给出了分母不为零的条件，并且ring一步就完成了化简，更简洁也更具可读性。审计代理需要能识别这种可以简化的“证明噪声”。

5.3 泛化性与特化性的平衡

你是该证明一个关于ℝ上牛顿法的通用定理，还是先证明normed_field上的？过度泛化（过度抽象）会增加证明的复杂度和理解难度，而过度特化则限制了定理的复用价值。例如，平方根迭代的证明，其核心思想依赖于a / x这个操作，这在一般的域中可能没有定义。所以，从ℝ或ℝ≥0开始是合理的。审计代理需要判断当前定理的抽象层次是否与 mathlib 中相邻定理保持一致。

5.4 文档字符串（Docstring）的撰写

一个没有文档的定理是难以使用的。好的文档字符串不仅陈述定理内容，还给出典型用例。审计代理可以检查文档字符串是否：

• 用自然语言复述了形式化陈述。
• 给出了至少一个简单的#example用法。
• 提到了重要的前提条件（如“初始值需足够接近根”）。
• 引用了相关的定理。

自动化生成高质量的文档字符串本身就是一个 NLP 任务，可以基于定理的类型和证明上下文来生成。

6. 展望与现实的鸿沟：当前局限与可行路径

构建一个全自动、高质量的形式化数值分析代理流水线，是 AI for Math 的终极梦想之一，但我们离它还很远。当前的局限是明显的：

1. 数学理解的深度：现有的 LLM 对深层次数学结构的理解仍然肤浅，它们擅长模仿模式，但缺乏真正的数学推理和“灵光一现”的能力。
2. 数据稀缺：高质量的(自然语言数学，形式化代码)配对数据极少。mathlib 本身是一个宝库，但需要大量的人工标注才能将其中的证明步骤与高层次的数学思想关联起来。
3. 计算成本：强化学习训练证明搜索代理需要与环境（Lean 内核）进行数百万次的交互，每次交互都涉及类型检查，成本高昂。

那么，在现阶段，什么是可行的路径？我认为是“人机协同，增量推进”：

• 第一步：打造强大的“副驾驶”。就像我们之前构建的简易代理，开发能深度理解 mathlib API、能根据当前证明上下文提供精准定理建议、能自动完成繁琐代数运算的 IDE 插件。这能极大提升专业形式化验证者的效率。
• 第二步：分模块攻克数值分析核心库。集中社区力量，优先形式化数值线性代数的基础（矩阵范数、条件数、LU分解的稳定性分析），因为这部分理论相对规整，且应用极其广泛。然后向常微分方程数值解、数值优化推进。
• 第三步：建立“半自动化”的贡献流水线。贡献者用自然语言描述定理和证明思路，由 AI 生成初步的形式化草图和证明骨架，贡献者进行修正、优化和最终的质量把关，然后提交至 mathlib。这个过程本身就能产生宝贵的训练数据。

这条路注定漫长，但每前进一小步，都意味着我们向“完全可靠的数值计算”迈近了一点点。当有一天，我们运行一个数值模拟程序时，不仅能得到结果，还能附上一份由机器生成并验证的、关于该结果在给定精度下可靠性的形式化证书，那将是计算科学的一个革命性时刻。

对我个人而言，在 Lean 中形式化哪怕一个简单的数值算法，也是一次思维的淬炼。它强迫你直面每一个曾经忽略的细节，让你对“收敛”、“稳定”、“误差”这些概念的理解达到前所未有的精确度。这种体验，或许比自动化本身更有价值。它让你从一个算法的“使用者”，真正变成一个“理解者”和“创造者”。