吴-里特特征列方法在Lean4中的形式化验证：从数学理论到可验证代码

1. 从数学理论到可验证代码：吴-里特特征列方法为何需要形式化？

在计算机代数、符号计算乃至现代数学证明辅助领域，吴-里特特征列方法是一个绕不开的经典算法。它由吴文俊先生提出，并由里特等人发展，核心目标是高效地将一个多项式方程组化简为一种特殊的三角列形式，从而为求解多项式方程组、几何定理机器证明等提供强有力的工具。简单来说，它就像是为一组复杂的、相互纠缠的方程进行“解耦”和“分层”，让你能像解一元一次方程那样，自底向上地逐个求解。

那么，为什么我们今天要在 Lean 4 这个定理证明器中，重新“实现”并“验证”这个已有成熟软件包（如Maple、Mathematica中的相关函数）的算法呢？这绝非重复造轮子。其核心价值在于“形式化验证”带来的绝对可信性。传统的软件实现，无论经过多少测试，理论上都存在隐藏Bug的可能性，尤其是在处理数学这种追求绝对严谨的领域。一个在百万次测试中运行良好的算法，可能在某个极其特殊的边界条件下给出错误结果，而这类错误在数学推导中可能是灾难性的。

在 Lean 4 中实现并验证吴方法，意味着我们不仅仅是在编写执行计算的代码，更是在同时构建一个该算法“完全正确”的数学证明。Lean 4 的类型系统允许我们将算法的规范（它应该做什么）和其实现（它具体怎么做）通过类型关联起来。当我们最终让代码通过 Lean 编译器检查时，我们实际上获得了一个机器检查过的证明：该程序的行为严格符合其数学定义。这对于需要极高可靠性的应用至关重要，例如在航天控制软件、加密协议验证或数学定理的自动化证明中，任何微小的计算偏差都可能导致完全不同的结论。

从网络热词中，我们可以看到大量关于“实现”的讨论，从哈希表底层到快速排序，从设计模式到具体业务功能。这反映了实践者对“知其然并知其所以然”的深度需求。对吴方法的 Lean 4 实现，正是这种需求的终极体现：我们不满足于仅仅调用一个WuMethodSolve的黑盒函数，我们要深入到算法的每一个逻辑分支、每一次多项式约化、每一个序的选择，并确保它们在所有数学可能的情况下都是正确的。这就像不仅要用 Java 实现一个HashMap，还要用形式化方法证明其get、put操作的时间复杂度边界和一致性语义。

2. 核心概念拆解：多项式、序与三角列

在深入 Lean 4 的实现细节之前，必须夯实几个基石性的概念。这是理解后续所有验证工作的前提。

2.1 多项式环与变元序

我们工作的舞台是多项式环，例如 ℚ[x₁, x₂, ..., xₙ] 或 ℤ[x₁, x₂, ..., xₙ]。吴方法处理的是多元多项式方程组。一个根本性的选择是“变元序”。我们必须为所有变元规定一个全序，比如 x₁ > x₂ > ... > xₙ。这个序至关重要，它决定了多项式“主变元”的选取，以及后续三角化过程的方向。常见的序有纯字典序和分次反字典序。在 Lean 4 中，我们需要用某种结构（比如一个List Variable或一个从Variable到Nat的索引映射）来严格定义这个序，并将其作为所有后续操作的前提条件。

2.2 伪除与约化

这是算法中最基础的操作。给定两个多项式f和g（其中g非零），关于某个主变元x，我们可以用g对f进行伪除，得到q和r，使得I * f = q * g + r。这里I是g关于x的初式的某个幂，r是关于x的次数低于g的多项式。r被称为f对g的“余式”或“伪余式”。这个过程反复执行，直到余式关于主变元的次数不能再降低。在 Lean 4 实现中，我们需要精确定义这个计算过程，并可能将其证明为一个返回“商-余式-乘子”三元组的函数，同时附带关于次数关系的证明项。

2.3 特征列与三角列

一组多项式集合CS如果满足：其中每个多项式的主变元都不同，且每个多项式对其前面所有多项式的余式均为零，那么CS就构成一个“三角列”。这是吴方法输出的理想形式。 而“特征列”是一种特殊的三角列，它是由某个多项式集合PS通过特定的算法（吴-里特算法）计算得到的，并且具有一些良好的性质，例如它是PS所生成理想的一个基，或者与PS有相同的零点集（在某种意义下）。特征列是“不可约”或“正则”的，这使得它比一般的三角列更强大。

在 Lean 4 的形式化中，我们不仅要定义TriangularSet和CharacteristicSet这两个结构体或类，更重要的是要定义它们的“规范”：即通过一系列命题（Prop）来刻画它们必须满足的条件。例如：

structure TriangularSet (vars : List Var) (R : Type _) [CommRing R] where polynomials : List (MvPolynomial vars R) mainVars : List Var -- 每个多项式的主变元列表 decreasing : ∀ i j, i < j → (mainVars[i] > mainVars[j] according to order) -- 主变元严格递减 reduced : ∀ i, ∀ j < i, remainder (polynomials[i]) (polynomials[j]) (mainVars[j]) = 0 -- 对前列余式为0

这只是一个概念示意，真实定义会更复杂，需要处理空列表、单多项式等情况，并妥善嵌入变元序。

3. 吴-里特算法流程的形式化描述

有了以上基础，我们可以勾勒出算法的主干。吴-里特算法是一个递归或迭代的过程，其输入是一个多项式集合PS，输出是一个特征列CS。以下是其核心步骤的形式化描述，也是我们在 Lean 4 中需要构造证明的路线图。

3.1 初始化与选择

首先，从输入集PS中选取一个“基点”。通常选取主变元最小（在序中最大）的多项式。如果存在常数（非零），则整个方程组无解（在代数闭域上），特征列可定义为{1}。这一步在 Lean 中需要处理集合的非空性和选择函数，可能用到Classical.choice或明确构造一个选取策略。

3.2 约化与添加

设当前已部分构造的三角列为B（初始可能为空），剩余多项式集合为R。算法核心循环如下：

1. 从R中取出一个多项式f。
2. 用当前的三角列B对f进行完全约化。即，依次用B中的每一个多项式（按其主变元从高到低的顺序）对f进行伪除，得到一个余式r。这个r关于B中所有多项式的主变元次数都是已约化的。
3. 如果r是零多项式，那么f是当前理想中已有的多项式，丢弃它。
4. 如果r是非零常数，同样表明方程组无解，算法可提前终止返回{1}。
5. 如果r非零非常数，则将r加入到三角列B中。这里的关键是，r的主变元必须小于B中现有所有多项式的主变元（根据约化过程，这自然满足），从而保持三角性。

3.3 更新与迭代

将r加入B后，原来B中的多项式可能需要用新的r重新约化，以保持“约化”的性质（即B中每个多项式对其前面多项式的余式为0）。这一步是算法复杂度的主要来源之一。更新后的B和移除f后的R进入下一轮循环。

3.4 终止性与正确性证明

算法的终止性基于每次添加新多项式r时，其主变元严格下降（相对于一个良基序），或者其次数在某种度量下减少。在 Lean 4 中，我们需要定义一个良基关系（Well-founded relation），并使用WellFounded.fix或类似的递归构造来定义这个算法，让 Lean 的类型检查器接受这是一个总会终止的计算。

正确性证明则更为深刻，需要证明最终得到的三角列CS满足：

• 零点关系：ZeroSet(CS) ⊆ ZeroSet(PS)，并且ZeroSet(PS) ⊆ ZeroSet(CS) ∪ ZeroSet(Initials(CS))，其中Initials(CS)是CS中多项式的初式集合。这就是著名的“零点分解定理”。
• 特征性：CS是PS所生成理想的一个特征基。

在 Lean 中，这些证明将体现为一系列定理（theorem）的陈述和证明。例如：

theorem zero_set_subset (ps : Set (MvPolynomial vars ℚ)) (cs : CharacteristicSet ps) : ZeroSet cs ⊆ ZeroSet ps := by -- 证明过程：需要利用算法构造过程和伪除的性质，展示 cs 中的多项式都是由 ps 中的多项式通过伪除和组合得到的。 ...

4. Lean 4 实现中的具体构造与难点

将上述数学描述转化为 Lean 4 代码，会遇到许多具体挑战。这不仅仅是编程，更是“让数学定义可计算化”和“为计算过程提供证明”。

4.1 数据结构的选择

首先是如何表示多项式。Mathlib4 提供了强大的MvPolynomial类型。我们需要基于此进行工作。对于多项式集合，使用List还是Set或Finset？List可以保持顺序，这对于三角列至关重要（多项式顺序对应变元顺序）。Finset则便于去重和集合运算。一个常见的策略是内部核心算法使用List以保证顺序，对外接口可以接受Finset并转化为List进行处理。

对于三角列，我们可以定义一个结构体：

structure TriangularSet (ord : VarOrder) where polys : List (MvPolynomial vars R) main_vars : List Var property : TriangularProperty ord polys main_vars

其中TriangularProperty是一个命题，封装了主变元递减和相互约化的条件。

4.2 伪除算法的实现与验证

这是最基础的砖石。我们需要实现一个函数pseudoRemainder (f g : MvPolynomial vars R) (x : Var) : MvPolynomial vars R，并证明其核心性质：

theorem pseudo_remainder_spec (f g : MvPolynomial vars R) (hx : x ∈ vars) (hg : g ≠ 0) : ∃ (k : ℕ) (q : MvPolynomial vars R), (leadingCoeff g x)^k • f = q * g + pseudoRemainder f g x ∧ degree (pseudoRemainder f g x) x < degree g x ∨ pseudoRemainder f g x = 0 := by ...

这里用到了∃和∧，说明这个函数计算的结果需要附带一个“证明包”，或者我们后续用一个独立的定理来陈述这个性质。在函数式编程和类型论中，我们更倾向于实现一个返回“余式r和证明项proof”的依赖对（Sigma 类型）的函数。

4.3 递归构造与终止性证明

吴-里特算法本质上是递归的。在 Lean 4 中，定义递归函数必须向编译器证明其终止性。我们可以定义一个度量函数measure : List Polynomial × List Polynomial → Nat，例如基于所有多项式主变元序的字典序，或者所有多项式的全次数和。然后使用termination_by指令来指定这个度量，并证明在每次递归调用时该度量是递减的。

partial def wu_algorithm (bas : List Polynomial) (rem : List Polynomial) : List Polynomial := match rem with | [] => bas | f :: rest => let r := full_reduce f bas match r with | 0 => wu_algorithm bas rest -- 丢弃 f | 1 => [1] -- 无解，提前返回 | _ => let new_bas := update_triangular bas r wu_algorithm new_bas rest end termination_by wu_algorithm bas rem => (measure bas rem)

update_triangular函数内部可能又包含循环，也需要单独的终止性证明。这是工程中最繁琐的部分之一，需要仔细设计度量。

4.4 效率与可行性考量

形式化验证并不追求运行时效率，而是逻辑正确性。因此，我们的初始实现可能非常直接且低效，比如使用列表的简单遍历和复制。这完全是可以接受的。首要目标是让定义和定理通过类型检查。在确保正确性之后，如果考虑实际计算，我们可以进行优化，并用“可计算性”而非“效率”来证明优化后的版本与规范版本等价。Mathlib4 中许多算法（如Nat.gcd）都有慢速（清晰）和快速（高效）两个版本，并通过定理关联它们。

5. 与现有数学库（Mathlib4）的集成与挑战

我们并非从零开始。Mathlib4 是一个庞大的、正在快速发展的形式化数学库。实现吴方法需要与其多个部分交互。

5.1 多项式代数模块

Mathlib.RingTheory.MvPolynomial是我们工作的核心。我们需要熟悉其 API：如何获取变元、获取/设置度、获取首项系数、进行多项式加减乘运算等。一个潜在的挑战是，Mathlib4 的多项式可能是抽象的、在无穷多变元上的，而吴方法通常处理有限、明确命名的变元集。我们需要处理好变元集的限定和索引。

5.2 序与良基关系

变元序的实现可以依赖Mathlib.Order中的类型类。我们需要定义VarOrder并证明它是一个LinearOrder或TotalOrder。对于良基递归，Mathlib.Logic.Function.Iterates和WellFounded相关的定理是必不可少的工具。

5.3 代数几何基础概念

为了陈述和证明零点定理，我们需要连接到Mathlib.AlgebraicGeometry的基础部分，特别是仿射簇ZeroSet的定义。这可能是最前沿也最具挑战性的部分，因为 Mathlib4 的代数几何库仍在建设中。我们可能需要从更基础的概念（如多项式理想的零点集）自行定义一些中间概念。

5.4 可计算性与经典逻辑

数学证明中大量使用“存在性”和“选择”。在构造算法时，我们有时需要从“非空集合”中选取一个元素。这涉及到是否使用选择公理Classical.choice。如果希望算法是完全可执行的（即能在 Lean 的虚拟机中运行并给出具体结果），我们需要避免使用不可计算的经典公理，或者将其限制在证明部分。这要求我们仔细区分“证明存在”和“计算得到”。例如，从集合中选取主变元最小的多项式，如果序是线性的且集合有限，这个选取是可以构造性完成的，无需经典选择。

6. 验证实例：从简单方程组到几何定理

理论实现之后，需要用实例来测试和展示。我们可以设计几个层次渐进的例子。

6.1 简单线性方程组

首先是一个简单的例子，几乎可以用心算验证。例如方程组{x + y - 1, x - y - 3}。我们的 Lean 4 实现应该能计算出特征列（可能形式为{x - 2, y + 1}或等价形式），并附带证明该特征列与原方程组等价。我们可以写一个测试：

example : let vars := [`x, `y] in let ps : Finset (MvPolynomial vars ℚ) := {X `x + X `y - 1, X `x - X `y - 3} let cs := wu_characteristic_set ps (by decide) in ZeroSet cs = ZeroSet ps := by native_decide

这里by decide可能用于提供变元序的证明，native_decide可以自动计算和判断有限域上的等式。这个例子主要测试算法流程是否畅通。

6.2 非线性代数方程组

考虑一个经典例子：求圆x^2 + y^2 = 1和直线y = x的交点。方程组为{x^2 + y^2 - 1, y - x}。吴方法应能产生三角列，例如{y - x, 2*x^2 - 1}，清晰地给出x = ± √(1/2)的关系。在 Lean 中，我们需要处理平方根，这可能会引入域扩张。测试的重点可能在于验证ZeroSet(CS) ∪ ZeroSet(Initials)是否覆盖原零点集，而不是具体解出数值。

6.3 几何定理的机器证明

这是吴方法的标志性应用。例如，证明“三角形三条高线交于一点”（垂心定理）。我们可以将几何条件坐标化、代数化，得到一组假设多项式方程H1, H2, ..., Hk，以及结论多项式方程G = 0。吴方法的过程是：

1. 将结论多项式G添加到假设集合，形成PS = {H1, ..., Hk, G}。
2. 计算PS的特征列CS。
3. 检查G是否可以被CS中的多项式约化为零，或者检查CS是否包含非零常数。 如果G对CS的余式为零，且在假设条件下CS中多项式的初式不为零（非退化条件），则定理成立。

在 Lean 4 中，我们可以将整个定理表述为一个Theorem：

theorem orthocenter_theorem (A B C H : Point) (h1 : collinear A B C → False) ... : let assumptions : Set (MvPolynomial [`x_A, `y_A, ...] ℚ) := ... in let conclusion : MvPolynomial [`x_A, `y_A, ...] ℚ := ... in ∃ (non_degen_conds : List (MvPolynomial ...)), (∀ cond ∈ non_degen_conds, cond ≠ 0) ∧ (characteristic_set_implies assumptions conclusion non_degen_conds) := by run_tac wu_tactic -- 这里需要一个自定义的 tactic 来调用我们实现的算法

这需要我们将算法包装成一个 Lean 的Tactic，使其能自动执行计算、构造余式为零的证明、并提取非退化条件。这是将形式化验证推向自动化应用的关键一步。

7. 实操心得与常见陷阱

在尝试进行此类形式化项目时，我积累了一些经验教训。

首要原则是“小步前进，频繁验证”。不要试图一口气写出完整的算法并证明。应该从最微小的单元开始：比如先定义变元序，证明它是全序。然后实现单变元的伪除，并证明其规范。接着实现用单个多项式约化另一个多项式，再推广到用三角列约化。每一步都用简单的例子（比如两个明确的多项式）在 Lean 里#eval或#check一下，确保计算方向正确，类型无误。

警惕“等式爆炸”。多项式运算，特别是符号运算，在 Lean 的项中可能会产生非常庞大的表达式。在证明中，直接使用simp或ring可能会超时。需要更有策略地使用化简规则，有时需要手动引导化简顺序，或者使用polyrith这类专门针对多项式等式的决策过程（如果 Mathlib4 已经集成或能接入）。

设计良好的中间抽象层。直接操作MvPolynomial的底层表示（如monomials和coeffs）会非常痛苦。尽可能利用 Mathlib4 已经证明的高级引理，比如关于degree、leadingCoeff、eval的定理。为自己频繁使用的操作（如“获取多项式p关于变元x的主系数”）封装函数和配套的引理库。

正确处理“可判定性”。算法中充满了判断：多项式是否为零？是否为常数？两个变元序关系如何？在构造性数学中，这些都需要可判定的（Decidable）实例。对于自定义的VarOrder，你需要提供DecidableEq和DecidableLT的实例。对于多项式是否为零，MvPolynomial在系数环可判定时通常是可判定的，但要注意效率。在证明中，使用by decide可以自动解决许多简单的可判定命题。

性能与抽象的两难。为了证明的简洁性，我们可能希望使用更抽象的数学定义。但为了算法的可执行性，我们又需要具体的计算。一个折中方案是：先在一个更具体、可计算的上下文中（如MvPolynomial (Fin n) ℚ）实现和验证核心算法，证明其逻辑正确性。然后，如果需要更一般的类型（如任何CommRing R和变元集），尝试通过抽象或重写来推广，并证明推广后的版本与具体版本在可计算的情况下行为一致。这比一开始就在完全抽象的层面挣扎要可行得多。

最后，形式化一个像吴方法这样中等复杂度的经典算法，是一个系统工程。它考验的不仅是数学理解和编程能力，更是使用交互式定理证明器进行“数学软件工程”的耐心与规划能力。每完成一个引理的证明，每让一小段代码通过类型检查，都是向完全可验证的数学计算迈出的坚实一步。这个过程本身，就是对算法理解最深刻的淬炼。