从吴文俊和吴方法谈起

《从吴文俊和吴方法谈起》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、从吴文俊和吴方法谈起－数学机械化的观点数学文化课程组李军1吴文俊中国科学院院士第三世界科学院院士首届国家最高科技奖国家第一届自然科学奖最高奖一等奖自动推理的最高奖Herbrand奖2006邵逸夫数学奖2最近，著名数学家吴文俊荣获邵逸夫数学科学奖。邵逸夫数学科学奖是一项国际性大奖，它的评委是来自国际数学界的知名权威。吴文俊说：这次邵逸夫奖的评委都是国际上有影响的大家，他们宣布我获得邵逸夫奖，是因为我的数学机械化问题的研究，这实际上是国际数学界对数学机械化研究的承认与肯定，它比奖金重要得多。数学机械化得到国际数学界承认3中央电视台《大家》栏

2、目：《吴文俊·我的不等式》片断4什么是数学机械化所谓机械化，无非是刻板化和规格化。数学问题的机械化，就要求在运算或证明过程中，每前进一步之后，都有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。使用一种机械化方法证明一类定理，才真正体现了机械化定理证明。1977年，吴文俊给出了初等几何一类主要定理的机械化证明方法－“吴方法”。5数学机械化：从设想到实现笛卡尔莱布尼茨希尔伯特6数学机械化：从设想到实现哥德尔塔斯基王浩吴文俊7笛卡尔的设想17世纪法国的数学家Descartes曾有过一个伟大的设想：“一切问题化

3、为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。”Descartes把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是全部科学的机械化。因为代数方程求解是可以机械化的。但Descartes没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座桥梁，实现了初等几何问题的代数化。8莱布尼兹之梦德国数学家Leibniz曾有过“推理机器”的设想。他研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言和造一台通用机器的构想。他的努力促进了Boole代数、数理逻辑以及计算机科学

4、的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。9希尔伯特的构想Hilbert在《几何基础》中提出了从公理化走向机械化的数学构想。Hilbert计划将数学知识纳入严格的公理体系中，并着力在公理化基础上寻找机械化的方法判定命题是否成立。Hilbert同时指出，定理的判定问题应当是分类解决的，解决方法要同时强调简单性和严格性。在Hilbert的名著《几何基础》一书中就提供了一条可以对一类几何命题进行判定的定理—当然，在那个时代，不仅Hilbert本人，整个数学界都没有意识到这一点。10哥德尔的著名结果Gödel著名的不

5、完全性定理指出一个不弱于初等数论的形式系统如果是无矛盾的，则是不完全的，即存在形式系统的一个命题，它和它的否定都不能由形式系统证明。因此，Hilbert的要求太高了。上述的Gödel不完全性定理断言：即使在初等数论的范围内，对所有命题进行判定的机械化方法也是不存在的！11塔斯基的判定法波兰数学家Tarski在1950年推广了关于代数方程实根数目的Sturm法则，由此证明了一个引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械方法判定。”Tarski得出的结论给定理证明机械化的研究带来了曙光。可惜他的方法太复杂，即使用高速计

6、算机也证明不了稍难的几何定理。12王浩：迈向数学机械化1959年，王浩设计了一个程序，用计算机证明了Russell、Whitehead的巨著《数学原理》中的几百条有关命题逻辑的定理，仅用了9分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。在1960年的《IBM研究与发展年报》（IBMJournal），王浩发表了《迈向数学机械化》（TowardMechanicalMathematics），“数学机械化”一词即出自此处。13吴文俊：机器证明领域的新的一页1977年，吴文俊在《中国科学》上发表论文《初等几何判定问题与机械化问题》。

7、1984年，吴文俊的学术专著《几何定理机器证明的基本原理》由科学出版社出版，这部专著着重阐明几何定理机械化证明的基本原理。1985年，吴文俊的论文《关于代数方程组的零点》发表，具体讨论了多项式方程组所确定的零点集。与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的机械化方法。自此，“吴方法”宣告诞生，数学机械化研究揭开了新的一幕。14《吴文俊·我的不等式》片断15三角形三条高线交于一点的代数证明D是BC和CA上高线交点16定理的假设部分是,由吴方法，可得非退化条件是.定理的结论是CO经过D点.显然在非退

8、化条件下定理成立。17Morley定理任意三角形中，一个角的三等分线，与和它相邻的角的三等分线相交，交点组成正三角形。18机器方法容易证明Morley定理任意三角形中，一个角的三等分线，与和它相邻的角的三等