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来管理项目依赖。这能避免无数版本冲突的噩梦。# 安装 elanLean 版本管理器 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_{n1} (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。在纸笔证明中我们可能会这样写由 AM-GM 不等式x_{n1} (x_n a/x_n)/2 ≥ sqrt(a)所以序列有下界sqrt(a)。计算x_{n1} - 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 · -- 基础情况 n0需证明 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 形式化数值分析的独特挑战从这个小例子我们可以总结出手动形式化数值分析的几个核心挑战这些也正是自动化流水线需要攻克的难关实数与浮点数的鸿沟mathlib 中的ℝ是完美的数学实数。但实际计算是在浮点数Float或Double中进行的。形式化数值分析最终需要搭建一座桥梁证明在考虑舍入误差的浮点运算下算法依然满足某种精度要求。这需要导入 IEEE 754 标准的形式化模型工作量巨大。算法终止性与复杂性牛顿法可能不收敛例如初始值选得不好。形式化中我们通常先证明“如果收敛则极限是根”再在附加条件如凸性下证明收敛。对于自动化代理来说它需要能识别这些不同的证明目标和所需的前提条件。大量不等式演算数值分析的本质是“逼近”证明中充斥着ε-δ语言和各种不等式柯西-施瓦茨、Holder、三角不等式等。自动化工具需要强大的不等式自动证明或化简能力。尽管艰难但每完成一个定理的形式化它就变成了 mathlib 中一块永久的、可被百分百信赖的砖石。接下来我们将探讨如何用智能代理来加速这块砖石的烧制过程。3. 智能代理流水线蓝图超越“证明搜索”的自动化当我们谈论“自动形式化”时最简单的想法是给机器一个自然语言命题它直接输出 Lean 代码。这目前还属于科幻范畴。更现实的路径是构建一个多智能体协作的流水线将大问题分解为多个可处理的子任务。下图展示了一个我设想中的管道架构自然语言描述/教科书片段 ↓ [理解与解析代理] ↓ 生成形式化猜想草图 (含占位符) ↓ [策略规划代理] ↓ 生成战术脚本蓝图 (Tactic Sketch) ↓ [证明搜索与填充代理] ↓ 调用外部证明器 (如 linarith, nlinarith, ring)、检索 mathlib ↓ [代码生成与合成代理] ↓ 输出初步的 Lean 证明代码 ↓ ↓←←←←←←←←←←←←←←←←←←←← ↓ ↑ [质量审计与重构代理] ↑ ↓ (风格检查、引理命名、结构优化) ↑ ↓ ↑ →→→→→→→→→→→→→→→→→→→→→→↑ (迭代修正) ↓ 可提交至 mathlib 的高质量代码这个流水线的核心思想是分工与迭代。每个代理负责一个专业领域并且后置的审计代理会对前置的输出进行批评和修正形成一个闭环。3.1 代理一理解与解析——从自然语言到形式化草图这个代理的任务是最难的。它需要理解“序列{x_n}二次收敛到L”这样的语句。目前基于大语言模型LLM的方法是主流。我们可以用大量(自然语言陈述形式化陈述)的对子来微调一个模型。例如训练数据可能包含输入“函数 f 在点 c 可微。”输出DifferentiableAt ℝ f c对于数值分析我们需要注入专业术语输入“迭代格式x_{k1} 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等。代理的目标是找到一系列战术将当前目标分解为已知公理或已证明引理。它需要访问两个关键资源mathlib 检索系统一个向量数据库存储了所有 mathlib 定理的名称、类型和文档字符串。给定当前目标⊢ |x_next - c| ≤ K * |x - c| ^ 2代理应能检索到相关的定理如abs_mul,abs_pow,Real.taylor_theorem等。外部证明器Lean 本身内置了一些决策过程如linarith线性算术、nlinarith非线性算术、ring环运算。代理可以调用它们来自动关闭一些简单的代数不等式子目标。这个代理的训练是极其耗资源的需要在海量的、随机生成的数学命题及其证明上进行训练。OpenAI 的GPT-f和 Google 的DeepMind在 Isabelle 和 Lean 上做过类似探索。一个实用的技巧是分层规划先让代理用“大纲模式”规划证明步骤例如1. 应用泰勒定理2. 将高阶项表示为余项3. 估计余项的界然后再用具体的战术去填充每一步。3.3 代理三代码生成与质量审计——从“正确”到“优美”即使前两个代理合作产出了一个能通过 Lean 内核检查的证明这段代码也可能是一团糟变量命名随意、证明步骤冗长重复、没有使用 mathlib 中现成的组合型定理如calc块或field_simp。这就是质量审计代理的用武之地。这个代理更像一个形式化代码的静态分析器与重构引擎。它的检查清单包括风格一致性变量名是否遵循 mathlib 惯例如h表示假设hx表示关于x的假设定理名是否清晰描述了其内容newton_quadratic_convergence就比theorem_1好证明结构化是否可以将一长串rewrite和apply替换为一个清晰的calc块是否可以将某个通用子证明提取为独立的lemma以提高可复用性性能与可读性是否使用了simp过度导致性能下降是否存在可以合并的重复子目标数学正确性虽然内核接受了但证明逻辑是否与数学家的直觉一致是否存在更优雅、更直接的证法例如证明二次收敛时是否清晰地分离了“存在收敛域”和“在域内估计误差”这两个逻辑部分审计代理可以基于规则也可以基于学习。例如它可以被训练来区分“专家编写的证明”和“新手或机器生成的证明”然后尝试将后者向前者的风格转换。它还可以调用一个“证明压缩”算法尝试寻找更短的等效证明。注意质量审计是当前研究的前沿也是区分“能用的原型”和“实用的工具”的关键。一个只会生成冗长、晦涩代码的自动化系统不会被数学社区所接受。4. 实战演练构建一个简易的“收敛性证明”辅助代理理论说再多不如动手试。我们不可能在本文内实现完整的流水线但可以构建一个极度简化的、针对特定模式“证明序列单调有界故收敛”的辅助代理。这个代理将结合规则引擎和 LLM 的提示工程。场景我们已经手动形式化了序列{x_n}的定义并证明了它单调递减且有下界。现在需要写出最终的收敛性证明。在 mathlib 中这对应定理Monotone.isLUB_of_tendsto或tendsto_of_monotone_and_bounded。新手可能会找不到这个定理。我们的简易代理工作流用户输入当前证明目标为⊢ ∃ L, Tendsto babylonian_seq atTop ( L)并且我们有已知假设h_mono : Monotone babylonian_seq和h_bdd : BddBelow (Set.range babylonian_seq)。规则匹配代理内部有一个规则库将目标模式(∃ L, Tendsto ... atTop ( L))与已知假设模式(Monotone ...)、(BddBelow ...)进行匹配。定理检索匹配成功后代理从预加载的 mathlib 定理索引中搜索同时包含关键词Monotone、BddBelow、Tendsto的定理。它会找到Monotone.isLUB_of_tendsto。代码生成与提示代理不会直接写出完整代码而是生成一个高度提示性的代码块给用户-- 智能代理提示根据您已证明的单调性和有界性可以考虑使用以下定理 -- 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_{n1} - 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 的终极梦想之一但我们离它还很远。当前的局限是明显的数学理解的深度现有的 LLM 对深层次数学结构的理解仍然肤浅它们擅长模仿模式但缺乏真正的数学推理和“灵光一现”的能力。数据稀缺高质量的(自然语言数学形式化代码)配对数据极少。mathlib 本身是一个宝库但需要大量的人工标注才能将其中的证明步骤与高层次的数学思想关联起来。计算成本强化学习训练证明搜索代理需要与环境Lean 内核进行数百万次的交互每次交互都涉及类型检查成本高昂。那么在现阶段什么是可行的路径我认为是“人机协同增量推进”第一步打造强大的“副驾驶”。就像我们之前构建的简易代理开发能深度理解 mathlib API、能根据当前证明上下文提供精准定理建议、能自动完成繁琐代数运算的 IDE 插件。这能极大提升专业形式化验证者的效率。第二步分模块攻克数值分析核心库。集中社区力量优先形式化数值线性代数的基础矩阵范数、条件数、LU分解的稳定性分析因为这部分理论相对规整且应用极其广泛。然后向常微分方程数值解、数值优化推进。第三步建立“半自动化”的贡献流水线。贡献者用自然语言描述定理和证明思路由 AI 生成初步的形式化草图和证明骨架贡献者进行修正、优化和最终的质量把关然后提交至 mathlib。这个过程本身就能产生宝贵的训练数据。这条路注定漫长但每前进一小步都意味着我们向“完全可靠的数值计算”迈近了一点点。当有一天我们运行一个数值模拟程序时不仅能得到结果还能附上一份由机器生成并验证的、关于该结果在给定精度下可靠性的形式化证书那将是计算科学的一个革命性时刻。对我个人而言在 Lean 中形式化哪怕一个简单的数值算法也是一次思维的淬炼。它强迫你直面每一个曾经忽略的细节让你对“收敛”、“稳定”、“误差”这些概念的理解达到前所未有的精确度。这种体验或许比自动化本身更有价值。它让你从一个算法的“使用者”真正变成一个“理解者”和“创造者”。
