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。算法核心循环如下从R中取出一个多项式f。用当前的三角列B对f进行完全约化。即依次用B中的每一个多项式按其主变元从高到低的顺序对f进行伪除得到一个余式r。这个r关于B中所有多项式的主变元次数都是已约化的。如果r是零多项式那么f是当前理想中已有的多项式丢弃它。如果r是非零常数同样表明方程组无解算法可提前终止返回{1}。如果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或FinsetList可以保持顺序这对于三角列至关重要多项式顺序对应变元顺序。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。吴方法的过程是将结论多项式G添加到假设集合形成PS {H1, ..., Hk, G}。计算PS的特征列CS。检查G是否可以被CS中的多项式约化为零或者检查CS是否包含非零常数。 如果G对CS的余式为零且在假设条件下CS中多项式的初式不为零非退化条件则定理成立。在 Lean 4 中我们可以将整个定理表述为一个Theoremtheorem 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和变元集尝试通过抽象或重写来推广并证明推广后的版本与具体版本在可计算的情况下行为一致。这比一开始就在完全抽象的层面挣扎要可行得多。最后形式化一个像吴方法这样中等复杂度的经典算法是一个系统工程。它考验的不仅是数学理解和编程能力更是使用交互式定理证明器进行“数学软件工程”的耐心与规划能力。每完成一个引理的证明每让一小段代码通过类型检查都是向完全可验证的数学计算迈出的坚实一步。这个过程本身就是对算法理解最深刻的淬炼。