【其它】吴文俊与数学机械化
一、机器证明：古老的梦想相传 Ptolemy 王曾向 Euclid 请教学习几何的捷径， Euclid 没有屈从帝王的尊严，直率地说：几何中无王者之路 ( There is no royal way in geometry ) 。
以希腊的几何学为代表的古代西方数学，其特点是在构造公理体系的基础上证明各式各样的几何命题。几何题的证法，各具巧思，争奇斗艳，无定法可循，只有依赖个人的经验、技巧和灵感。 学习几何的孩子做梦都在想：要是几何题象解一元二次方程那样多好。这种愿望由来已久， 17 世纪法国的数学家 Descartes 曾有过一个伟大的设想：“一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。” Descartes 把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是全部科学的机械化。因为代数方程求解是可以机械化的。但 Descartes 没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座桥梁，实现了初等几何问题的代数化。
比 Descartes 晚一些的德国数学家 Leibnize 曾有过“推理机器”的设想。他研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言和造一台通用机器的构想。 Leibnize 认为，他的方案一旦实现，人们之间的一切争论都可以被心平气和的机器推理所代替。他的努力促进了 Boole 代数、数理逻辑以及计算机科学的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。
更晚一些，德国数学家 Hilbert 明确提出了公理系统中的判定问题：有了一个公理系统，就可以在这个系统基础上提出各式各样的命题，那么，有没有一种机械的方法，即所谓算法，对每一个命题加以检验，判明它是否成立呢？正是在 Hilbert 的名著《几何基础》一书中就提供了一条可以对一类几何命题进行判定的定理 — 当然，在那个时代，不仅 Hilbert 本人，整个数学界都没有意识到这一点。
数理逻辑的研究表明， Hilbert 的要求太高了。著名的 Godel 不完全定理断言：即使在初等数论的范围内，对所有命题进行判定的机械化方法也是不存在的！
数学大师们坚持不懈地求索，表明数学机械化的思想重要而深刻；而数学机械化在历史上发展缓慢，同时也意味着这一方向道路漫长而艰难。
证明的机械化，如果没有可以进行数学演算的机器，只能是纸上谈兵。电子计算机的问世，促使数学机械化的研究活跃起来。波兰数学家 Tarski 在 1950 年推广了关于代数方程实根数目的 Sturm 法则，由此证明了一个引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械方法判定。”可惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定理。
1959 年，著名数理逻辑学家，美国洛克菲勒大学王浩教授设计了一个程序，用计算机证明了 Russell 、 Whitehead 的巨著《数学原理》中的几百条有关命题逻辑的定理，仅用了 9 分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。特别的是，他第一次明确提出“走向数学的机械化”（ Toward Mechanical Mathematics ）。 1976 年，美国两位年轻的数学家在高速电子计算机上耗费 1 200 小时的计算时间，证明了“四色定理”，使数学家们 100 年来未能解决的难题得到肯定的回答。
在数学发展的漫长历史中，积累了无数的几何定理。这里面有许多巧夺天功、趣味隽永的杰作。由于传统的兴趣和应用的价值，初等几何问题的自动求解遂为数学机械化的研究焦点。自 Tarski 的引人注目的定理发表以来，已经 26 年过去了，初等几何定理的机器证明，仍然没有令人满意的进展。在经过许多探索和失败之后，人们在悲叹：光靠机器，再过 100 年也未必能证明出多少有意义的新定理来！
吴文俊的工作，揭开了机器证明领域的新的一页。
二、吴方法：王者之路
当中国的历史艰难地走出十年浩劫的磨难的时候， 1977 年，吴文俊在《中国科学》上发表的论文《初等几何判定问题与机械化问题》，为数学机械化领域送去了一缕清新的春风。 1984 年，吴文俊的学术专著《几何定理机器证明的基本原理》由科学出版社出版，这部专著遵循机械化思想引进数系和公理，依照机械化观点系统地分析了各类几何体系，明确建立了各类几何的机械化定理，着重阐明几何定理机械化证明的基本原理。 1985 年，吴文俊的论文《关于代数方程组的零点》发表，具体讨论了多项式方程组所确定的零点集。这篇重要文献，是正式建立求解多项式方程组的吴文俊消元法的重要标志。与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的学术路线。自此，“吴方法”宣告诞生，数学机械化研究揭开了她新的一幕。
几何问题的代数化是几何问题机械化的第一步，为此需要引进数系，建立坐标系，把几何命题的图中的各种关系利用代数方程来描述。在适当选取坐标系后，如果几何定理的假设条件可表示为一组代数方程 ： f 1 = 0 ， f 2 = 0 ， … ， f r= 0 ，而几何定理的结论由代数方程 C : g = 0 所刻画，这里 f 1 , f 2 ,… , f r 和 g 都是变元 x 1 ,x 2 ,…,x n 的多项式，那么几何定理的机械化证明就归结为如下问题：
机械化问题 构造并提供一种确定的、机械的算法，使得依此算法进行有限步之后即可判定：在若干附加条件之下，结论 C 是否可由假设 推出，即是否可由 f 1 = 0 ， f 2 = 0 ， ……
f r= 0 推出 g = 0 。
由此可见，实现数学定理机械化证明的关键，在于必须对表示定理假设的多项式组 的零点集给出构造性的描述 , 以便区分多项式组 的零点集 , 从而可以确定在多项式组 零点集的哪部分之中 , 能够保证多项式 g =0. 吴文俊消元法（吴方法）恰恰完成了这项任务。因此，吴方法是定理机器证明吴文俊原理的理论基础，定理机器证明的机械化原理的建立是吴方法的成功运用。
吴文俊原理 设数学定理的假设条件由多项式方程组 ＝ 0 表示，定理的结论由多项式方程 g =0 表示。并设 CS ＝ {A 1,A 2,….,A k} 为多项式方程组 的特征列。如果多项式 g 对 的特征列 CS 的余式 R=0, 则在条件 I i ≠ 0, i=1,2,…,k 之下 , 可从 =0 推出 g =0 。
条件 I i ≠ 0, i=1,2,…,k 称为数学定理成立的非退化条件。这组非退化条件是在计算特征列过程中自动产生的。非退化条件这一概念的发现 , 是吴文俊在数学机械化证明领域的突出贡献。这一概念的引进 , 实现了数学定理机器证明的决定性突破。
一般说来 , 用吴方法判定一个命题 , 要分三步进行 : 第一步是把所给命题化为代数形式，即判定一组多项式的公共零点集是否被包含于另一多项式的零点集的问题 ; 第二步是整序，即把刻划命题条件的多项式组 经整序化为升列 AS ；第三步是求余，即将刻划命题结论的多项式 g 对于升列 AS 约化求取余式 R 。 若 R=0 ，即可断定命题在非退化条件 I i ≠ 0, i=1,2,…,k 之下成立，或者说命题一般成立，其中 I 1, I 2,…, I k 是升列 AS 中各多项式的初式。若 R 不为 0, 则当 AS 为不可约升列时 , 可断定命题不真。
多项式方程组求解曾被认为是极为困难的问题 , 这已为它的研究历史过程所证明。但是 , 吴文俊消元法的叙述简明自然，顺理成章，结论易懂，方法易学。可以用相当短的时间向初学者介绍吴方法，并在计算机上具体操作吴方法的计算过程。初学者往往惊奇的发现：吴方法竟是这样的简单自然，感叹为什么别人没有发现它！事实上，将公认的难题，应用初等方法简朴自然地加以解决，是数学科学返璞归真的最高境界。
三、《九章算术》： 惟有源头活水来
50 年代，拓扑学刚刚从艰难迟缓的发展中走向突飞猛进，吴文俊敏锐地抓住了拓扑学的核心问题，在示性类与示嵌类的研究上取得了国际数学界交相称誉的突出成就。 1956 年荣获国家自然科学一等奖， 1957 年当选为中国科学院学部委员（现称院士）。那时他才 38 岁。作为一位年轻的数学家，这已是莫大的荣誉了。而对吴文俊来说，这只是在西方人开创的方向上做出的工作，新中国的数学家应该开拓出属于自己的研究领域。
但是，路在何方呢？那就是数学机械化！是什么力量使得吴文俊从一位卓有成就的拓扑学家，走上数学机械化的研究道路呢？吴文俊在《吴文俊文集》前言中有过动情的叙述：
作者关于机械化思想的形成，决非一朝一夕，至少在 70 年代以前，机械化的概念在作者脑海里还毫无踪影。经过对中国古代数学的学习和触发，结合着几十年来在数学研究道路上探索实践的回顾与分析，终于形成了这种数学机械化的思想。这种思想一旦形成，就自然地化成一股顽强的动力。十几年来，作者一直在这一方向道路上摸索前进，艰苦奋斗，义无反顾。
70 年代初，吴文俊开始研读中国数学史。中国古代数学曾有过辉煌的历史，直到 14 世纪，在许多数学领域都保持西方望尘莫及的水平。但是，西方一些数学史家不了解也不承认中国古代数学的光辉成就，将其排斥于“数学主流”之外。吴文俊对此作了正本清源的研究。 1975 年，他撰写了《中国古代数学对世界文化的伟大贡献》，文中详细列举在代数、几何、三角、解析几何和微积分等学科的发现和创立过程中，中国传统数学所起的重大作用，吴文俊认为：近代数学之所以能够发展到今天，主要是靠中国的数学，而非希腊的数学，决定数学历史发展进程的主要是中国的数学而非希腊的数学。这一论断在当时真可谓空谷惊雷，振聋发 聩 。此后，吴文俊对中国数学史的研究一发而不可收。大约在 1976 年，他的论文《我国古代测望之学重差理论评价—兼评数学史研究中某些方法问题》洋洋洒洒 3 万余言，列举参考文献达 48 种，从古代“重差理论”入手，见微知著，批判了数学史研究中“以今代古”所产生的巴比伦神话、印度神话以及丢番图神话；正是在此文中，吴文俊意识到“几何与代数的配合、代数的几何应用与几何的代数化正是宋元天元术的主要含义”，指出“在宋元数学家的手里为了发展天元术而建立了一整套的代数机器”。这为他日后机器证明思想埋下了伏笔。随后的另一篇文章《〈海岛算经〉古证探源》，提出了古证复原的三项原则，在数学史界引起了强烈反响。 1986 年，吴文俊应邀在国际数学家大会做 45 分钟报告，作为国际著名的数学家，吴文俊的报告却是“近年来中国数学史的研究”。 吴文俊热情讴歌中国古代数学的代表作《九章算术》。在他主编的《〈九章算术〉与刘徽》的前言中，他写到：“《九章算术》是我国数学方面流传至今最早也是最重要的一部经典著作。它承前启后，一方面总结了秦汉以前的数学成就，另一方面又成为汉代以来达两千年之久数学研究与创造的源泉。特别是三国时期刘徽的《九章算术注》，对数学理论多所阐发，影响深远。总之，《九章算术》与刘徽《九章算术注》，对数学发展在历史上的崇高地位，足以与古希腊的欧几里得《几何原本》东西辉映，各具特色”。他进一步指出：“作为一名中国的数学工作者，首先应该对自己的数学历史有深刻的认识，为此必须首先对《九章算术》与刘徽《九章算术注》有确切的了解。”“要预见数学的将来，不能不研究《九章算术》与《九章算术注》所蕴含的深邃的思想在数学发展过程中的历史功绩，也不能不正视正在展露头角的这种思想对数学现状的影响”。
吴文俊以一位数学家的素养敏锐地感受到中国传统数学“寓理于算”鲜明特点表现在它的机械化和构造性，他在论文《从〈数书九章〉看中国传统数学构造性与机械化的特色》中着力阐明了这一点。后来在为数学史家李继闵先生的著作《〈九章算术〉及其刘徽注研究》 作序时，他把自己多年研究数学史的体会系统完整地表述出来，他 指出：
我国传统数学在从问题出发以解决问题为主旨的发展过程中建立了以构造性与机械化为其特色的算法体系，这与西方数学以欧几里得《几何原本》为代表的所谓公理化演绎体系正好遥遥相对。《九章》与《刘注》是这一机械化体系的代表作，与公理化的代表作欧几里得《几何原本》可谓东西辉映，在数学发展的历史长河中，数学机械化算法体系与数学公理化演绎体系曾多次反复互为消长，交替成为数学发展中的主流。肇始于我国的这种机械化体系，在经过明代以来近几百年的相对消沉后，势必重新登上历史舞台。《九章》与《刘注》所贯穿的机械化思想，不仅曾深刻影响了数学的历史进程，而且对数学的现状也正在发扬它日益显著的影响。它在进入 21 世纪后在数学中的地位，几乎可以预卜。
也就是在这个时期，吴文俊到计算机工厂劳动，通过接触计算机，切身体会到了计算机的巨大威力，敏锐地觉察到计算机有极大的发展潜能。他一头扎进机房，从 HP-1000 机型开始，学习算法语言，编制算法程序。就这样，中国数学史的启发，“玩”计算机的感受，更是几十年在数学研究道路上的探索与实践，终于在吴文俊的脑海里升华为数学机械化的思想。 1977 年，吴文俊的论文《初等几何判定问题与机械化证明》发表于《中国科学》，吴文俊特地为此文写了一个附注，阐明机械化思想起源：
我们关于初等几何定理机械化证明所用的算法，主要牵涉到一些多项式的运用技术，例如算术运算与简单消元法之类。应该指出，这些都是 12 至 14 世纪宋元时期中国数学家的创造，在那时已由相当高度的发展。 … 事实上 , 几何问题的代数化与用代数方法系统求解 , 乃是当时中国数学家主要成就之一 , 其时间远在 17 世纪出现解析几何之前。
吴文俊汲取中华民族灿烂文化之精华，发扬中国古代数学的优良传统，创造了世所公 认的机器证明的“吴方法”，彻底改变了数学机械化领域的面貌。吴文俊的卓越建树，生动的证明了这样一个真理：正确认识和研究数学的历史，不仅是数学发展的必然要求，也是一个数学家永葆学术青春的重要源泉之一。
四、数学机械化：无尽的前沿
Fourier 曾有过这样的名言“对自然的深入研究，是数学发现最丰富的源泉”。然而，这还是不够的，还应该加上这样的续言：数学内容的不断丰富和在更深层次的成熟发展，必然对自然界的认识、理解和改造产生更大的作用。
吴文俊所倡导的数学机械化研究，一方面继承了古代中国数学思想的精华，一方面适应了现代科学技术的发展。数学机械化的研究最先在几何定理机器证明取得了突破性的成果，随着时间的推移、工作的积累和方向的拓展，数学机械化必将为中国乃至世界数学的发展做出积极的贡献，也必将使数学更好地为科学技术服务，尤其是为高科技提供理论武器和有效的工具。从几何的机器证明到内容更为丰富的数学机械化是一种必然的趋势。这里采撷几朵绚丽的奇葩，以展示数学机械化的应用和它对当代高科技的影响。
物理规律的发现 数学在解释物理现象、解决物理问题方面所处的重要地位是毋庸置疑的。今天，科学家们对于借助计算机和数学理论来发现物理规律的热情依旧不减。
在科学史上， Newton 通过观测和试验从 Kepler 定律导出万有引力定律是一个重要的历史事件。但是如何通过理论推导来重现 Newton 的伟大发现，这一点在现行的教科书里几乎没有触及。相反地，教科书中大量介绍了如何从 Newton 定律推导 Kepler 定律。
1986 年吴文俊访问美国 Argonne 国家试验室， Gabriel 教授正为如何借助计算机和数学工具，从 Kepler 定律推导出 Newton 定律而绞尽脑汁。回国后，吴文俊用自己的方法，通过计算机，完成了这一推导工作，并因此博得了许多科学家的称赞。国际自动推理研究领域的著名科学家， Argonne 实验室的 Wos 教授认为，吴的这一贡献对自动定理证明领域是一次极为重要的拓广，表现了吴的非凡的洞察力和卓越的智慧。进一步的工作揭示，假设对 Newton 定律一无所知，仅仅从 Kepler 定律的微分代数方程描述出发，经过整序运算，计算机自动产生了新的微分代数表达式，再加上一些技术性的分析，可以得到表达 Newton 定律的微分代数表达式蕴含在其中——也就是说，在假设 Kepler 定律的前提下，用计算机自动地发现了 Newton 定律， Newton 多年的心血，现在只需一刻钟的功夫，就重现于眼前，这真是一个激动人心的结果！
机器人与机构学 机器人的制造是多学科共同发挥作用的复杂的系统工程。工业机器人的主体基本上是一只类似于人的上肢功能的机械手臂，或是无关节结构，或是关节式结构。如果要在三维空间对物体进行作业，一般则需要具有六个自由度，即沿三个坐标轴的直线移动和绕这三轴的转动。例如， PUMA560 机器人，就是六自由度关节型电动机械手臂。对于这个具体的机器人，求解运动学方程，就是要决定各关节应转动的角度 q 1 , q 2 ,…, q 6 , 分别是多少 ? 这需要解一组非线性方程组如果采用数值迭代方法，求解过程很慢，同时也不能保证求出所有的解。一个自然的问题就是能否找出 q i 的封闭解。虽然就 PUMA560 来说，封闭解已被决定，但是对于一般的 PUMA 型机器人时，用吴文俊方法，依然可以求出特征列意义下的封闭解。而这是以往的方法很难达到的。
机构学是现代各种机械设计的基础，平面机构运动学分析与综合又是机构学的基础。此类问题研究主要是依据德国学者 L.Burmester 所建立的运动几何学方法 , 按照这个理论，平面机构综合问题有图解法和解析法两类。图解法过程繁复，工作量很大且不精确；解析法建模复杂，求解也复杂；若用数值法求解，又不易得到全部解。现在，借助于吴文俊整序方法，这类问题已获得了特征列形式的封闭解。
计算机科学中的应用 数学机械化在中国得以迅速发展，一个很重要的因素是计算机的介入。现在，一个可喜的良性循环已经形成，即数学机械化对于促进计算机科学自身的发展，对于计算机科学中的一些应用领域都产生了积极的影响 , 形成了投桃报李的局面。计算机视觉是一个重要的应用研究领域。这一方面，任何有意义的新结果，必然会促进机器人的发展。 1988 年和 1991 年，纽约大学的 Kapur 教授和通用电气公司的 Mundy 博士，敏锐而快速的把中国人创立和发展的特征列方法引入高科技的应用当中。用 Mundy 博士自己的话“最近我们发觉把吴文俊三角化方法和求根技术结合起来，可以形成解非线性约束问题的有效方法。我们在把这一方法用于机器视觉和过程控制”。
数学机械化与数学 机械化数学是数学的一部分，随着计算机大规模的渗透人们的生活，自然也改变了人们的学习、工作和从事研究的方式，一张纸、一支笔的情景基本上已成为历史。机械化数学的努力就是要将数学的各个领域一部分一部分的机械化，从而使传统数学的许多方面，由于有了数学机械化而面貌一新。这里仅列举一二。
微分几何、代数几何是引人入胜的数学分支，它们不但在理论的发展长河中考验了一大批杰出的数学家，在许多工程应用中也起到了不可替代的作用。 Clifford 代数与重要的 E.Cartan 外微分运算向结合，形成了局部微分几何定理的机器证明的新算法，利用这一结果可以给出陈省身关于曲面论中一个十分深刻的定理的非常简单的证明。代数几何中，在等价的意义下做分类，是非常重要且基本的问题。在一维情形下，用机械化数学的方法，做出了同构意义下的分类处理，是值得继续扩展成果的方向。
非线性发展方程的解，不仅仅是偏微分方程立论中关心的重要问题，同时它还具有十分明显的物理应用背景，一些著名方程，如力学，固态物理、等离子体物理和化学物理等领域中出现的一类非线性波方程，需要求物理上有兴趣的钟状、纽结状的孤立波解。现在已经应用特征列方法解过几十个非线性波方程，非线性发展方程。所得结果除涵盖已知解外，还发现了许多新解。
相辅相成、互惠互利，是机械化数学与一般数学关系的绝妙写照。
1981 年吴文俊在《数学的机械化与机械化的数学》一文中指出：“我们的研究工作还只是一个开端。如何继续发扬中国古代传统数学的机械特色，对数学各个不同领域探索实现机械化的数学，则是本世纪以致可能绵亘整个 21 世纪才能大体趋于完善的事。”近 20 年来 , 在吴文俊的积极倡导下，中国的数学机械化研究已初现丰富多彩之势。展望 21 世纪，我们有理由相信，机械化数学和数学机械化必将为数学以致整个科学注入新的活力。 不是原创也可以看看。
如果能用数学描述一切科学，用机械方法证明和求解一切数学问题，…… 引用第2楼醉乡常客于2006-07-22 00:41发表的“”:
不是原创也可以看看。
如果能用数学描述一切科学，用机械方法证明和求解一切数学问题，……
兄开玩笑了.根据哥德尔的定理,第一条是做不到的:) 兄说的是那个“总有不能啥啥”的定理吧！ 引用第4楼醉乡常客于2006-07-22 00:50发表的“”:
兄说的是那个“总有不能啥啥”的定理吧！
就是那个不能啥啥啥的定理:) 引用第1楼hooker于2006-07-22 00:25发表的“”:
http://www.mmrc.iss.ac.cn/~wtwu/
原来是一位大科学家的高论呀！ 迈向数学机械化：从塔斯基到王浩1
王磊
（上海交通大学科学史系，上海，200240）
摘 要：本文介绍了哥德尔不完备定理如何使希尔伯特定理判定问题研究陷入困境。评价了塔斯基在理论上给出了定理判定的方法意义。特别指出是王浩首次在计算机上实现了高效证明定理的方法，并明确提出“迈向数学机械化”。
关键词：数学机械化 塔斯基 王浩
一、 数学家的伟大设想
机器使人从体力劳动中解放出来，数学家们因而设想用机器解决数学问题，代替人从事脑力劳动。17世纪，法国数学家笛卡尔就曾设想用机械解决数学问题。借助“通用数学”把一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。笛卡尔创立的解析几何，在空间形式和数量关系之间架起了一座桥梁。1637年出版的《方法论》的附录《几何》就是尝试如何将代数应用到几何上，利用代数的一般性，把推理程序机械化以减小解题工作量，依据笛卡尔的设想，所有的几何问题都可以归结为代数方程的求解问题，在给方程问题寻求了标准解法后，完全可以用一种程序化、标准化的方式解决所有的几何问题。
德国数学家莱布尼茨在这一思想的基础上又前进了一步，他设想建立一种理想的“通用语言”，利用它来进行推理，使问题的正确性可以通过计算来验证。莱布尼茨计划创造两种工具，其一是通用语言；另一种是推理演算。前者的首要任务是消除现存语言的局限性、不规则性，使新语言成为世界上人人公用的语言；新语言使用简单明了的符号、合理的语法规则，便于逻辑的分析和综合。后一种，即推理演算，则用作推理的工具，它将处理通用语言，规定符号的演变规则，从而使逻辑的演算可以按照一条明确的道路进行下去。莱布尼茨还提出了直接进行机械乘法的思想。
1899年，希尔伯特在《几何基础》中提出了从公理化走向机械化的数学构想。希尔伯特计划将数学知识纳入严格的公理体系中，并着力在公理化基础上寻找机械化的方法判定命题是否成立。希尔伯特同时指出，定理的判定问题应当是分类解决的，解决方法要同时强调简单性和严格性。以希尔伯特为代表的形式主义学派，希望通过形式逻辑的方法，构造一个有关数论（自然数）的有限公理集合，推出所有数论原理（完备性）且无矛盾（相容性），并以此出发构造整个形式主义的数学体系。
1931年，哥德尔(Kurt G?del)发现并证明了著名的不完备定理，这条定理彻底粉碎了希尔伯特的形式主义理想。在形式逻辑中，数学命题及其证明都是用一种符号语言描述的，可以机械地检查每个证明的正确性，于是便能从一组公理开始无可辩驳地证明一条定理。哥德尔第一不完备定理，从根本上否定了这一设想。不完备定理实际上表明，这样的公理系统要么不完备，要么有矛盾。
二、 塔斯基：在否定中发现肯定
哥德尔不完备定理的否定性结论给定理判定问题的发展蒙上了一层阴影。然而，关于判定方法的研究结果并不全是否定的。1921年，波斯特（E.L. Post）为真值表判定法的有效性给出了严格的证明。1921年，兰福德（C.H. Langford）给出了线性次序初等理论的判定法。1930年，普列斯博格（M. Presburger）为仅包含加法运算的整数运算找到了判定法。1943年，麦克铿赛(J.C.C. Mckinsey)给出了初等格论全称语句的判定法。但是，突破性的进展源自塔斯基（A. Tarski）的工作。1948年，在《初等代数和几何的判定法》（A Decision Method For Elementary Algebra And Geometry）中，塔斯基推广了关于代数方程实根数目的斯笃姆（Strum）法则从而证明了一条重要定理：初等几何和代数范围的命题都可以通过机械方法判定。就本质而言，塔斯基的判定方法是一种“消去量词”的方法。实际上，塔斯基自己指出，这一证明方法早在1930年就已经获得，只是没有机会发表，它既可用来判定实数的初等代数中语句的成立与否，亦能用来判定初等几何语句。
在塔斯基看来，所谓初等代数，是指实数理论中的一个部分，其中仅用到表示实数的变量，表示个别数目的常数；表示施用于实数的初等运算和实数之间的初等关系的符号；还有初等的逻辑词项。在初等代数的公式中包含代数方程和不等式；用初等逻辑词项把方程、不等式连结起来，就得到初等代数的语句。另一方面，在初等代数中不存在用变量去代表的任意实数集合、实数序列或实数函数等等。塔斯基的“初等”概念是指不涉及集合论。
塔斯基首先构建了一个初等代数的形式系统，并定义出语句类。系统由变项、代数常项、代数运算符号、代数项、代数关系符号、原子公式、语句连接词、（存在）量词和公式构成。原子公式包括等式和不等式。公式由原子公式用语句连接词和量词构造。以此形式系统为基础，塔斯基建立了初等代数的判定方法。方法分为两部分。第一部分实现变换：对于任意给定的公式，总能用机械的方法找到一个与其等值的公式，它满足实现判定所需要的形式。第二部分实现判定：对于任意给定的不含量词的语句，总能用机械的方法判定它是否为真。在这个形式系统中，塔斯基成功地引入了判定代数方程实根数目的斯笃姆定理，比照方程求根处理命题判定问题。塔斯基的判定法在内容与形式上和斯笃姆定理有着很密切的联系，并且进一步把定理推广到了多个未知数的任意方程和不等式系的情形。
塔斯基指出，判定方法能告诉人们每一步做些什么，在运用它的时候不需要别的知识。只要能懂得判定方法并照着所指出的去做，就能进行定理判定。对于初等几何的判定问题，塔斯基坚持了将几何代数化的思想。初等几何语句就是指能够通过一个固定的坐标系把它变成初等代数语句的语句。塔斯基仔细考虑了二维欧氏几何的情况：欧氏平面中的任意点可以理解为多项式。利用三个常项表示点与点之间关系：二项关系“相等”用“＝”表示；三项关系“在中间”用“B”表示；四项关系“等距离”用“D”表示。变项与原子公式也用形式化的方式表示。初等几何语句即表达关于点的某个事实以及点与点之间的关系。三角形、平面、圆、直线等等的概念都可以翻译为这个代数系统的语言。要得到初等几何的判定方法，只须给每个初等几何的语句A对应一个初等代数的语句A*。从解析几何可以知道，A是真的，其充分必要条件是A*是真的。由于可以用机械的方法判定A*的真确性，则A的真确性可以机械地判定。塔斯基认为，虽然存在普遍适用于初等代数和几何的判定方法不能被认为是必然的，但是判定方法的存在却是必然的。
塔斯基给出的判定法是一种理论化的方法，在《初等代数和几何的判定法》一书中并无任何应用这种方法解题的例子。塔斯基得出的结论给定理判定问题的研究带来了曙光，虽然哥德尔不完备定理否定了希尔伯特的思路，但是在其他方向寻找判定方法是可行的。然而，尽管塔斯基的方法在理论上取得了成功，却因繁杂无比而难以在当时的计算机上证明稍有难度的定理。
三、 王浩：迈向数学机械化
二十世纪50年代，电子计算机诞生了。与以往的计算器械不同，电子计算机不仅可以实现数学计算的机械化，而且可以处理逻辑关系。二进制代码与开关电路结合得更好，大幅提高了运算速度。程序由外插变为内存，当计算题目改变时，不必变换线路板而只需更换程序。上述特点使电子计算机成为了证明数学定理的有力工具。
随着电子计算机逐步进入美国的大学校园和研究机构，利用电子计算机进行数学问题证明的研究蓬勃发展。1959年，美国洛克菲勒大学教授王浩设计了几个计算机程序，仅用3分钟，就在IBM 704型计算机上证明了罗素与怀特海《数学原理》中220条有关命题逻辑的定理，稍后又扩展到了400条，这一成果宣告了用计算机进行定理证明的可行性。王浩因此获得了1983年人工智能国际联合会和美国数学会联合颁发的“里程碑” （Milestone Prize）奖。 在1960年的《IBM研究与发展年报》（IBM Journal），王浩发表了《迈向数学机械化》（Toward Mechanical Mathematics），“数学机械化”一词即出自此处。这篇文章后收录于《数理逻辑总览》（A Survey of Mathematical Logic）的第9章，1959年由科学出版社出版。
为了达到用机器证明定理的目的，首要的工作就是将定理形式化，使人们可以像调试程序一般，实现用机械化方法检验新数学结果。先将命题证明形式化，以期实现机械化。总结以往对判定问题的研究，王浩认为应当在形式化方面加以修改，以适应机器进行证明的需要。对于一个命题的完整证明－判定过程应当建立在牢固的逻辑基础上，也就是谓词演算。“利用在数理逻辑中强调形式化这一优点的一个自然的想法，就是试图系统地利用计算机证明定理。” 2
王浩提出，研究的重点不应当局限于理论上的可判定性，而在于实际的可行性。同时，应当发展非构造性命题的构造性解释，把非构造性方法规约到构造性方法或用构造性方法来证明非构造性方法的正确性。存在两种不同的数学定理机器证明：一种是人利用计算机作为局部的辅助工具进行定理证明，这种方法以四色定理的证明为代表。四色定理的计算机证明在当时被认为是一个巨大的成就。但是王浩对此评价说，真正的数学机械化是要用电子计算机对整类的定理进行有效地判定。四色定理的机器证明有别于真正的定理机器证明，是在计算机辅助下的特例机证。如果按照证明四色定理的思路进行下去，那么虽然个别定理证明的部分脑力劳动被机器所替代，但是人们还需要为每个要证明的定理去设计程序。解决数学问题的难度与工作量并未有实质性的减轻。另一种方法就是以系统的机械化证明为特点的尝试。这种思想提出：要建立一种处理一类有关问题的一般方法，对于适用的问题能给出完全的解决。一个一般性的方法可以对给定的问题类找到判定过程，在应用这一证明方法时，这一类问题中的每一个都能够被判定，也就是说最终能确定它是不是定理。
计算与证明存在明显的不同：首先，处理对象不同。计算处理的对象是数字，而证明处理的对象是命题。其次，规则精确性不同。计算规则的精确性远胜过证明规则。再次，计算是有限的。计算过程是可判定的，可以递归的，或者可以通过数学近似方法达到这一目标。然而，证明过程通常不是有限的,它是不可判定的。对于近似方法，在定理的证明中还没有形成一个清晰概念。最后，计算有行之有效的步骤，而在证明中，判定方法并不显然。在计算中，简捷的方法并不具有普遍性，更多强调规则。在证明领域，人们依赖的仍然是直觉、洞察力、经验以及其它模糊而难以模仿的原则。除非能发现它们之间的特定联系，否则想要消除证明过程的复杂和冗长是不可能办到的。
数学研究处理的主要问题是计算和证明。计算器械的研制已经取得了许多伟大的成就，莱布尼茨、帕斯卡和巴贝基都曾进行过计算器的研制，电子计算机的出现更使得计算问题变得轻而易举。如果在数学研究中占有很大比重的定理证明工作不能实现机械化，无法用机器代替人脑，那么机械化的数学就不可能实现。毫无疑问，上述的不同之处是阻碍数学定理证明机械化的主要原因。王浩认为，数学定理的机器证明有赖于数理逻辑和计算机器的有力结合。
如何处理计算与证明的不同之处，王浩给出了自己的看法：首先，哥德尔对于第一个问题已经在理论上给予了回答，人们已经实现了利用数字机械处理字符信息。第二个不同之处，大体上已经被数理逻辑的形式化研究在过去八十年取得的成就所解决。第三个问题的解决对于定理机器证明也很重要。但是，现在关心的应当是它的实际可行性，而不是理论上的可能性。哥德尔不完备定理的结论并不妨碍现在所进行的尝试。对于“近似证明”这一概念，指由构想逐步改进并最终达到具体证明，从这个意义上说，是可以更精确的形式化的。王浩认为，最后一个不同之处也许是最根本的。以往的工作夸大了这个问题的复杂程度，这一部分是由于抽象的判定很难现实化，另一部分则是由于没有选择有效的替代程序。人对于大量细小问题的处理是无能为力的，这在本质上限制了数学研究的对象，以及数学处理问题的方式。机器在这些方面的优越性，可能会产生很多令人惊喜的新成果，而这得益于它们引起的新的转折，这正是人们所要适应的。基于上述讨论，王浩认为算法的分析要有推理分析和数字分析作为支持，这样才能实现数学问题求解的机械化。
早在1953年，王浩就已经开始思考用机器证明数学定理的可能性。1957年，在《对图灵计算机理论的改写》（A Variant to Turing's Theory of Computing Machines）一文中，他表达了自己对这一问题的初步的想法。1956年，认知心理学家在机器证明定理方面取得了举世瞩目的成就。纽维尔－肖－西蒙（Newell-Shaw-Simon）3的报告指出，在JOHNNIAC型计算机上，他们编制的程序LT（Logic Theorist）成功证明了罗素与怀特海的《数学原理》中第二章52条定理中的38条，对于其余14条定理，LT（Logic Theorist）程序没有找到证明。未能证明的定理绝大部分是由于超出了机器时间和存储空间的限制。1963年，他们在计算机上证明了全部52条定理。
1958年的夏天，王浩在波启浦夕（Poughkeepsie）的IBM研究实验室（IBM Research Laboratory）利用IBM704型计算机上编写了三个程序。1959年，王浩又进一步对这些程序进行了修改。程序是用SAP（Shared Assembly Programming Language），即公用汇编语言写成的。第一个程序为命题计算提供了证明－判定过程，它可以依据给定命题是否为一个定理，而给出证明或反证。利用这个程序，《数学原理》前五章的200多条定理在37分钟内证明完毕，由于其中12/13的时间是用来进行读入－输出操作，所以实际上用来证明的时间不足3分钟。这些定理中包含了纽维尔－肖－西蒙所证明的52条定理，用时不足5分钟。如果除去输入－输出所占用的时间，那么实际证明时间将不足半分钟。对于纽维尔－肖－西蒙不能证明的命题，或者需要较多时间证明的定理，则在几秒钟就给出了证明。
另外两个程序用来证明书中的其余定理。第二个程序用以指示机器利用基本符号形成命题，再从中选取出重要的命题。在一个小时之中，形成了1，4000条命题，并在磁盘上存储其中了选取的1000条定理。由于选取条件过于严格，所以选出定理不足十分之一。第三个程序作为一个大程序的组成部分，用来处理谓词演算。《数学原理》中关于谓词演算共有150条定理。王浩设计的程序在一个小时以内证明并打印了其中85％的定理。
王浩在研究中还发现，虽然理论上的结果表明，一阶逻辑在总体上是不可判定的，但是研究的结果却出人意料。因为王浩的计算机程序在不到九分钟的时间里证明了《数学原理》中一阶逻辑部分的全部定理（350条以上）。这说明了《数学原理》中全部一阶逻辑的定理都是属于一个简单且可判定的子域中。
虽然计算机运行得很快，但是粗糙的算法使问题的复杂性很快超出了计算机的能力。所谓算法，是指一组有穷的规则，它在任何时刻都能精确地告诉执行算法的人或机器，对某一类给定问题该做什么。如果给出某一问题类K的算法以及属于K的一个问题，那么只要执行算法所要求的操作，并精确地遵循已给规则，任何人都可以解决该问题。一个过程能够机械化，即能被一台机器或一个人用机械的、非创造型的方法执行。过程因素可以归纳为两个重要定理：有穷性定理和确定性定理。能够精确描述的任何过程都可编成计算机执行的程序，它应该是这样一个序列，即下一个状态由上一个状态的结果决定。由于理论的计算与可行的计算之间存在巨大的鸿沟，所以数学定理机器证明不应当仅仅停留于理论上的设想，而是要着手研究可以具体实施的方法。王浩意识到，应当注意通常的多项式复杂类，并认为有可能是取得突破的方向。
判定理论上的研究为数学机械化的展开奠定了基础，然而更为重要的是对实际可行性的研究，也就是如何真正用程序在计算机上高效地实现数学定理的证明。塔斯基的方法在设计时并未考虑电子计算机的特性，难以适应实际的运行要求。电子计算机的优点在于强大的数据处理能力，具备高速性和准确性。因此，为了用电子计算机证明定理，必须有一种与之相适应方法，也就是要设计一种能借助其强大功能的算法，充分发挥计算机的巨大威力。
王浩所取得的成就在当时震动了数学与数理逻辑学界，他的先驱性成就被人们誉为“一击落七蝇（Seven flies with one blow）”。这一现实的成功极大地激发了人们寻求用计算机高效证明定理的努力。正是王浩吹响了向数学机械化进军的号角。
参考文献
1. 塔斯基，初等代数和几何的判定法，科学出版社，1959
2. Feferman, Anita Burdman, Alfred Tarski：Life and logic, Cambridge University Press, 2004
3. Newell A., J. C. Shaw and H. A. Simon, Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristics, Computers and Thought, McGraw-Hill, 1963,134-152
4. Wang Hao, Toward mechanical mathematics, IBM Journal, 4 (1960), 2-22
5. Wang Hao, A Survey of mathematical logic, Science Press, Beijing (1962)
6. 王浩，数理逻辑通俗讲话，科学出版社，1981
7. 吴文俊，数学机械化，科学出版社，2003
8. 纪志刚，吴文俊与数学机械化，上海交通大学学报，2001，3，Vol.9
Toward Mechanical Mathematics: from Tarski to Wang Hao
Wang Lei
School of Humanities, Shanghai Jiao Tong University, Shanghai 20030, China
Abstract：This article explains the reasons why G?del's theorem of incompleteness made the research of theorem proving in difficult position and gives some comments on Tarski's theoretical method for theorem proving. The author points out that Wang Hao proposed "toward mechanical mathematics" firstly and practiced an efficient way in theorem proving on computer.
Key Words: Mechanical Mathematics; Tarski; Wang Hao
作者简介：王磊，上海交通大学科学史系在读硕士研究生
基金项目：上海交通大学人文社科基金“吴文俊与数学机械化”
2 王浩，数理逻辑通俗讲话，科学出版社，9页
3 Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristics, Report P-951, Computers and Thought, McGraw-Hill, 1963,134-152 数学机械化：回顾与展望
吴文俊
数学机械化这一名词取自数理逻辑学家王浩先生的著作。王浩先生毕生从事数理逻辑的研究，不仅是一位倡导用计算机来证明逻辑命题的先驱者，而且还身体力行。1958年时，王浩设计了几个计算机程序，使用当时的IBM704机，在3分钟内，自动证明了Russell与Whitehead的名 著“数学原理”一书中的220条命题，稍后又扩展到400条。这一成就震动了学术界，被誉为“一 击落七蝇（Seven flies in one blow)”。王浩先生还因此而于1983年获得人工智能国际联合会与美国数学会联合颁发的里程碑奖（Milestone Prize)。
王浩先生关于数理逻辑的文章，曾收集编写成<<数理逻辑总览(A Survey of Mathematical Logic)>>一书，于1959年由科学出版社出版，以下简称<<总览>>。书中的第9章，原来发表于1960年的IBM研究与发展年报。章名“向机械化数学前进(Toward Mechanical Mathematics)”，我们所采用的数学机械化一词，即出自此处。
该章第一节引论中，一开头即将计算与证明作一比较，指出两者有四大不同之处。简言之，如果用我们现在的词汇来说，计算是机械化的，而所谓证明则否。在本章中，王浩先生把数理逻辑的最基础部分（命题逻辑）的定理证明成功地归结为机械化的步骤，得以用机器获得自动的证明。在本章以及<<总览>>的其它诸章中，王浩先生还多处提出了在数学推行这种机械化证法的想法，使数学成为机械化的数学。
上面只谈了数学机械化一词的来历，至于它的实质意义，我想不必下什么艰深的学院式严格定义，只想请读者们回忆一下在中小学求学时学习数学的过程。在小学时，加减乘除与开方等运算都是按部就班依照一定的法则机械地进行的。但是像解鸡兔共笼一类所谓四则难题，就无法可循而需运用巧思。到初中一二年级学习代数，用各种消去法解线性联立方程组时，又像四则运算那样，可以依一定法则机械地逐步进行以至求出解答。但到学习几何时，就又像四则难题那样，证起定理来往往无所措手，需要高度的巧思。两种问题两种风格，其难易之别甚为显然，其关键就是其一是机械化的，而另一则否。是否能化难为易，以及如何才能化难为易，也就是如何把原来非机械化因而极为困难的数学问题变成机械化而容易起来，乃是数学机械化的主题思想，也是它的主要目标。
一个依据一定法则可以按部就班，机械地进行的方法在现代通称为算法。在当前的计算机时代，有算法即可编为程序，而在计算机上实施，因此当代的计算机科学大师Knuth，曾说计算机科学即是算法的科学。
中国数学源远流长，远古的数学成就，总结于<<九章算术>>一书，依据现存资料与地下文物，<<九章>>的成书年代，可大致定在公元前二，三世纪，其中成果大都以算法的形式出现。例如开平方的算法，在<<九章>>中称为开平立方术。对于鸡兔共笼一类问题，可用盈不足术来解答。更一般的问题，则有方程术与正负术，实质上即是解线性联立方程组的消去法与移项法则。在几何方面，中国根本不考虑定理与证明，而重在几何问题的解决。例如 田亩丈量与勾股测量一类问题，导致开平方术，相当于解最简单的二次方程。从<<九章>>以至历代的数学著作，其中成果大都以术的形式来表达。
总之，中国的传统数学，由求解几何问题以及其它各种类型问题所导致的方程求解成为古算发展的一条主线。解决问题的方法又往往以术亦即算法的形式出现，因而中国的传统数学，实质上是Knuth意义下的一种没有计算机的计算机科学，也正是王浩先生意义下的一种机械化数学。
中国传统数学通过化几何问题求解为方程求解而走上了一条机械化的道路。对于西方传统几何定理的证明以及其它种种数学领域中的定理证明，形式上与机械化格格不入，是否也可以找到 一条道路，使证明也成为机械化的呢。
中国传统的机械化数学，对此提供了入手的线索。
数学机械化之出现于古代中国，决非偶然。这里面有一层通常不为人所察觉更不易为人理解的深刻原因－－记数位值制的发明。
人人都知道记数的进位制，我们通常用的是十进位制。一个正整数不论多大，都可用相当于从0，1，到9的十个数字或符号甚或实物来表示。现代的计算机则用二进制来表示整数，这时只要用可以表示0与1的某种器件就行了。在技术上容易实现的二进制与人们习惯使用的十进制之间的转换，则用所谓译码器来实现。世界各古代民族，往往有着不同的进位制。例如古巴比伦用六十进位制，古希腊与埃及用十进位制，中美洲的玛雅民族则用二十进位制。然而，所有这些古代民族的进位制，都是不完全的，更谈不上意义重大的位值制了。
位值制是中华民族的创造，是世界上独一无二的独特创造。
所谓位值制，说来平淡无奇。它无非是说，在用十个符号来表达十进制整数时，每个符号依据它在表达式中的不同位置。而有着不同的位值，例如111，这里面的三个同样的1，由于它们的位置不同，而自左至右，分别代表着102 ，10与1三种不同的位值，如果是二进位制，则三个1将分别代表22，2和1三种不同的位值，因而111将相当于10进制中的5。
这个平淡无奇的位值制，却有着意想不到的作用。为了说明这一问题，不妨引用他人的一番评论。
在美国数学史家A.Cajori的著作<<数学符号史（A history of mathematical notations) >>一书的卷1，页70上，曾引述过法国曾当过拿破仑大臣的数学与天文学大师Laplace的一段话。现译之如下，文中的印度与印度人，自然应纠正为中国与中国人。
“从印度人那里，我们学到了用10个字母来表示所有数的聪明办法，这个聪明办法，除了赋予给每个符号以一绝对的值以外，还赋予了一个位置的值，这是一种既精致又重要的想法。这种想法看起来如此简单，而正因为如此简单，我们往往并未能足够认识它的功绩。但是，正由于这一方法的无比简单，以及这一方法对所有计算的无比方便，使得我们的算术系统在所有有用的创造中成为第一流的。至于创造这种方法是多么困难，则只要看看下面的事实就不难理解。这个事实是：这一发明甚至逃过了阿基米德与阿波罗尼斯的天才，而他们是古代两位最伟大的人物。”
平淡无奇的位值制，逃过了阿基米德与阿波罗尼斯的天才，却诞生在古代的中华大地上。
古代的中华民族，就在这平淡无奇的位值制基础上，产生了机械化的四则运算法则，建立起数学大厦，创立了富有特色的东方数学－－－机械化数学。
正与欧几里得<<几何原本>>之成为西方数学公理化演绎体系的经典代表作那样，<<九章算术>>以及公元263年魏刘徽的<<九章注>>,可以视为是东方数学机械化算法体系的经典代表之作。在<<九章>>及其<<注>>中，成果不是表示成定理的形式，而是以术即算法的形式出现。推理与计算的出发点，不是一大批公理，而是根据经验实例等总结而成寥寥可数简单明了的原理。主题也不是几何定理的证明，而是方程的求解。总之，与欧几里得<<几何原本>>相当，<<九章>>及其<<注>>中，汇集了古代东方数学的精髓及其大成，是机械化算法体系的一部传世之作。
与欧几里得几何相反，机械化的中国古代数学，在几何学上根本不考虑定理的证明与发明，而是着重各种问题特别是几何问题的解决。由此提炼成原理法则，进而解决其它更难的问题。这种问题的解决，往往自然导致方程的求解。例如，简单的物物交换问题导致线性联立方程组的解法与负数概念的发现（方程术与正负术）。简单的勾股测量与田亩量度导致出入相补原理与勾股定理以及开平方算法（勾股术与开平方术）。前者相当于西方的Pythageras定理而后者相当于解最简单的二次方程X2 ＝A。大规模工程建设与测高望远又导致三国时代刘徽<<海岛算经>>与唐初王孝通<<辑古算经>>关于三次方程的出现。这条解方程的发展主线到宋元时代达到了高峰。由于历史来源，中国古籍中把现代所称的解方程通称为“开方”。
在解方程的发展过程中，天元概念与天元术的发明是一种飞跃。在数学发展史上其意义之重大是可与位值制的创造相提并论的，这是中华民族在数学上影响深远的又一贡献。
自<<九章>>中的线性联立方程组与二次方程到天元术的出现，我国方程的发展，至少已在1000年以上。但是在此之前，尽管已发展到高次方程能数值求解（增乘开方法，正负开方术），却并没有未知数（即天元等）的概念，建立方程需要非机械化的难以捉摸的种种巧思，只有在方程建立之后，才有种种机械化的算法来解答。天元概念与天元术的出现，使方程的建立也成为机械化的过程，从此变得轻而易举。这是中国式机械化数学的思想与方法像位值制那样化难为易的又一次体现。
天元术起于宋代而发展到元代，已经发现了解高次联立方程组的途径与处理方法。与之相伴又产生了几何代数化方法，以及相当于多项式的表达方式与运算方法及消去法。八五期间攀登项目中解多项式方程组的一个主要方法－－特征列法，即源自元朱世杰<<四元玉鉴>>（1303年）的四元术，即解多至四个未知数的多项式方程组的机械化算法。虽然由于中国当时用筹算，实际上只能解两个未知数（天元与地元）的联立方程组，至多是三个或四个未知数的极其简单的所谓稀疏方程组而已，理论与方法上也有许多缺陷，但其提出的主要思想与途径则是完全正确的。我们所用的特征列法，只是在<<四元玉鉴>>所指出的途径上给以现代化的处理，使之臻于严密合于现代数学的要求而已。
<<四元玉鉴>>中除了解高次联立方程组以及其它许多重要的成就外，还有一项迄今似乎还未有人觉察的意义重大的揭示：把几何定理的证明与发明转化为方程的求解。
中国古算在几何方面着重的是几何问题的求解，而不考虑几何定理的证明，更没有几何公理一类的词汇（参阅本书附录2）。但是几何问题的解决，其答案往往以公式的形式出现，而这些公式，正相当于现在通称的几何定理，由观天测地导致的勾股弦公式与所谓日高公式以及魏刘徽<<海岛算经>>中许多测高望远的公式，即是这样的定理。这些公式（或定理）都是从一些简单易明的原理如出入相补原理（而不是公理系统）推导而来。只是这种推导是非机械化的而需要一定的巧思。然而在朱世杰的<<四元玉鉴>>中，却指出某些古代已知公式（即定理），如果引入天元（即未知数）并建立相应的方程，则通过解方程来解决相应的几何问题，即可自然导致这些公式。
这提供了一条证明与自动发现几何定理的新路：把非机械化的定理求证与发明归结为可以机械化的方程求解。
事实上，我们倡议的数学机械化，就是在遵循我国古时机械化数学的启示，从1976至1977年间开始，把几何代数化，将相应的多项式组进行适当处理，把非机械化的几何定理证明转化为机械化的高次联立方程组的处理，即所谓几何定理的机器证明，由此打开局面，而再逐步走上更一般更深层的数学机械化道路的。
中国的机械化数学，在宋元时期达到高峰。在这有待更高攀登的关键时刻，有望进一步发展到解析几何与微积分之际，却骤然衰退，一落千丈。在中国的大地上，从此为由西方传入的非机械化的欧几里得几何及其公理化体系所代替，直至今日。对于这一段中国式机械化数学在中国大地上盛极而衰的原因，我们将不作分析，而留之于今后的数学史家。
中国式的机械化数学，虽然在中国本土上宋元以来近于销声匿迹，但并未从此消亡，而在欧洲大地上以另一种形式被发扬光大。
古代的欧亚大陆，在帕米尔高原以东的中华大地上，发展了一套机械化算法体系，以<<九章算术>>为代表的东方数学。在黑海、爱琴海，红海以西，则发展了一套公理化演绎体系，以欧几里得<<几何原本>>为代表的西方数学。两者之间隔着一个中亚细亚的波斯，阿拉伯世界，其中米索不达米亚平原上的巴比伦，在远古时期对数学就有光辉的创造。尽管古代交通不便，但也有丝绸之路沟通东西。古时战争频繁，既有波斯的西征希腊，也有亚力山大的东征。此后又有阿拉伯，蒙古、土耳其的大规模西侵与十字军的东征。阿拉伯人甚至还通过北非占领了半个西班牙，并在西班牙建立了具有现代形式的最早的大学，其中就有天文学系，数学自然包括在内。如果说科学、技术、与文化将不随着军队的前进而传播，将是不可思议的。中亚的阿拉伯世界成为东西方数学交流荟萃之地，是在情理之中的。
公元476年时，罗马城陷开始了中世纪时代。这时以欧几里得为标志的公理化几何学，已经衰落。欧洲在数学上经历了一个相当长的黑暗时期。一个转折似乎出现在公元1453年。是年东罗马帝国首都 君士坦丁堡为土耳其攻陷，象征了中世纪时代的结束。君士坦丁堡的大批学者向西流亡，君士坦丁堡的大批藏书，也跟着向西转移。这些书籍中即有古希腊的大量著作，也有大批阿拉伯的译著。其中不少来自东方，当然也有中亚阿拉伯等国自己的创造。在此之前，在十二世纪时欧几里得的几何原本与Al Khowarizmi的著作，都已从阿拉伯文译成拉丁文。可以想见，君士坦丁堡的陷落更促进了欧几里德几何的复活与东方数学的西传。东方数学的影响与作用，从Laplace关于位值制的评论，可以略见一二只是西方史家向来把这些都归之于东方的印度，不仅抹杀阿拉伯世界的贡献，对东方的中国更近于视而不见。对此使人大惑不解的现象，孙克定先生曾经有一句耐人寻味的话：印度是英国的宠儿。
使几何定理的证明也能走上机械化道路的转折点出现在１７世纪的1637年，是Descartes关于几何学的著作问世。此书公认为是座标几何或解析几何的创始之作，现将此书的某些特点略举如下：
１．此书不考虑什么公理、定理与证明，而把几何的重点转为几何问题的求解，这种几何问题有不少来自透镜的设计制造。
２．建立了几何的代数化，使几何问题的求解转化为方程的求解。
３．把几何问题转化为方程所求得的解答，表达成几何的定理，这可视为从方程解答导致定理自动发明的某些原始实例。
４．建立方程正根个数的Descactes符号判别法则。
总之,Descartes的几何学开辟了几何定理证明机械化的道路。我们２０多年来有关几何定理的机器证明与发明不妨认为正是沿着这一道路走下来的。
不难看出，我国古代几何学的发展过程，与Descartes几何学相对照，在方向与方法上正相一致。
从Descartes著作问世到１９世纪以至今日，几何学有着蓬勃的空前发展。仅举其大者。１９世纪中出现了非欧几何、投影几何、直线几何、球几何以及与近世密码学与组合学等应用学科密切相关的有限几何。更重要的是出现了影响到数学整个发展成为２０世纪核心部分的微分几何、代数几何与拓扑学（亦称连续几何）。此外还有以群为标志Klein关于几何学的分类，以及以公理系统为标志的各种“非欧”几何如 Cayley 几何等的分类。在1９世纪之末，又出现了迄今再版至第１２版的Hilbert名著《几何基础》。此书把欧几里得几何奠定于坚实的基础之上，并沟通了欧氏几何公理系统与Deseartes的座标系统，无异于在公理化与机械化之间搭起了一座桥梁。
美妙的几何定理也层出不穷，试举复投影几何中的下述定理为例：
复投影空间的一个三次曲面上，如果只含有限多条直线，则这样的直线恰有２７条。
活跃于整个１９世纪的投影几何，有着无数条美妙的定理。但美国的代数几何学巨匠，现任世界数学会主席的Munford先生，却一概视之为破烂，而对上述２７条直线的定理，则情有独钟，誉之为破烂袋中的宝石。
这一定理叙述简明，但牵涉到的一些概念却极不简单，证明尤其困难，它需要现代代数几何学中一整套艰深的理论与方法。
１７世纪上半世纪解析几何的诞生，促使了下半世纪微积分的出现。与此同时，也出现了以微分方程定义的几何图象的研究，即是早期的微分几何。到１９世纪，更出现了内蕴的微分几何（Gauss)与黎曼几何，成为２０世纪最活跃且影响深远的数学学科之一。
１９世纪与２０世纪之交，法国的Poincar练⒈砹艘幌盗形恼拢?戳⒘送仄搜АＴ谡庑┪恼碌牡谝黄?校琍oincar烈杂梢蛔榻馕龇匠趟?ㄒ宓募负瓮枷螅?魑?芯康亩韵螅?院笥忠??烁春闲蔚母拍睿?鼓持殖潭鹊幕?祷?悸堑靡猿闪ⅲ?哟送仄搜У靡杂蟹稍镜姆⒄梗??褚殉晌?贝??е凶钣杏跋斓难Э浦?弧
页:
[1]