三年级数学电子课本数学机械化：回顾与展望 .doc

2020年11月16日发(作者：计文波)
数学机械化：回顾与展望


谢谢观赏
数学机械化这一 名词取自数理逻辑学家王浩先生的著作。王浩先生毕生从事数理
逻辑的研究，不仅是一位倡导用计算机来 证明逻辑命题的先驱者，而且还身体力行。
1958年时，王浩设计了几个计算机程序，使用当时的IB M704机，在3分钟内，自动证明
了Russell与Whitehead的名 著“数学原理”一书中的220条命题，稍后又扩展到400
条。这一成就震动了学术界，被誉为“一 击落七蝇（Seven flies in one blow)”。
王浩先生还因此而于1983年获 得人工智能国际联合会与美国数学会联合颁发的里程碑
奖（Milestone Prize)。
王浩先生关于数理逻辑的文章，曾收集编写成<<数理逻辑总览(A Survey of
Mathematical Logic)>>一书，于1959年由科学出版社出版，以下简称<<总 览>>。书中
的第9章，原来发表于1960年的IBM研究与发展年报。章名“向机械化数学前进(T oward
Mechanical Mathematics)”，我们所采用的数学机械化一词，即出自此处。
该章第一节引论 中，一开头即将计算与证明作一比较，指出两者有四大不同之
处。简言之，如果用我们现在的词汇来说， 计算是机械化的，而所谓证明则否。在本
章中，王浩先生把数理逻辑的最基础部分（命题逻辑）的定理证 明成功地归结为机械
化的步骤，得以用机器获得自动的证明。在本章以及<<总览>>的其它诸章中，王 浩先
生还多处提出了在数学推行这种机械化证法的想法，使数学成为机械化的数学。
上面只谈了数学机械化一词的来历，至于它的实质意义，我想不必下什么艰深的
学院式严格定义，只想请 读者们回忆一下在中小学求学时学习数学的过程。在小学
时，加减乘除与开方等运算都是按部就班依照一 定的法则机械地进行的。但是像解鸡
兔共笼一类所谓四则难题，就无法可循而需运用巧思。到初中一二年 级学习代数，用
各种消去法解线性联立方程组时，又像四则运算那样，可以依一定法则机械地逐步进行以至求出解答。但到学习几何时，就又像四则难题那样，证起定理来往往无所措
手，需要高度的巧 思。两种问题两种风格，其难易之别甚为显然，其关键就是其一是
机械化的，而另一则否。是否能化难为 易，以及如何才能化难为易，也就是如何把原
来非机械化因而极为困难的数学问题变成机械化而容易起来 ，乃是数学机械化的主题
思想，也是它的主要目标。
一个依据一定法则可以按部就班 ，机械地进行的方法在现代通称为算法。在当前
的计算机时代，有算法即可编为程序，而在计算机上实施 ，因此当代的计算机科学大
师Knuth，曾说计算机科学即是算法的科学。
中国数 学源远流长，远古的数学成就，总结于<<九章算术>>一书，依据现存资料
与地下文物，<<九章>> 的成书年代，可大致定在公元前二，三世纪，其中成果大都以
算法的形式出现。例如开平方的算法，在< <九章>>中称为开平立方术。对于鸡兔共笼
一类问题，可用盈不足术来解答。更一般的问题，则有方程 术与正负术，实质上即是
谢谢观赏
谢谢观赏
解线性联立方程组的消去法与移项法则 。在几何方面，中国根本不考虑定理与证明，
而重在几何问题的解决。例如 田亩丈量与勾股测量一类问 题，导致开平方术，相当于
解最简单的二次方程。从<<九章>>以至历代的数学著作，其中成果大都以 术的形式来
表达。
总之，中国的传统数学，由求解几何问题以及其它各种类型问题所 导致的方程求
解成为古算发展的一条主线。解决问题的方法又往往以术亦即算法的形式出现，因而
中国的传统数学，实质上是Knuth意义下的一种没有计算机的计算机科学，也正是王浩
先生意义下 的一种机械化数学。
中国传统数学通过化几何问题求解为方程求解而走上了一条机械化的道路 。对于
西方传统几何定理的证明以及其它种种数学领域中的定理证明，形式上与机械化格格
不入 ，是否也可以找到 一条道路，使证明也成为机械化的呢。
中国传统的机械化数学，对此提供了入手的线索。
数学机械化之出现于古代中国，决非偶然。 这里面有一层通常不为人所察觉更不
易为人理解的深刻原因－－记数位值制的发明。
人人都知道记数的进位制，我们通常用的是十进位制。一个正整数不论多大，都
可用相当于从0，1，到 9的十个数字或符号甚或实物来表示。现代的计算机则用二进制
来表示整数，这时只要用可以表示0与1 的某种器件就行了。在技术上容易实现的二进
制与人们习惯使用的十进制之间的转换，则用所谓译码器来 实现。世界各古代民族，
往往有着不同的进位制。例如古巴比伦用六十进位制，古希腊与埃及用十进位制 ，中
美洲的玛雅民族则用二十进位制。然而，所有这些古代民族的进位制，都是不完全
的，更谈 不上意义重大的位值制了。
位值制是中华民族的创造，是世界上独一无二的独特创造。
所谓位值制，说来平淡无奇。它无非是说，在用十个符号来表达十进制整数时，
每个符 号依据它在表达式中的不同位置。而有着不同的位值，例如111，这里面的三个
同样的1，由于它们的 位置不同，而自左至右，分别代表着10
2
，10与1三种不同的位
值，如果是二进 位制，则三个1将分别代表2
2
，2和1三种不同的位值，因而111将相当于
10进 制中的5。
这个平淡无奇的位值制，却有着意想不到的作用。为了说明这一问题，不妨引用
他人的一番评论。
在美国数学史家的著作<<数学符号史（A history of mathematical
notations) >>一书的卷1，页70上，曾引述过法国曾当过拿破仑大臣的数学与天文学< br>大师Laplace的一段话。现译之如下，文中的印度与印度人，自然应纠正为中国与中国
人。
“从印度人那里，我们学到了用10个字母来表示所有数的聪明办法，这个聪明办
法， 除了赋予给每个符号以一绝对的值以外，还赋予了一个位置的值，这是一种既精
致又重要的想法。这种想 法看起来如此简单，而正因为如此简单，我们往往并未能足
谢谢观赏
谢谢观赏
够认 识它的功绩。但是，正由于这一方法的无比简单，以及这一方法对所有计算的无
比方便，使得我们的算术 系统在所有有用的创造中成为第一流的。至于创造这种方法
是多么困难，则只要看看下面的事实就不难理 解。这个事实是：这一发明甚至逃过了
阿基米德与阿波罗尼斯的天才，而他们是古代两位最伟大的人物。 ”
平淡无奇的位值制，逃过了阿基米德与阿波罗尼斯的天才，却诞生在古代的中华
大地上。
古代的中华民族，就在这平淡无奇的位值制基础上，产生了机械化的四则运算法
则，建立起数学大厦，创 立了富有特色的东方数学－－－机械化数学。
正与欧几里得<<几何原本>>之成为西方数学 公理化演绎体系的经典代表作那样，
<<九章算术>>以及公元263年魏刘徽的<<九章注>>,可以 视为是东方数学机械化算法体
系的经典代表之作。在<<九章>>及其<<注>>中，成果不是表示成定 理的形式，而是以
术即算法的形式出现。推理与计算的出发点，不是一大批公理，而是根据经验实例等< br>总结而成寥寥可数简单明了的原理。主题也不是几何定理的证明，而是方程的求解。
总之，与欧几 里得<<几何原本>>相当，<<九章>>及其<<注>>中，汇集了古代东方数学
的精髓及其大成，是 机械化算法体系的一部传世之作。
与欧几里得几何相反，机械化的中国古代数学，在几何学上 根本不考虑定理的证
明与发明，而是着重各种问题特别是几何问题的解决。由此提炼成原理法则，进而解
决其它更难的问题。这种问题的解决，往往自然导致方程的求解。例如，简单的物物
交换问题导 致线性联立方程组的解法与负数概念的发现（方程术与正负术）。简单的
勾股测量与田亩量度导致出入相 补原理与勾股定理以及开平方算法（勾股术与开平方
术）。前者相当于西方的Pythageras定理 而后者相当于解最简单的二次方程X
2
＝A。大
规模工程建设与测高望远又导致三国 时代刘徽<<海岛算经>>与唐初王孝通<<辑古算
经>>关于三次方程的出现。这条解方程的发展主线 到宋元时代达到了高峰。由于历史
来源，中国古籍中把现代所称的解方程通称为“开方”。
在解方程的发展过程中，天元概念与天元术的发明是一种飞跃。在数学发展史上
其意义之重大是可与位值 制的创造相提并论的，这是中华民族在数学上影响深远的又
一贡献。
自<<九章>> 中的线性联立方程组与二次方程到天元术的出现，我国方程的发展，
至少已在1000年以上。但是在此 之前，尽管已发展到高次方程能数值求解（增乘开方
法，正负开方术），却并没有未知数（即天元等）的 概念，建立方程需要非机械化的
难以捉摸的种种巧思，只有在方程建立之后，才有种种机械化的算法来解 答。天元概
念与天元术的出现，使方程的建立也成为机械化的过程，从此变得轻而易举。这是中
国式机械化数学的思想与方法像位值制那样化难为易的又一次体现。
天元术起于宋代而发展到 元代，已经发现了解高次联立方程组的途径与处理方
法。与之相伴又产生了几何代数化方法，以及相当于 多项式的表达方式与运算方法及
消去法。八五期间攀登项目中解多项式方程组的一个主要方法－－特征列 法，即源自
元朱世杰<<四元玉鉴>>（1303年）的四元术，即解多至四个未知数的多项式方程组的
谢谢观赏
谢谢观赏
机械化算法。虽然由于中国当时用筹算，实际上只能解两个未知 数（天元与地元）的
联立方程组，至多是三个或四个未知数的极其简单的所谓稀疏方程组而已，理论与方
法上也有许多缺陷，但其提出的主要思想与途径则是完全正确的。我们所用的特征列
法，只是在 <<四元玉鉴>>所指出的途径上给以现代化的处理，使之臻于严密合于现代
数学的要求而已。
<<四元玉鉴>>中除了解高次联立方程组以及其它许多重要的成就外，还有一项迄
今 似乎还未有人觉察的意义重大的揭示：把几何定理的证明与发明转化为方程的求
解。
中国古算在几何方面着重的是几何问题的求解，而不考虑几何定理的证明，更没
有几何公理一类的词汇（ 参阅本书附录2）。但是几何问题的解决，其答案往往以公式
的形式出现，而这些公式，正相当于现在通 称的几何定理，由观天测地导致的勾股弦
公式与所谓日高公式以及魏刘徽<<海岛算经>>中许多测高望 远的公式，即是这样的定
理。这些公式（或定理）都是从一些简单易明的原理如出入相补原理（而不是公 理系
统）推导而来。只是这种推导是非机械化的而需要一定的巧思。然而在朱世杰的<<四
元玉 鉴>>中，却指出某些古代已知公式（即定理），如果引入天元（即未知数）并建
立相应的方程，则通过 解方程来解决相应的几何问题，即可自然导致这些公式。
这提供了一条证明与自动发现几何定 理的新路：把非机械化的定理求证与发明归
结为可以机械化的方程求解。
事实上，我 们倡议的数学机械化，就是在遵循我国古时机械化数学的启示，从
1976至1977年间开始，把几何 代数化，将相应的多项式组进行适当处理，把非机械化
的几何定理证明转化为机械化的高次联立方程组的 处理，即所谓几何定理的机器证
明，由此打开局面，而再逐步走上更一般更深层的数学机械化道路的。
中国的机械化数学，在宋元时期达到高峰。在这有待更高攀登的关键时刻，有望
进一步 发展到解析几何与微积分之际，却骤然衰退，一落千丈。在中国的大地上，从
此为由西方传入的非机械化 的欧几里得几何及其公理化体系所代替，直至今日。对于
这一段中国式机械化数学在中国大地上盛极而衰 的原因，我们将不作分析，而留之于
今后的数学史家。
中国式的机械化数学，虽然在 中国本土上宋元以来近于销声匿迹，但并未从此消
亡，而在欧洲大地上以另一种形式被发扬光大。
古代的欧亚大陆，在帕米尔高原以东的中华大地上，发展了一套机械化算法体
系，以< <九章算术>>为代表的东方数学。在黑海、爱琴海，红海以西，则发展了一套
公理化演绎体系，以欧几 里得<<几何原本>>为代表的西方数学。两者之间隔着一个中
亚细亚的波斯，阿拉伯世界，其中米索不 达米亚平原上的巴比伦，在远古时期对数学
就有光辉的创造。尽管古代交通不便，但也有丝绸之路沟通东 西。古时战争频繁，既
有波斯的西征希腊，也有亚力山大的东征。此后又有阿拉伯，蒙古、土耳其的大规 模
西侵与十字军的东征。阿拉伯人甚至还通过北非占领了半个西班牙，并在西班牙建立
了具有现 代形式的最早的大学，其中就有天文学系，数学自然包括在内。如果说科
谢谢观赏
谢谢观赏
学、技术、与文化将不随着军队的前进而传播，将是不可思议的。中亚的阿拉伯世界
成为东西方 数学交流荟萃之地，是在情理之中的。
公元476年时，罗马城陷开始了中世纪时代。这时以 欧几里得为标志的公理化几何
学，已经衰落。欧洲在数学上经历了一个相当长的黑暗时期。一个转折似乎 出现在公
元1453年。是年东罗马帝国首都 君士坦丁堡为土耳其攻陷，象征了中世纪时代的结
束。君士坦丁堡的大批学者向西流亡，君士坦丁堡的大批藏书，也跟着向西转移。这
些书籍中即有古希 腊的大量著作，也有大批阿拉伯的译著。其中不少来自东方，当然
也有中亚阿拉伯等国自己的创造。在此 之前，在十二世纪时欧几里得的几何原本与Al
Khowarizmi的著作，都已从阿拉伯文译成拉 丁文。可以想见，君士坦丁堡的陷落更促
进了欧几里德几何的复活与东方数学的西传。东方数学的影响与 作用，从Laplace关于
位值制的评论，可以略见一二只是西方史家向来把这些都归之于东方的印度 ，不仅抹
杀阿拉伯世界的贡献，对东方的中国更近于视而不见。对此使人大惑不解的现象，孙
克 定先生曾经有一句耐人寻味的话：印度是英国的宠儿。
使几何定理的证明也能走上机械化道路 的转折点出现在１７世纪的１６３７年，
是年Descartes关于几何学的著作问世。此书公认为是 座标几何或解析几何的创始之
作，现将此书的某些特点略举如下：
１．此书不考虑什 么公理、定理与证明，而把几何的重点转为几何问题的求解，
这种几何问题有不少来自透镜的设计制造。
２．建立了几何的代数化，使几何问题的求解转化为方程的求解。
３．把几 何问题转化为方程所求得的解答，表达成几何的定理，这可视为从方程
解答导致定理自动发明的某些原始 实例。
４．建立方程正根个数的Descactes符号判别法则。
总之 ,Descartes的几何学开辟了几何定理证明机械化的道路。我们２０多年来有
关几何定理的机器 证明与发明不妨认为正是沿着这一道路走下来的。
不难看出，我国古代几何学的发展过程，与 Descartes几何学相对照，在方向与方
法上正相一致。
从Descarte s著作问世到１９世纪以至今日，几何学有着蓬勃的空前发展。仅举其
大者。１９世纪中出现了非欧几何 、投影几何、直线几何、球几何以及与近世密码学
与组合学等应用学科密切相关的有限几何。更重要的是 出现了影响到数学整个发展成
为２０世纪核心部分的微分几何、代数几何与拓扑学（亦称连续几何）。此 外还有以
群为标志Klein关于几何学的分类，以及以公理系统为标志的各种“非欧”几何如
Cayley 几何等的分类。在1９世纪之末，又出现了迄今再版至第１２版的Hilbert名著< br>《几何基础》。此书把欧几里得几何奠定于坚实的基础之上，并沟通了欧氏几何公理
系统与Des eartes的座标系统，无异于在公理化与机械化之间搭起了一座桥梁。
美妙的几何定理也层出不穷，试举复投影几何中的下述定理为例：
谢谢观赏
谢谢观赏
复投影空间的一个三次曲面上，如果只含有限多条直线，则这样的直线恰有２７
条。
活跃于整个１９世纪的投影几何，有着无数条美妙的定理。但美国的代数几何学
巨匠， 现任世界数学会主席的Munford先生，却一概视之为破烂，而对上述２７条直线
的定理，则情有独 钟，誉之为破烂袋中的宝石。
这一定理叙述简明，但牵涉到的一些概念却极不简单，证明尤其 困难，它需要现
代代数几何学中一整套艰深的理论与方法。
１７世纪上半世纪解析几 何的诞生，促使了下半世纪微积分的出现。与此同时，
也出现了以微分方程定义的几何图象的研究，即是 早期的微分几何。到１９世纪，更
出现了内蕴的微分几何（Gauss)与黎曼几何，成为２０世纪最活 跃且影响深远的数学
学科之一。
１９世纪与２０世纪之交，法国的Poincar发 表了一系列文章，创立了拓扑学。
在这些文章的第一篇中，Poincar以由一组解析方程所定义的几 何图象，作为研究的
对象，稍后又引进了复合形的概念，使某种程度的机械化考虑得以成立，从此拓扑学
得以有飞跃的发展，迄今已成为当代数学中最有影响的学科之一。
诸如代数几何、微分几何与拓扑学与数学机械化的关系与展望，由于说来话长，
在此不作深论。
不仅是这些现代最活跃的几何学，即使是最古老最初等的欧几里得几何，在１９
世纪中 也并不寂寞。即使是一个小小的三角形，除了本书中所提到九点圆Feuerbach定
理和Morle y定理等外，还有着Brocard点以及与之相关的七点圆等，可谓美不胜收。初
等几何以其定理的简 单易懂与证明的曲折直观却又难以捉摸而具有无比的魅力，吸引
着无数的爱好者。类似的几何定理与其不 用座标的证明方式，往往统称为综合几何与
综合证法，以区别于解析几何及其代数化的证法。直到今天， 美妙的综合几何定理还
不时出现。除了本书中已经提到的如Thbault-Taylor-周咸青定理 ，金字塔定理（国
外有数学家称之为北京定理）以及非欧几何的许多定理之外，不妨再举两例。
美国代数学家e对拓扑学有过重大贡献，从他的工作中曾提炼出下面的一
个问题。
设平面上有八个互不相同的点，将这八个点巡回记为A
1
,A
2,...A
8
,而A
9
=A
1
等。每两
个相继 的点A
i
,A
i+1
及隔一个的点A
i+3
构成一三点组, 这样的三点组共有8组。假设每一组的
三点都在一直线上，并称这时的８个点构成8
3
点组。问题是8
3
点组的8个点是否必须在
一直线上。
我们的方法给 出了答案，如果平面是实的，则结论是对的，即８个点必须在一直线
上。但若平面是复的，则结论是否定 的，而且可以给出所有可能8个点不在一直线上的
8
3
点组来。我们的方法还可以讨论 ８点中某些点可以重合的那种所谓退化的情况。
匈牙利的著名数学家Erds，曾得过Wol f奖。有一个来源于Erds的问题：假设
平面上有５个点A
1
...,A
5
, 将这５个点两两相连可得１０条直线.在每一条连线A
i
A
j
上 任
谢谢观赏
谢谢观赏
取一点B
ij
, 这样从给定的５点Ai
(i=1,...5)所得的１０点组B
ij
(i,j=1,...5; i< j)显然
有无穷多个。Erds的问题是反过来如果任给１０个点B
ij
(i,j=1 ,...5;i以找到５个点A
i
(i=1,...,5),使每一 B
ij
恰在连线A
i
A
j
上。
Erds的问题难倒了许多数学家，我们的方法证明了在一般情形下只能有有限多
个５点组 A
i
符合条件。并进一步证明了此数是６，这基本上解决了Erds问题。
几何作图也是一类诱人的问题，在１９世纪中叶得到充分的关注。除了通常的规
尺作图外，１９世纪的几 何学家，还阐发了只用直尺或只用圆规之类的作图理论与作
图方法。在古希腊时代，就有求作一圆与三圆 相切的Appolonius问题以及所谓几何三
大问题。１９世纪又出现了所谓求作三圆彼此相切且各 与三角形的两边相切的
Malfatti问题，更重要的是给出了可以规尺作图的充要条件。例如App olonius问题可
以用规尺作出，而Malfatti问题则否。Gauss更据以证明可以规尺作 图的所有可能的正
多边形，特别指出正 １７边形可以用规尺作出，这一出人意表的成果使年轻的Gau ss
决定献身数学。在近代，也有源自著名数学家Zassenhaus与Van der Waerd en的一个问
题。已知一个三角形的三条边，就可作出它的内外分角线来。反过来，知道三角形的
内外分角线的三条，是否可以作出相应的三角形来，就很不简单，但运用上述判准，
却可以得到完全的 解决，即一般说来光用规尺是不可能的。
像以上这些形形色色美妙有趣的定理相信还会层出不穷。
这样的定理，如果用通常的综合几何的方法来证，显然将是多而少功，难见其成
的，甚至是无从入手的。
诸如此类来源各别性质各异的几何定理与几何问题，都已被我们一视同仁，通过
座标与 方程组，用统一的方法使用计算机这一新型的工具或是证明或是解决。这个统
一的方法，正是遵循我古代 实质上是机械化的数学，从鸡兔共笼到盈不足术，到方程
术又到天元术，导致几何的代数化，以及Des cartes系统化了的通过座标转为方程求解
这样一条机械化的道路所发展起来的。
上面把几何定理与几何问题的求证求解，通过座标的引入化为方程组的问题，这
里的方程组是指多项式方 程组。正是通过对多项式方程组机械化解法的研究，才能获
得以上列举种种各别的综合几何上的应用。这 一方法还已被应用于与实际应用有密切
关系的有限几何，而且还已尝试用于谓词逻辑的命题证明，取得了 与数理逻辑学家们
用多种方法所得可以相当的成果（王浩先生的方法局限于最简单的命题逻辑）。此外，我们还发展了多种新颖的几何定理证明方法：应用Clifford代数的内涵证法，例
证法， 以及可读证法等，在理论上，我们又发展了方程判别系统与构造性代数几何。
不仅如此，来自 各门自然科学、工程技术，以及数学本身的形形色色问题，往往
导致到各种形式的方程，特别是多项式方 程组。我们解多项式方程组的一般方法，也
因之而可应用之于科学技术中多种多样的具体问题，因之而在 八五期间，取得了不少
具体成果。例如：理论物理中的杨-Baxter方程与杨-Mills方程，非 线性偏微分发展方
程的行波解与孤立子解，平面常微分方程的极限环与有关问题，优化与极值问题，机< br>械构造问题，四连杆设计问题，曲面造型问题，计算机视觉与小波问题等，种种应用
谢谢观赏
谢谢观赏
还正方兴未艾，不及备述。
与以上相反，通常证明几何定理的综 合几何方法，尽管直观生动，其使用范围却
是颇为有限的。它一般说来只能占据中学教育的一隅之地，对 于现代数学的影响与推
动可以说微乎其微。前举现代最活跃的两个几何学领域，微分几何与代数几何，尽 管
有着直观的背景，它们最基本的几何对象，都是通过座标与方程来表达的，虽然方程
可以是超 出通常的多项式方程组之外。
甚至是在中学几何教育的一隅之地，传统的综合几何方法，往往 只限于点，线，
圆，三角形等几何对象，像极其重要而其简单程度仅次于圆的圆锥曲线，其性质讨论古希腊时代需要难以卒读的鸿篇巨著，而在现代中学教育的解析几何部分，却只须寥
寥数页，即已精 义殆尽。自然，综合几何的方法，有关的训练在中学教育中当然是必
不可少的。如何将综合几何与解析几 何两种方法在中学教育中得到平衡协调的处理，
是一个需要严肃对待的问题。由于中学教育对于子孙后代 影响深远，必须慎重处理，
决不能草率从事。在这方面，富有教学经验又有一定程度现代数学训练的中学 数学老
师们，应该有最大的发言权。近日得知，美国的科学家与教育家们已经提出了21世纪
几 何学万岁的口号，指出21世纪的教育应当把几何学放在头等重要的地位。这一新情
况值得我国科学家与 教育学家们的深切关注。
正是由于以上种种原因，我们八五期间的攀登项目，实质上以解多项 式方程组及
其应用为核心内容，几何定理的机器证明，只是其应用之一而已。只是为了容易为人
们接受的缘故，才把八五的项目取名为<<机器证明及其应用>>。至于八五期间所取得
的许多具体成果 ，则除前面已提到者外，可以参阅本书以及有关著作，不妄枚举。
另一方面，数学的各个领域 ，都有自身的定理求证与方程求解，决不只是限于各
种几何。机械化方法所导致的方程，也可以形形色色 ，多项式方程只是其中最为简单
而较易入手的方程而已。对微分几何的定理证明，相应的将是一种微分代 数方程组，
即其一例。数论的不定方程，则是不必通过座标的又一实例。
数学的机械 化，虽然在国外的数学论著中，未见有明白的论述，但仍若隐若现不
时以不同的方式出现。例如1900 年Hilbert著名的23个数学问题中，其中第10个问题，
用本书的词汇来表达，将是：是否有一 机械化算法，可以求得一切不定方程组的整数
解或判断其无整数解。这一问题在1970年获得了圆满的 解决，答案是否定的。但数理
逻辑学家们旋即指出：许多著名的数学难题，其能否解决都由某一相应的不 定方程是
否有正整数解来决定，这些数学难题包括Fermat大问题，Goldbach问题，四色问 题，
Riemann猜测等，虽然并不包括所有的数学难题，但对于包括在内的难题，则相应的不
定方程可以取为不高于3次。顺便一提，对于一次以及某些特殊形式的二次不定方程，
其机械化求整数 解的算法，早已为古代中国与印度的数学家所给出，古印度的贡献尤
为特出。对于一般的二次不定方程， 则曾得Wolf奖的德国数学家Siegel也已给出了求
整数解的机械化算法。
试 再举本人比较熟悉的代数拓扑学为例。早在1959年，美国就有位拓扑学家对
某种类型的拓扑空间提出 一种机械化的方法，只是由于过于复杂而无以为继几成绝
谢谢观赏
谢谢观赏
响。7 0年代时，本人对于某种特殊空间在特殊性质范围内给出了机械化方法，只是由
于过于特殊而影响不大。 两者类似于初等几何范围内包罗虽广，但效率太低的Tarski
机械化定理。与效率虽高但内容不多的 Hillert机械化定理。总之，数学的各个领域，
都有它自身的发展规律与发展模式，都有着自己的 定理求证与问题求解。对于一个特
定的定理范围或问题范围，过大则机械化证明或解答的算法可以根本不 存在，过小则
即使有机械化的算法，也可以缺少数学内涵，而意义不大。这样的例子在数学中不胜
枚举。如何在不同的数学领域，找到这样一种既足够大因而包含丰富的数学内涵又足
够小不致于不可能 有机械化算法，乃是数学家们在走上机械化道路应该面对的严肃课
题。
数学的机械化，是 一条看不见尽头的漫长道路，八五期间之局限于初等几何定理
求证与多项式方程组求解，只是一个起步。 我们希望在九五期间，能跳出这个框框，
在项目已正名为数学机械化的情形下，能对数学机械化的事业有 更深层次的推进。

谢谢观赏