2010级信息与计算科学专业导论

信息与计算科学专业导论

学号 姓名 成绩

数学机械化

一、数学机械化简介

证明定理：古希腊：欧几里德几何学

数学活动

解方程：古代中国数学

二、什么是数学机械化？

所谓机械化，无非是刻板化和规格化。

数学问题的机械化就要求在运算或证明过程中，每前进一步之后，都有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。 数学机械化—从设想到实现

从笛卡尔、莱布尼兹、希尔伯特、塔斯基、王浩、吴文俊等数学家的思想来看一下数学机械化从设想到实现的简要历史。

1．Descartes的设想

首先，把任一问题转化为数学问题

第二, 将任一数学问题转化为代数问题

第三，将任一代数问题转化为单个方程求解

评价： 笛卡尔的计划失败了，但它人不失为一个伟大的计划，

而且即使失败了，它对数学的影响也超过了偶尔获得成功的千万

个计划。

2．Leibniz之梦

德国数学家 Leibniz 曾有过“推理机器”的设想。他研究过逻

辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言

和造一台通用机器的构想。

他的努力促进了 Boole 代数、数理逻辑以及计算机科学的研

究，正是沿着这一方向，经后人的努力，形成了机器定理证明的

逻辑方法。

3．Hilbert的《几何基础》

Hilbert在《几何基础》中提出了从公理化走向机械化的数学

构想。Hilbert计划将数学知识纳入严格的公理体系中，并着力在

公理化基础上寻找机械化的方法判定命题是否成立。

在书中就提供了一条可以对一类几何命题进行判定的定理

— 当然，在那个时代，不仅 Hilbert 本人，整个数学界都没有意

识到这一点。

4. Tarski的定理

波兰数学家 Tarski 在 1950 年推广了关于代数方程实根数

目的 Sturm 法则，由此证明了一个引人注目的定理：“一切初等

几何和初等代数范围的命题，都可以用机械方法判定。”

Tarski得出的结论给定理证明机械化的研究带来了曙光。可

惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定

理。

5．王浩的定理机器证明程序

1959 年，王浩设计了一个程序，用计算机证明了 Russell 、

Whitehead 的巨著《数学原理》中的几百条有关命题逻辑的定理，

仅用了 9 分钟。王浩工作的意义在于宣告了用计算机进行定理证

明的可能性。

6．吴方法的产生

1977 年，吴文俊在《中国科学》上发表论文《初等几何判定

问题与机械化问题》。 1984年，吴文俊出版学术专著《几何定理

机器证明的基本原理》。这部专著着重阐明几何定理机械化证明的

基本原理，与国际上流行的代数理想论不同，明确提出了具有中

国自己特色的、以多项式零点集为基本点的机械化方法。自此，“吴

方法”宣告诞生，数学机械化研究揭开了新的一幕。

吴方法遵循中国传统数学中几何代数化的思想，首次实现了

高效的几何定理自动证明，显现了无比的优越性。他的工作被称

为自动推理领域的先驱性工作，并于1997年获

“Herbrand自动推理杰出成就奖”。

在授奖辞中对他的工作给了这样的评价:

“几何定理自动证明首先由赫伯特·格兰特于50年代开始研究。虽

然得到一些有意义的结果，但在吴方法出现之前的20年里，这一

领域进展甚微。在不多的自动推理领域中，这种被动局面是由一

个人完全扭转的。吴文俊很明显是这样一个人。他将几何定理证

明从一个不太成功的领域变为最成功的领域之一。”

三、数学机械化或机器证明方面：从初等几何着手，在计算机上证明了一类高难

度的定理，同时也发现了一些新定理，进一步探讨了微分几何的定理证明。提出了利用机器证明与发现几何定理的新方法。这项工作为数学研究开辟了一个新的领域，将对数学的革命产生深远的影响。1978年获全国科学大会重大科技成果奖。

四、中国数学史方面：吴文俊认为中国古代数学的特点是：从实际问题出发，经

过分析提高，再抽象出一般的原理、原则和方法，最终达到解决一大类问题的目的。他对中国古代数学在数论、代数、几何等方面的成就也提出了精辟的见解。

五、主要参考书目

1. 数学机械化，吴文俊著，科学出版社，2003

2. 方程求解与机器证明，高小山等，科学出版社，2003

六、主要软件

1.（数学机械化平台) http://www.77cn.com.cn/mmp

2. DISCOVERER http://www.77cn.com.cn/~xbc/software.html