几何定理的机器证明(转载)
2006-08-13 15:55阅读：
现在大家应该已经形成这样的认识：算法就是针对一类问题的程序性方法，所谓程序性就是每前进一步都有章可循地确定下一步做什么和怎么做。从思想方法上你一定感到这与我们学过的欧氏几何有很大不同，算法思想是从问题解决出发给出算法解而不是按照定义——公理——定理——证明的演绎系统进行的，此二者就是数学发展史中发挥巨大作用的机械化思想和公理化思想。
与源于古希腊的欧氏几何不同，中国古代的几何学乃至整个数学是“术”（算法）的科学，强调构造性、算法化，注意解决科学实验和生产实践中提出的各类问题。例如由观天测地产生的勾股弦公式、日高公式等都是这样的，又如在《四元玉鉴》中己经指出，如果引入天元(即未知数)并建立相应的方程，通过解方程即可自然导出这些几何公式。由此提供了一条证明与发现几何定理的新路：把非机械化的定理求证归结为机械化的方程求解。首届（2001年）国家最高科技奖获得者吴文俊先生曾明确提出，中国古代数学是一种机械化数学，数学机械化思想是中国古代数学的精髓。吴先生的研究起到了正本清源的作用，证实中国古代数学是世界数学的主流之一，促进了西方数学与中国古代数学两大主流的融合，推动了数学的发展，同时也掀起了对中国数学史再认识的新高潮。
公理化体系的几何定理证明非常不机械化。我们都有这样的经验，一个平面几何定理的证明，往往要经过冥思苦想，奇巧构思，无章可循地添加辅助线，迂回曲拆地给出证明。如何利用计算机进行自动推理，特别是进行几何定理的自动证明，是学术界长期研究的课题。所谓定理的机械化证明，就是对一类定理（这类定理可能成千上万）提供一种统一的算法，使得该类定理中每个定理，都可依此方法给出证明。从“一理一证”到“一类一证”，这是数学认识和实践的飞跃。
我们研究的几何机械化问题历史上可以追溯至十二、三世纪宋元时期初次出现的几何学代数化，将几何学问题化为多项式问题，以及相伴而生的多项式组消去法。事实上，早在17世纪大哲学家、大思想家和大数学家莱布尼兹就有机械化证明的设想。只是直到19世纪末及以后由于希尔伯特及其追随者们建立并发展了数理逻辑，这一问题才具有了明确
的数学形式。又由于20世纪40年代计算机的出现，才使这一设想有了现实的意义。以下我们按照时间顺序简要介绍一下几何机械化的背景：
在希尔伯特的经典著作《几何基础》中我们可以发现两条机械化定理H和P，这一类可机械化的几何定理的特征是假设部分的代数关系式对于某些特定变量都必须是线性的。这种机械化方法效率最高，即使用手算也可证明颇不简单的定理，但其使用范围过于狭窄。20世纪30年代，美国数学家J.F.Ritt提出了代数几何的构造性理论，并首先提出了多项式组约化整序、特征列等概念，为吴文俊后来的工作铺平了道路。一个必须介绍的人物是波兰数学家Tarski，他在1948的一篇经典著作中解决了实闭域的判定问题，其主要目的之一是给出初等几何定理的机械化证明。只是该方法效率颇低，虽经Seidenberg等人优化仍是繁到不可收拾，因而远远不是切实可行的。1964年Hironaka提出了Grobner基的概念，他称之为“标准基”。1965年B.Buchberger在他的博士论文中深入研究了Grobner基的性质，并给出了Grobner基的算法及改进算法，Grobner基的名称来自于Buchberger的导师W.Grobner(1899~1980)。后文提到的Grobner基方法就是源于对Grobner基性质和算法的应用。吴方法是20世纪70年代末吴文俊先生受中国古代数学机械化思想影响，借助30年代Ritt的理论工作，针对几何定理机器证明问题研究和发展的新方法。吴先生不仅作了许多理论工作，鉴于吴方法的高效性，他还进行了大量的机证实验，证明和发明了不少几何定理。他的工作也影响了国内外一大批数学工作者，将几何机械化乃至整个数学的进程向前推进了一大步。适用吴方法证明的定理有下面特征：假设与结论部分的代数关系式都可以用多项式方程来表示。具体地说：
设A,B,C,D,E,F是平面上的点，借助解析几何知识下列几何性质可以表达为一个或几个多项式方程：
1.AB平行于CD；
2.AB垂直于CD；
3.A,B,C共线；
4.AB=CD；
5.C在以A为原点，AB为半径的圆上；
6.C是AB中点；
7.锐角ABC与锐角DEF相等；
8.BD是角ABC的平分线。
一般地，几何定理机器证明问题可以分成下面两个主要步骤：
第一步，用解析几何方法建立坐标系设未知量，将条件表示成所设未知量的多项式方程组G1，将求证表示成多项式方程组G2.（几何的代数化与坐标化）
第二步，用一定算法（如吴方法）判断G2是否可以由G1推出。（代数讨论的机械化）
我们也分这两步来介绍。第一步只要看一个简单的例子：射影定理的代数化
求证：直角三角形斜边上的高是斜边两线段的比例中项。
建立坐标系、设未知量如：
l
条件代数化：
1.
AD垂直于BC，斜率互为负倒数，整理得：h1(u1, u2, x1, x2)
= x1u1–x2u2 = 0
2.
D在BC所在直线上，整理得：h2(u1, u2, x1, x2)
= x1u2–x2u1–u1u2 = 0
条件是四元二次多项式方程组
l
求证代数化：
|AD|2 = |CD|·|BD|, 整理得：
g1(u1, u2, x1, x2) =
结论G2: g1(u1, u2, x1, x2) =
0
第二步也就是机械化的核心步骤：判断G2是否可以由G1推出。这样的问题就我们目前所学实在无能为力，甚至说清“推出”二字也很难。比较明显地我们说可以推出x2–y2–4
= 0还可以推出x =
0等，但是对多元高次的多项式方程组我们就必须借助高等的数学工具和计算机算法来帮忙了。
一种可行的算法是借助前面提过的Grobner基的性质，用计算机去求由多项式组{hi}和g生成的一种代数结构的Grobner基（一组多项式），看这组基中是否包含数字1来判断是否可以推出结论g
= 0.
吴方法同样是由{hi}构造一组多项式，称为广义特征列。判断g =
0对广义特征列的拟除余式是否为0，就知道求证是否成立了。
上述算法很难理解，事实上多项式方程组求解的问题非常困难，对这个问题的探索理论上引发了代数几何学的建立。我们试着用简单的语言对上面的方法作一点解说：（解释原理，数学上不一定精确）
要证多项式方程g = 0由多项式方程组{hi =
0}推出，就是要证：
g = c1h1 + c2h2 +…+ cnhn,
其中{ci}是和g, {hi}含有相同变元的多项式组。一种朴素的想法是g关于{hi}做除法：用h1去除g,
再用h2去除余式m1,
再用h3去除余式m2……只要最后hn除余式mn-1为0即可。但是由射影定理的例子可见g关于{hi}实行这样的除法是行不通的。于是我们想办法转化：Grobner基与广义特征列都是多项式组{pi}，使得所有写成d1p1
+ d2p2 +…+ dmpm形式的多项式的0点集合就是所有c1h1
+ c2h2 +…+
cnhn形式多项式的0点集合（这个集合是令多项式为0的各变元取值的集合，几何上称仿射簇，可以理解为保证多项式方程组同解）。于是问题转化成证明g
= d1p1 + d2p2 +…+
dmpm，由于Grobner基与广义特征列具有很好的代数性质，两种算法都可以采用类似多项式除法的办法进行验证。Gröbner基方法中考虑g模{pi}约化的范式（类似于前述多项式除法的最终余式），范式为0说明g
= 0 可由{pi =
0}推出，定理得证。吴方法中考虑g关于{pi}拟除的余式Rem(g, {pi}),
余式为0定理得证。
需要指出的是求Grobner基与广义特征列的过程同时也是多项式方程组消元的过程，比证明g =
0用途更广泛的是这两种方法同时给出了求解多项式方程组的有效算法（即使不能求出每个未知量，至少可以保证同解地消掉其中的一部分变元，因而也可用于多参数方程组消参），宏观上这类似前面正文讨论的消元法，因此吴方法也被称为吴消元法。同时吴文俊先生大力倡导数学机械化的应用，如应用于线性控制系统、机构综合设计、平面星体运行的中心构形、化学反应方程的平衡、代数曲面的光滑拼接、从开普勒定律自动惟出牛顿定律、全局优化求解等等。在他的指导和带动下，数学机械化方法还在一些交叉研究领域获得初步应用，如理论物理、计算机科学、信息科学、自动推理、工程几何、机械机构学等等。数学机械化研究正不断开拓更多的应用领域。
关于几何定理的机器证明最后再谈两点，其一文中介绍的Grobner基方法由于在求基的过程中引入大量中间多项式，又可能出现复杂的有理系数，该算法会占用大量的处理时间和存储空间在定理证明中效率远不如吴方法高。二者效率详细对比和大量机证实验可参见http://zhwzh.bj4hs.edu.cn/paper/main.html.
最后一点引用吴文俊先生的话总结数学机械化的实质：
“把质的困难转化为量的复杂。”
这不也是算法思想的实质吗？
