数理化知识宝典：数学领域的重要突破

几何，其严密的逻辑推理使人信服，其精巧的思维方法令人陶醉。它以其独特的魅力吸引着众多的数学爱好者。2000多年以来，一直统治几何学的传统证题方法，在当代计算机参与下受到了挑战，从而使几何证题又出现了一条新路。

机械证明的创立

利用机械进行运算的想法，最早可以追溯到中国古代数学。中国估算以算法为中心，注重计算技术的提高，与古希腊及其延续的数学公理化和演绎推理的传统迥然不同。从实际问题出发，建立算法的机械化一直是古代中国数学研究的传统，也是中国数学家所努力的方向和孜孜以求的目标。成书于公元前1世纪的数学名著《九章算术》是中国算法机械化的光辉典范。《九章算术》中解决问题的方法，不是公理化的演绎法，而是按照一定的程序运算获得结果，算法化、程序化很强，即使求解几何问题也是如此。17世纪中叶，笛卡儿有过类似的思想，可惜他的设想未能实现。

近代的机器证明思想由莱布尼兹首先提出，他设想过数学领域的推理机器，并认识到这一计划的重要性。但是，莱布尼兹并没有能实际地去实现自己的计划。到了19世纪末，希尔伯特等创立并发展了数理逻辑，为定理证明机械化提供了一个强有力的工具，使这一设想有了明确的数学形式。

20世纪40年代，电子计算机的出现才使前人设想的实现有了现实可能性。到50年代，机器证明开始兴起为一个数学领域。人们试图把人证明定理的过程，通过一套符号体系加以形式化，变成一系列在计算机上自动实现的符号计算过程。数学家们首先从最古老而不太复杂的欧氏几何开刀。

我们知道，欧氏几何学中的许多性质、定理，通过观察图形或实验并不难了解，但要给出严格的证明，有时就非常困难。数学家和计算机专家瞄准这一崭新领域开始进军了，根据计算机高速运算能力和程序化过程，对几何命题的逻辑关系进行联接。1950年波兰数理逻辑学家塔斯基断言一切初等几何和初等代数范围内的命题，都可以用机械化方法判断其真伪，这使人们很受鼓舞。1956年，美国人纽厄尔、西蒙和肖乌等人通过研究证明定理的心理过程，建立了机器证明的启发式搜索法，编制了一个“逻辑理论机”程序，用计算机成功地证明了38条定理，这一年被看作历史上计算机证明以至于人工智能研究的开端。1959年，美国洛克菲勒大学数理逻辑学家王浩教授设计了一个用计算机证明定理的程序，计算机只用了9分钟，就证明了350多条并不简单的定理。

1975年以后，数学家创立新理论，开创新方法，开始了计算机证明世界数学难题。1976年6月，美国数学家阿佩尔和哈肯等人用高速计算机工作了1200小时，向全世界宣布证明了困扰数学界百余年的“四色猜想”难题，轰动世界，震撼全球。从中初步摸索了一些规律和途径。

中国人的骄傲

1976年，中国科学院院士、中国科学院系统科学研究所研究员吴文俊教授，在拓扑学、几何学、数学史方面做出了卓越成就以后，开始了从事数学机械化尖端科学的研究。他发现《九章算术》的许多数学题都可以编成程序用计算机解答。在此基础上，他分析了法国数学家笛卡儿的数学思想，又深入探讨希尔伯特《几何基础》一书隐藏的构造性思想，开拓了机械化数学的崭新领域。

他的思路是把几何问题转变为代数问题，再按程序消去约束元或降低约束元的次数，使问题得到解决。(www.xing528.com)

按照这一思路，他编写了一种新程序，然后在一台档次很低的计算机上，几秒钟就证明了像西孟孙线那样不简单的定理，并陆续证明了100多条几何定理。他的算法被誉为“吴氏方法”。数学家周咸青应用吴氏方法也证明了600多条定理。这一新方法引起了科学界的高度关注。

1978年初，吴文俊又把他的方法推广到高深数学分支——微分几何定理机械化的证明，走出完全是中国人自己开拓的新数学道路。

在几何定理机械证明取得重大成功之后，到80年代，吴教授把研究重点转移到数学机械化的核心问题——方程求解上来，又取得了重大成功。这时，他不仅建立数学机械化证明的基础，而且扩张成广泛的数学机械化纲领，解决一系列理论及实际问题，他把机器定理证明的范围推广到非欧几何、仿射几何、圆几何、线几何、球几何等领域。他的成果在国际上产生了很大反响。

消点法震惊了世界

数学命题种类繁多，不可能所有的数学命题都能一下得到解决，于是有不少科学家研究更新的证明方法。

1991年，中国科学院成都计算机应用研究所研究员张景中及杨路等人发明了“L类几何定理证明器”，它可以在一台简单的电脑上判断命题的正误，也是用代数方法进行论证的。这些方法还不尽如人意，计算机只能判断命题的真假，并且计算过程很复杂，人们难以检验其是否正确。

1992年5月，张景中、周咸青和周小山在面积方法的基础上发明了“消点法”，编成了世界上第一个“几何定理可读证明的自动生成”软件。“消点法”把证明与作图联系起来，把几何推理与代数演算联系起来，使几何解题的逻辑性更强了。运用这一方法在微机上可以证明很多几何定理，并通过屏幕显示出证明的过程。这在当时是世界上最新、最好的几何定理证明软件。他们在电脑上证明了600多条较难的平面几何与立体几何定理。专家认为，这种证明方法，大多数是简捷而易理解的，甚至比数学家给的证明还要简短、实用。

“消点法”震惊了世界，它使机械证明定理上了一个新台阶。但是，“消点法”还不是证明几何题的通法，它主要是解决与面积有关的一些命题，而像几何作图、几何不等式、添加辅助线等问题尚未取得令人满意的成果。因此，“消点法”还不是机器证明几何定理的终点，这一问题有待于进一步探讨。

用电脑证明几何题，使几何学改变了从古希腊到现在一直沿用逻辑推证的传统方法，把逻辑思维才能获得定性化结论的问题，转化成通过计算能解决的定量化问题。由于实现了程序化、机械化，从而降低了几何学的难度。这不仅使几何学在电子信息社会获得新发展有了可能，而且有利于解决几何与其他数学难题，将会使几何学对于人类社会发展的贡献越来越大。