自动几何定理证明中吴方法恒等式证明的结构化重构

《Mathematics》：A Structured Reconstruction of Identity Proofs in Wu’s Method for Automated Geometric Theorem Proving

　　

自动化几何定理证明旨在利用计算机机械地证明几何定理。源于自动推理，随着计算机代数学和符号计算的发展，该研究领域已逐渐演变为人工智能与自动推理交叉的核心方向之一。现有自动化几何定理证明方法包括综合法、演绎数据库方法、几何不变量法以及基于计算机代数的代数方法，如吴方法（Wu’s method）和基于Gr?bner基（Gr?bner basis）的方法等。其中，计算机代数方法将几何命题表述为点坐标上的多项式方程，并通过大量多项式变换完成证明。吴方法和Gr?bner基方法是此类方法中的代表，理论上均能保证判定IMO-AG-30中所有几何定理的真值。吴方法被视为自动推理领域的开创性成就，它将几何定理证明转化为多项式代数问题，从而自然契合计算推理。由于其在证明等式型几何命题方面的完备性和高效性，它已成为数学机械化中的基本方法之一。然而，由于其证明过程严重依赖多项式变换和复杂的消元过程，生成的证明往往难以理解，其潜在的几何结构难以辨识，这限制了其在教育和研究中的应用。

为解决上述问题，Zou等人在吴方法发展的基础上指出，通过对其消元过程进行适当改进，待证结论可表示为从给定条件导出的多项式与多项式系数的组合形式，从而直接导出命题的恒等式证明。换言之，对于可代数化表述的几何命题（即等式关系），可以构造如下形式的恒等式：

$$cg = \sum_{i} q_i f_i$$

其中$f_i$为假设的多项式表示，$g$为结论的多项式表示，$q_i$为适当的系数多项式。一旦该恒等式建立，结论的有效性即可在代数形式上严格导出。此类恒等式证明并非将论证仅仅呈现为一系列复杂的消元步骤；相反，它们明确揭示了假设与结论之间的逻辑关系，从而显著提高了证明的结构化程度与可读性。在吴方法的框架下，这种基于恒等式的视角在保持吴方法完备性的同时，大大增强了证明的结构表达能力。然而，相关工作主要停留在理论层面，缺乏可执行的算法框架以支持基于恒等式方法的实际应用。

与此同时，几何表示的创新也成为提升证明可读性的另一关键突破。与繁琐的坐标展开相比，点几何（point geometry）作为一种通过加法、减法、内积和外积直接对点进行操作的几何代数框架，提供了更为自然和紧凑的几何结构表达方式。点几何继承质点几何和向量几何的代数逻辑，同时消除了传统坐标方法中对原点和基方向的固有依赖。它在表示中保留了几何直观性，更适合结构优化和自动推理。当与基于恒等式的方法结合时，点几何表述可在保持计算严谨性的同时进一步增强结构优雅性和人类可解释性。

Peng等人将点几何引入基于恒等式的证明构造中，以点的代数运算替代传统坐标展开，发展了一种基于点几何的恒等式证明方法。该方法不仅继承了吴方法对等式型问题的完备性，还融入了点几何的代数结构，包括加法、标量积和向量构造，使恒等式表达更为紧凑，几何结构更为透明。在此基础上，后续研究进一步探索了其在几何命题自动生成和几何关系识别等任务中的潜力，为几何知识的发现与表示提供了新视角。然而，该方法尚未发展为完全可执行的算法框架，其普适性和理论深度仍需进一步系统研究。

为此，本文聚焦于基于恒等式方法的理论重构与可执行实现，旨在提高传统代数方法的结构可解释性和人类可读性。本文的主要贡献如下：研究人员引入了与余式多项式相关联的余式追踪矩阵（Remainder Tracking Matrix, RTM），提出了一种可追踪的特征列构造与记录的方法；设计并实现了基于吴方法的完整恒等式生成算法，支持从给定假设集中自动生成结构化恒等式证明；通过若干几何命题实例验证了所提方法的有效性，并展示了其在结构优化、公式解释和潜在定理发现方面的实际潜力。

## 研究背景与问题

自动化几何定理证明是数学机械化与人工智能交叉领域的核心研究方向。在该领域中，吴方法通过将几何命题代数化为多项式方程，并利用高效的伪除法（pseudo-division）消元机制完成定理判定，已成为最具代表性的代数方法之一。然而，吴方法在实际应用中存在显著的局限性：其证明过程依赖于大量多项式变换和复杂的代数消元操作，生成的证明以多项式序列的形式呈现，难以直观揭示假设与结论之间的推理关联，导致证明的可解释性和可读性严重不足。这一问题限制了吴方法在教育验证、几何知识发现等需要人类理解场景中的应用。

传统的恒等式证明思想为解决上述问题提供了理论方向。该思想的核心在于构造一个恒等式，将结论多项式的某个倍式表示为假设多项式与多项式系数的线性组合，从而使命题的正确性在结构上清晰可见。然而，现有的基于恒等式的方法多停留在理论层面，缺乏系统化的算法实现，无法支持从假设集到恒等式的自动化构造。具体而言，如何在吴方法的特征列（characteristic set）构造过程中同步记录多项式系数依赖关系，如何将隐含的代数消元过程转化为具有明确逻辑语义的结构化证明表示，以及如何实现可执行的恒等式生成算法，都是亟待解决的关键问题。此外，点几何等新型几何表示框架虽能增强证明的几何直观性，但尚未与恒等式方法深度整合，其算法化、系统化实现仍处于初步探索阶段。

## 研究内容与主要结论

本文围绕吴方法的证明机制重构展开研究，从恒等式证明的视角出发，建立了吴方法代数消元过程的结构化理论框架，并实现了可执行的算法系统。研究的主要内容和结论包括：

**余式追踪矩阵的引入与理论构建。** 研究人员提出了余式追踪矩阵（Remainder Tracking Matrix, RTM）的概念，用于系统记录多项式集合在代数运算过程中生成的多项式系数依赖关系。RTM确保每个生成多项式相对于原始假设多项式集都具有清晰的矩阵表示，实现了构造过程的可追溯性和结构化组织。基于RTM，本文建立了特征列与假设集之间的显式多项式系数关系，为恒等式构造奠定了代数基础。

**恒等式方法的理论重构。** 通过建立结论多项式与假设多项式之间的恒等表示，研究人员将吴方法的代数消元过程转化为具有明确逻辑语义的结构化证明表示。具体而言，在特征列的逐步构造过程中，每个多项式均可表示为原始假设多项式的系数组合，这一关系通过RTM完整记录；进而，结论多项式关于特征列的伪余式为零时，可通过RTM回溯至原始假设集，构造出形如 $cg = \sum q_i f_i$ 的完整恒等式。

**算法设计与实现。** 研究人员设计并实现了完整的恒等式生成算法，包括基于RTM的初始化、特征列构造与同步演化、结论多项式恒等式构造等关键模块。该算法支持从给定假设集自动生成结构化恒等式证明，将理论层面的恒等式方法转化为可执行的计算框架。

**实例验证与应用展示。** 通过垂心定理、Desargues定理、Simson定理等典型几何命题的机器辅助验证，研究人员展示了该方法在构造可读性证明方面的有效性，验证了其结构化表示优势和实际应用潜力。

该论文发表于《Mathematics》期刊，为吴方法中几何证明的结构化表示提供了新途径，并为几何不变量的代数表征以及自动化几何定理证明可解释性的提升奠定了理论基础。

## 关键技术方法

本研究采用的技术方法主要包括以下方面：（1）特征列构造与伪除法消元，基于Ritt-Wu框架实现多项式系统的三角化；（2）余式追踪矩阵（RTM），用于在特征列构造过程中同步记录多项式系数依赖关系的矩阵表示工具；（3）多项式对结构的余式算法，包括多项式间余式计算（prem）、多项式关于升列的余式计算（prems）、多项式集合关于升列的余式计算（remset）等核心运算模块；（4）恒等式构造算法，通过结论多项式关于特征列的伪余式判定与系数回溯，实现从特征列到原始假设集的恒等式恢复。实例验证中的几何命题采用标准坐标代数化模型。

## 研究结果

**特征列的构造过程与结构性质。** 研究人员系统阐述了特征列的迭代构造机制：从初始多项式集出发，选取基集（basic set/baseset），计算多项式集关于该基集的余式集，将余式集添加至原集合形成扩展集，重复选取基集和余式计算直至余式集为空。该过程揭示了特征列的三项关键结构性质：迭代生成性，即元素通过前一步迭代的多项式集经余式计算和系数组合逐步生成；显式代数依赖性，即每个多项式均可表示为原始假设多项式与多项式系数的组合；稀疏性，即新多项式的系数表示通常仅涉及部分原始多项式，有助于提升后续算法的存储和计算效率。

**多项式余式计算的矩阵表示。** 研究人员建立了三个层次的矩阵表示体系：多项式间余式计算的矩阵表示，将单次余式运算中的被除式与除式分别表示为关于原始多项式集的代数组合矩阵，导出余式的矩阵更新公式；多项式关于升列余式计算的矩阵表示，按升列逆序执行多轮消元，定义累积组合项矩阵Q，完整表达最终余式的矩阵结构；多项式集合关于升列余式计算与特征列构造，将矩阵表示推广至一般情形，确保特征列构造中每步余式生成均伴随显式的多项式系数组合关系。

**余式追踪矩阵的定义与性质。** 研究人员正式定义了RTM：设从初始假设多项式集生成的多项式集为S，若S中每个多项式均可表示为IS中多项式的系数组合，则记录这些多项式系数的矩阵M称为S的RTM。RTM在多项式集合进行余式计算或系数组合等代数运算时同步更新。RTM具有结构清晰统一、可追溯性强、便于计算和算法实现等显著优势。

**恒等式构造原理。** 基于RTM，研究人员建立了完整的恒等式构造机制：任何求解过程中生成的多项式P均可表示为初始假设集的矩阵形式P = Π_S · M^T；余式计算中，余式R获得更新的RTM M_R；特征列CS的每个元素C_i对应RTM M_i，满足C_i = Π_S · M_i^T；最终结论多项式g关于特征列的余式为零时，g可表示为g = Π_S · (M^Tb)^T = Π_S · ?^T，即完成恒等式构造。

**算法实现。** 研究人员实现了包含以下阶段的完整算法框架：初始化阶段，为初始假设集分配单位矩阵作为初始RTM，建立多项式与RTM行向量的一一对应；特征列生成阶段，基于迭代构造思想重复执行余式计算，持续更新和记录RTM直至确定特征列；恒等式判定与构造阶段，通过余式计算判定结论多项式，若余式为零则通过RTM显式构造恒等式。核心算法包括：create_poly_matrix_pairs（创建多项式-矩阵对）、prem（多项式对余式算法）、prems（多项式关于升列余式算法）、remset（多项式集合关于升列余式算法）、charset（特征列构造算法）、Gprem/Gprems（恒等式构造算法）、wumatrix（集成实现算法）。

**应用实例。** 垂心定理实例中，假设集对应两个多项式，构造的特征列为{-f₂, f₁}，对应RTM为单位矩阵，最终导出恒等式g ≡ -1/2·y₃·f₁ + 1/2·f₂，非退化条件为y₃ ≠ 0（几何上等价于点C不在AB上，确保三角形非退化）。Desargues定理实例中，假设集含六个多项式，构造的恒等式无需除法或消去操作，因而不需要额外的非退化条件。Simson定理实例中，假设集经特征列构造后，结论多项式关于升列的伪余式为零，在相应非退化条件下存在累积因子c使得c g可表示为特征列多项式的系数组合，通过代入最终获得关于原始假设集的显式恒等式表示。

## 讨论与结论

本文旨在提高吴方法生成证明的可读性。基于恒等式证明原理，研究人员引入了余式多项式的余式追踪矩阵概念，提出了特征列及其对应RTM同步构建的理论框架。该框架明确了恒等式方法中的结构映射关系，为吴方法的证明过程提供了代数重构。在此基础上，设计并实现了恒等式构造算法，通过若干典型几何命题的机器验证展示了该方法的可行性和有效性。

本文结论部分明确指出：未来研究将进一步结合点几何的表示优势与恒等式证明方法，可能产生具有更强几何直觉的证明；进一步研究还可能探索算法复杂度优化、几何知识库构建以及人工智能辅助推理。本项工作不仅拓展了吴方法在自动化几何定理证明中的表达范围，也为几何不变量的代数表征和几何知识的结构化发现提供了新的理论工具和实际途径。

具体研究结论可概括如下：本文通过引入余式追踪矩阵RTM，实现了吴方法消元过程中多项式系数依赖关系的系统化记录；建立了特征列与假设集之间的显式矩阵表示关系，将传统吴方法的"黑箱式"消元转化为可追溯、可解读的结构化证明；设计并实现了完整的恒等式生成算法wumatrix，支持从给定假设集自动生成结构化恒等式证明；通过典型几何定理的验证，证实了该方法在提升自动几何证明可读性和可解释性方面的实际效果，为自动化几何定理证明的进一步发展提供了理论基础和方法论支持。