10. 计算机证明的吴方法

1977年，吴文俊院士在《中国科学》上发表论文《初等几何判定问题与机械化问题》；1984年，吴文俊出版学术专著《几何定理计算机证明的基本原理》，依照机械化观点系统地分析了各类几何体系，明确建立了各类几何的机械化定理，着重阐明几何定理机械化证明的基本原理。1985年，吴文俊的论文《关于代数方程组的零点》发表，具体讨论了多项式方程组所确定的零点集。这篇重要文献，是正式建立求解多项式方程组的吴文俊消元法的重要标志。与国际上流行的代数理论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的学术路线。自此，“吴方法”宣告诞生，为数学机械化研究揭开了新的一页。
“吴方法”的基本思想，首先借助坐标系，把定理的假设与求证部分用一些代数关系式表示出来，即“几何问题代数化”，然后再把表示代数关系的多项式做适当处理，即把终结多项式中的坐标逐个消去，当消去的结果为零时，定理也就得到了证明。
几何问题代数化是几何问题机械化的第一步，为此需要引进数系，建立坐标系，把几何命题图中的各种关系利用代数方程描述出来。在适当选取坐标系后，如果几何定理的假设条件可表示为一组代数方程[H]：f₁=0，f₂=0，…，f_r=0，而几何定理的结论由代数方程C：g=0所刻画，这里f₁,f₂,…,f_r和g都是变元x₁,x₂,…,x_n的多项式，那么几何定理的机械化证明就归结为如下问题：机械化问题构造并提供一种确定的、机械的算法，使得依此算法进行有限步之后即可判定，在若干附加条件之下，结论C是否可由假设[H]推出，即是否可由f₁=0，f₂=0，…，f_r=0推出g=0。
由此可见，实现数学定理机械化证明的关键，在于必须对表示定理假设的多项式组[H]的零点集给出构造性的描述,以便区分多项式组[H]的零点集,从而可以确定在多项式组[H]零点集的哪部分之中,能够保证多项式g=0。吴文俊消元法（吴方法）恰恰完成了这项任务。因此，吴方法是定理计算机证明原理的理论基础，定理计算机证明的机械化原理的建立是吴方法的成功运用。
吴文俊原理设数学定理的假设条件由多项式方程组[H]＝0表示，定理的结论由多项式方程g=0表示。并设CS＝{A₁,A₂,….,A_k}为多项式方程组[H]的特征列。如果多项式g对[H]的特征列CS的余式R=0,则在条件I_i≠0（i=1,2,…,k）之下,可从[H]=0推出g=0。
条件I_i≠0（i=1,2,…,k），称为数学定理成立的非退化条件。这组非退化条件是在计算特征列过程中自动产生的。非退化条件这一概念的发现，是吴文俊在数学机械化证明领域的突出贡献。这一概念的引进，实现了数学定理计算机证明的决定性突破。
11. 吴方法计算机证明一例
下面，以初等几何定理“平行四边形的对角线相互平分”为例，分三步说明如何用吴方法进行几何定理的计算机证明。
第一步：几何问题代数化
①建立坐标系，选好命题诸元
建如上图所示的坐标系：取点A、B、C、D为平行四边形的四个顶点，且选点A为坐标系的原点，线AB在x轴上，E为对角线AC和BD的交点；它们的坐标分别取为A(0,0)，B(u1,0),C(u2,u3),D(x1,u3),E(x2,x3)，其中u1,u2,u3为自由变元，x1,x2,x3为约束变元。为保证平行四边形ABCD不退化，要求 u1≠0、u3≠0；为保证AB∥DC，点A、B的第二个坐标同为零，点C、D的第二个坐标同为u3。
②把几何命题图中的各种关系利用代数方程描述出来
由线段AB = DC，得： ？1= u2-u1-x1= 0；
由B，E，D三点共线，得：？2 = x3(x1-u1)-u3(x2-u1)=0；
由A，E，C三点共线，得：？3 = x3u2-u3x2=0；
③待证明的结论为：
第二步：整序（三角化）

第三步：进行逐步除法

这里的二、三两步可用计算机完成。
大家看完这一证明后，可能感到此法比用两角夹一边证明 ABE和 CDE全等来证明“平行四边形的对角线互相平分”复杂很多。只从此一例来看，的确如此。但当从计算机证明来看问题，其意义就大不相同，而是开辟了数学定理证明的一个新方向，提供了对一大类几何问题的证明方法，前景不可限量。