吴文俊： 用数学机械化征服世界

1919年，也就是“五四运动”爆发的那一年，吴文俊出生于上海。早年他就读于交通大学（现西安交通大学和上海交通大学的前身）数学系，后赴法国留学，获法国国家博士学位。

1951年夏天回国后，一直到1952年，吴文俊在北京大学数学系教书。院系调整后，他调到了中国科学院数学研究所。当时，出于扩大研究范围的考虑，他对拓扑学进行了形势分析和历史调查，并在无意中发现他的这个做法符合法国一位大数学家讲过的一句话：如果我们想要预见数学的將来，适当的途径是研究这门科学的历史与现状。

通过分析、思考，吴文俊进一步明确了自己的研究方向，建立了示嵌类理论。1956年，因在拓扑学中的示性类和示嵌类方面的卓越成就，吴文俊获得了首届国家自然科学奖一等奖，并在第二年被选为中国科学院学部委员（后称院士），那一年他只有38岁。

1974年至1975年，数学研究所领导建议全体人员学习中国古代数学。原来对中国古代数学不以为然的吴文俊，通过学习，在认识上竟然产生了一个巨大的飞跃，而且把自己获得的新认识跟手头从事的研究联系起来。

也就是在这个时期，吴文俊被下放到北京无线电一厂劳动，当时这家工厂正在生产一种混合式电子计算机。在那里，他亲眼目睹了计算机效率之高，就想：是不是可以把计算机应用到数学上来。数学家为计算机的创建做了许多工作，反过来，是否可以用计算机来帮助数学家，比如证明几何定理？

吴文俊在演讲（供图/尹传红）

实际上，吴文俊已切身体会到计算机的巨大威力，并敏锐地觉察到计算机极大的发展潜能。于是，他一头扎进机房，从 HP-1000 机型开始，学习算法语言，编制算法程序。

学习中国数学史和接触到计算机，这两个机遇的碰撞让吴文俊感觉到，中国数学的思想和方法跟现在的计算机是合拍的，这促使他开始进行一些机器证明方面的尝试。

经过对中国古代数学的学习和触发，结合对几十年来在数学研究道路上探索实践的回顾与分析，吴文俊终于形成了数学机械化的思想。他意识到，中国古代数学正好是适合计算机时代的一种算法的数学，或者叫计算机数学，他个人称之为机械化的数学。他总结出中国古代数学的特点是：从实际问题出发，经过分析提高，再抽象出一般的原理、原则和方法，最终达到解决一大类问题的目的。

1976年和1977年之交，吴文俊根据当时的思想认识，在几何定理的证明上进行了尝试。那个时候没有什么像样的计算机，他是用手算，就好像他自己是一个机器，仿造机器的动作，通过一步一步手算来进行定理的证明。经过几个月的艰苦尝试，终于取得了成功，产生了所谓几何定理的机器证明，这在国外引起了相当大的反响。

吴文俊在讲课（供图/尹传红）

1977 年，吴文俊的论文《初等几何判定问题与机械化证明》发表于《中国科学》。接下来，他在数学机械化或机器证明方面，从初等几何着手，在计算机上证明了一类高难度的定理;同时也发现了一些新定理，进一步探讨了微分几何的定理证明，提出了利用机器证明与发现几何定理的新方法。这项工作为数学研究开辟了一个新的领域，对数学的革命产生了深远的影响，1978年，吴文俊获全国科学大会重大科技成果奖。20世纪80年代以来，吴文俊把数学发展成为有系统的、范围较广的，不仅限于数学，而且应用到许多不同的领域的过程，叫作数学的机械化。

1984 年，吴文俊推出学术专著《几何定理机器证明的基本原理（初等几何部分）》，奠定了数学机械化研究在中国的基础。1985 年，吴文俊的论文《关于代数方程组的零点》发表，这篇重要文献，是正式建立求解多项式方程组的吴文俊消元法的重要标志。自此，“吴方法”宣告诞生，并且在国际机器证明领域产生了巨大的影响，有着广泛而又重要的应用价值。数学机械化研究由此揭开了新的一幕。

（责任编辑/江盼 美术编辑/张小穗）