我国近现代数学的一项突出成就――数学机械化

开篇：润墨网以专业的文秘视角，为您筛选了一篇我国近现代数学的一项突出成就――数学机械化范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！

中国近现代数学在世界处于什么地位呢？一些人叹息中国数学落后于国外，甚至夸大其词。事实上，我国近现代数学工作者在一些方面已经作出了突出成就，吴文俊院士和他的数学机械化研究就是其中的杰出代表. 2000年，吴文俊院士获得首届国家最高科学技术奖. 2006年，他获得了被媒体誉为“21世纪东方诺贝尔奖”的香港邵逸夫数学科学奖. 两次获奖理由都是因为他对数学机械化这一新兴交叉学科作出开创性的贡献.

1 什么是数学机械化

“所谓数学机械化，其思想实质在于以构造性与算法化的方式从事数学研究，是数学的推理过程机械化以至自动化，以尽量减少聪明才智的要求，并由此减轻艰难的重脑力劳动. ”[1]数学机械化主要有两个特点：算法化，它遵循了一定的操作规则和程序；刻板化，所有的程序步骤都是据一定的法则按部就班地进行，不存在跳跃性.

数学机械化的思想在中小学数学学习中就已有体现. 比如，加减乘除四则运算、开方运算、幂的运算、绝对值运算、方程和方程组求解、不等式和不等式组求解等等，这些都是按部就班地依照一定的法则机械化进行的，蕴涵一定的数学机械化思想方法.

诚如吴文俊所言，“数学机械化”这一名词最早取自美国洛克菲勒大学数理逻辑家王浩先生的著作《向机械化数学前进》(Woward Mechanical Mathematics).

2 国外数学家的早期工作

早在17世纪时，法国数学家笛卡儿(Descartes)和德国数学家莱布尼兹(Leibnize)就已经产生了数学机械化思想萌芽. 笛卡儿的解析几何学即是努力建立几何的代数化，把几何问题的求解通过引入坐标转化成代数方程的求解，从而开辟了几何定理证明机械化的道路. 莱布尼兹设计了最原始的乘法计算器，并设想研制出推理机器，自动检验数学命题的正确性. 19世纪末，德国数学家希尔伯特(Hilbert)等人创立并发展了数理逻辑，至此，数学证明机械化思想初步形成. 对于希尔伯特的著作《几何基础》，吴文俊认为[1]，“该书更重要处，是在于提供了一条从公理化出发，通过代数化以到达机械化的道路. ”而此时，数学机械化思想还仅是一种预示性的理论，还无法具体操作和实施. 20世纪40年代电子计算机问世，数学机械化思想有了现实的可能性. 1950年，波兰数学家塔斯基(Tarski)从理论上证明了初等几何以及初等代数范围内的定理证明是可以证明的. 1959年，王浩设计了几个计算机程序，仅用3分钟就在IBM704型计算机上证明了数学家罗素(Russell)与怀特海(Whitehead)的数学著作《数学原理》中220条有关命题逻辑的定理，后来又扩展到400条. 这就宣告了数学定理证明的计算机操作的可行性. 王浩在《数理逻辑总览》中多次提出要使数学成为机械化的数学.

3 吴文俊的研究工作

吴文俊早期从事拓扑学的研究工作，他所提出的“吴示性类”与“吴示嵌类”以及“吴公式”成为拓扑学中的经典成果，广受国际数学同行们的赞誉.

1974年，因为当时社会现实的因素，他转向中国古代数学史的研究. 在此之前他并不了解中国古代传统数学成就，他说[2]，“中国的数学家，除了专门从事中国古代数学史的专家以外，绝大多数的中国数学家，包括陈省身和我，由于所受教育以及西方史书的影响，对中国的古代数学都是比较轻视，认为不足道的. ”

随着研究的深入，吴文俊逐渐认识到中国古代数学的特点是算法化和构造性. 例如，《周髀》中的日高公式主要是基于算法的考虑；汉初完成的《九章算术》在开平方、开立方运算过程中使用构造方法；宋元时代，探讨高次线性方程组的求解，等等. 可以说，中国古代数学正是沿着这样的数学机械化范式进行研究的，这不同于西方以希腊数学为传统的逻辑演绎体系. 虽然在西方数学研究历程中也曾有过诸多算法，但却不如中国如此突出和鲜明. 他用“机械化”一词高度概括了中国古代数学家解决数学问题的思路和方法.

专研中国古代数学史的同时，吴文俊也在计算机工厂劳动. 正是在这种情况下，他认识到计算机的原理与中国古代数学机械化思想是相通的，两者可以有效地结合起来，并促进彼此的深入发展.

1977年，吴文俊发表了《初等几何判定问题与机械化证明》. 与此同时，他提出了数学机械化纲领：在数学的各个学科选择适当的范围实现机械化，推动数学发展与脑力劳动机械化；应用数学机械化方法解决相关高科技领域的关键基础理论问题. 1985年，他发表了《关于代数方程组的零点》，讨论多项式方程组所确定的零点集. 至此，他正式确立了多项式方程组求解的吴文俊消元法，国际上简称为“吴方法”. “吴方法”的确立与广泛应用，复兴了国际数学机械化的研究.

吴文俊指出[1]，“我们从事机械化定理证明工作获得成果之前，对Tarski的已有工作并无接触，更没有想到Hilbert的《几何基础》会与机械化有任何关系. 我们是在中国古代数学的启发之下提出问题并想出解决办法来的. ”

4 吴方法的运用

1997年，吴文俊获得“厄布朗(Herbrand)自动推理杰出成就奖”，在授奖词中对他的工作给了这样的介绍和评价[3]：“几何定理自动证明首先由赫博特格兰特(Herbert Gerlenter)于50年代开始研究. 虽然得到一些有意义的结果，但在吴方法出现之前的20年里，这一领域进展甚微. 在不多的自动推理领域中，这种被动局面是由一个人完全扭转的. 吴文俊很明显是这样一个人. ”数学机械化思想的核心就是方程求解的“吴特征列方法”，这一方法实现了几何自动推理研究的突破，而推理的自动化正是计算机产生智能行为的一个关键. 以下简单地举几个吴方法运用的事例.

4.1 证明已有的科学定理和规律

物理学史上，牛顿通过观测和试验，推广了开普勒定律，推导出万有引力定律. 上世纪八十年代末，当美国学者正为如何借助计算机和数学工具从开普勒定律推导出牛顿定律而一筹莫展时，吴文俊使用吴方法巧妙地解决了这个重要的问题. 从开普勒定律的微分代数方程描述出发，经过整序运算，计算机可以自动产生新的微分代数表达式，再加上一些技术性的处理，就可以得到牛顿定律的微分代数表达式.

吴方法的一个特点是在证明时不考虑定理中几何元素的顺序. 所以用吴方法证明的几何定理实际上与定理的几何图形无关. 例如蝴蝶定理的证明：设A、B、C、D为圆上四点. E=AC∩BD，过点E与EO垂直的直线分别交AD、BC与M、N. 证明E是MN的中点. 这是高中数学中一个经典问题，一般来说，用正弦定理证明相对简便. 但是事先需要确定图形的形状，比如这个定理可以是下图三种情形中的任意一种. 而用吴方法证明此定理就不需要考虑命题中的几何图形. 定理一旦被证明是正确的，它的推论也自然成立，也就是对于所有的图形都正确.

吴文俊明确指出[1]，“目前我们所能证明的定理局限于已经发明的机械化方法的范围，例如初等几何与初等微分几何之内. 而如何超出与扩大这些机械化的范围，则是今后需要探索的长期的理论性工作. ”根据歌德尔的不完全定理，即使在初等数论的范围内，对所有数学命题进行证明的机械化方法也是不存在的.

4.2 发现新的数学关系和规律

吴方法不仅可以自动证明几何定理，还可以用来自动发现未知的几何关系. 几何中常见的关于面积、体积的公式可以用这个方法自动推导出来. 比如反映三角形面积与三条边间关系的海伦 (Heron)―秦九韶公式k=[KF(]s(s-a)(s-b)(s-c)[KF)]，就可以根据吴方法由计算机自动推理得出.

一个金字塔形状的几何体，用一个平面去截它，截面能否是一个正五边形？用吴方法解答这个问题时会得到一个令人意外的现象：上述平面和金字塔形状几何体的棱的延长线相交，有五个交点恰好是另一个正五边形的顶点，就是说还有一个正五边形存在，并且前一个正五边形在某种意义上处于黄金分割的位置，而后一个五边形处在于前一个在某种意义上相对偶的地方. 当然，这个发现在目前并没有任何实用意义，但是它为纯数学提供了一个和谐美妙的关系.

吴文俊强调[1]，“我们应该着重指出，我们并不鼓励以后人们将使用计算机来证明甚至发现一些有趣的几何定理. 恰恰相反，我们希望人们不再从事这种虽然有趣却即是对数学甚至几何学本身也已意义不大的工作，而把自己从这种工作中解放出来，把自己的聪明才智与创造能力贯注到更有意义的脑力劳动上去. ”

4.3 代数方程求解

数学机械化理论研究的核心内容是方程求解. 方程求解不仅是重要的数学问题，而且在许多的领域存在着应用. 事实上，很多科学和工程中的问题都可以转化为方程求解的问题. 无论是证明已有的定理和规律，还是发现新的数学关系和规律，实质上都是试图把所研究的问题转化成代数问题，列出方程组，进而求其零点解集. “求解代数方程组是数学上极为困难的问题，在理论上属于代数几何学. 但是，西方数学难以建立有效算法来真正去解这个方程组. 而吴文俊方法恰好能有效地做到这一点. ”[4]

5 我国其他数学家的工作

在吴文俊数学机械化思想方法的启发下，我国许多数学家在数学机械化领域也作出了许多卓越成就. 1992年，张景中院士根据面积法所创立的消点算法，成功地研制出几何定理自动生成可读的数学证明软件. 2000年，他进一步发展，研制出与传统几何证明方法一致的第三代智能数学平台软件，又称为“Z+Z”智能教育平台. 这开创了世界智能性数学教学软件的先河. 张景中院士和杨路、高小山、周咸青合作，把消点法用于非欧几何可读证明的自动生成也得到成功，并得到一批非欧几何新定理.

1999年，数学家杨路创立了降维算法，并研制出实现这种算法的数学软件. 通过这种软件，在计算机上证明了二千多个不等式. 不等式的机械化证明，这是几何定理机械化证明领域的又一个重大突破.

王梓坤院士指出，[5]“我们可以自豪地说：几何定理机械证明研究的重大成果大都是由我国数学家所取得的. ”

6 我国数学机械化研究方向与进展

“数学机械化是适应信息时代产生的基础研究领域，具有中国特色且在国际上领先. ”[6]中科院数学与系统科学研究院承担一项国家重点基础研究发展计划项目――数学机械化方法及其在信息技术中的应用. 参与项目研究的有中科院、北京大学、清华大学、南开大学、中国科技大学等. 主要有七个研究方向：数学机械化理论与核心算法，差分与微分方程的机械化算法，实几何与实代数的高效能算法，数学机械化与信息安全与编码理论，数学机械化在生物特征识别中的应用，数学机械化在几何建模中的应用，基于网络的数学机械化软件开发.

目前取得的一些研究成果无论是理论基础还是实际应用都是十分丰硕的，下面主要是从应用价值的角度简单地列举几项成就. 在信息安全方面，进行了密码分析与密码技术、协议的设计与分析，设计了能应用于电子现金系统的盲签名方案；设计了能用于移动通信的签名方案；设计了广播加密协议. 在生物特征识别中的应用，对指纹图象增强、奇异点检测和指纹搜索等方面进行了研究；研究掌纹识别的基本方法，并建立了一个具有一定规模的掌纹库. 基于网络的数学机械化软件开发方面，设计了包括《油田开发规划优化系统》和《油藏数值模拟中病态方程组求解》等大型复杂应用软件；根据哈尔滨电机厂提供的若干技术指标要求(例如，作业空间，加工效率，加工精度等)，设计了一台大型串联五轴数控机床.

参考文献

[1] 吴文俊.数学机械化[M].北京：科学出版社，2003.

[2] 梁芳.几何定理机器证明的方法――吴方法思想的形成[J].数学通报，2003,(6):4-6.

[3] 高小山,石赫.卓越的贡献 高度的评价――吴文俊及其科学成就[J].中国科学院院刊，2001,(1):64-66.

[4] 胡作玄.吴文俊――从拓扑学到数学机械化[J].自然辩证法通讯，2003,(1):81-90.

[5] 孙熙椿.数学机械化与我国数学家所取得的巨大成就[J].中学数学研究，2004,(2):43-46.

[6] 高小山.数学机械化研究展望[J].中国基础科学，1999,(1):26-28.

“本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文”