由开普勒证明牛顿

让吴文俊十分感慨的是，他的机器证明研究一开始就得到有力的支持，他的成果“是在国家的特别资助下完成的”。从那时到现在，他已换过六七代计算机，有的价值十几万美元，甚至几十万美元。“这足以证明社会主义制度的优越性。国家在还不那么富裕的情况下总要拨出一些钱，资助科学家。”他说在科技部的支持下，周光召院长提议为他配备一台“比较高档”的计算机。

吴文俊的数学机械化方法研究开始有了初步成果。1986年，美国通用机器公司下属的一个研究机构，组织了一次国际学术会议，邀请吴文俊参加。有两位数学家邀请吴文俊谈了一天有关机器证明的研究。会后，美国科学家沃斯邀请吴文俊访问阿贡实验室，问他能不能用数学机械化方法从开普勒对行星运动的观测结果，直接导出牛顿的三定律。天体间引力与质量成正比比较容易理解，而与距离平方成反比就费解了。美国能源部一个研究小组用他们的方法解决不了这个难题，正面临解散的危险。回国后，吴文俊用了不到一个月时间就用数学机械化方法解决了这个难题——由开普勒的观测结果直接推导出牛顿三定律。

此前，吴文俊用数学机械化方法证明了几个定理，说明这种方法是可行的。那时候一个上千项的大数学式子，24小时用纸、笔算下来，十几页纸都放不下。现在（1977年），同样的问题计算机一秒钟都用不了就解决了。这意味着脑力劳动实现了机械化，科学家可以增强研究能力，提高研究效率，从而延长工作寿命。

吴文俊的研究于20世纪80年代中期传到国外。一个学生听了吴文俊的课，出国后向他的老板谈到了，这位老板显然是一位对新事物十分敏感的人，他向外界介绍了吴文俊的数学机械化方法。美国数学会《现代数学》杂志全文转载了吴文俊的一篇论文——这份杂志从来不刊登已发表过的论文。美国通用机器公司、康奈尔大学、法国信息技术研究中心等召开专门会议，研究吴文俊的数学机械化方法，并掀起了一个高潮，反响极大。

目前，吴文俊的研究仍在国际数学界处于领先地位，并形成了以海内外华人数学家为主的“吴学派”，关于几何的机器证明都是“吴学派”提出来的。用数学机械化方法证定理、解方程，正处在“吴学派”与国际数学界同行的较量之中。数学机械化方法研究是中国数学家吴文俊开创的全新研究领域，并引起国外数学家的高度重视。美国人工智能协会前主席布列德索写信给我国主管科技的领导人，称赞“吴关于平面几何定理自动证明的工作是一流的。他独自使中国在该领域进入国际领先地位”。

现在由吴文俊担任学术指导，国内有二三十个单位的六七十名科学家在从事数学机械化研究。高小山博士说，数学机械化方法的应用领域极其广阔，它可以为数学和其他领域的研究提供工具，为计算推理提供一种强有力的工具。在数学研究中的应用，可以把数学家从繁重的脑力劳动中解放出来，从而推动学科发展。这是数学机械化方法将来发展的主要方面之一，现在已经起步了。另外一个方面，数学机械化方法将会被应用于交叉研究，如力学、理论物理、机械构造、计算机技术、图像压缩、信息保密、新一代数控机床、计算机图形学、计算机辅助设计、机器人等许多领域。

1997年在获得国际著名的“埃尔布朗自动推理杰出成就奖”时，吴文俊还获得了这样的赞誉：几何定理自动证明首先由赫伯特·格兰特于20世纪50年代开始研究，虽然得到了一些有意义的结果，但在吴方法出现之前的10年里这一领域进展甚微。在不多的自动推理领域中，这种被动局面是由一个人完全扭转的。吴文俊很明显是这样一个人。

吴文俊，中国共产党党员，著名数学家，中国科学院院士。1919年5月12日出生于上海，1940年毕业于上海交通大学，1949年获法国斯特拉斯堡大学博士学位。1951年回国，先后在北京大学、中国科学院数学所、中国科学院系统所、中国科学院数学与系统科学研究院任职。曾任中国数学会理事长，中国科学院数理学部主任，全国政协常委，2002年国际数学家大会主席，中国人工智能学会名誉理事长，中国科学院系统所名誉所长。2017年5月7日，吴文俊在北京逝世。

吴文俊对数学的主要领域——拓扑学做出了重大贡献，开创了崭新的数学机械化领域，获得首届国家最高科技奖、首届国家自然科学一等奖、有东方诺贝尔奖之称的邵逸夫数学奖、国际自动推理最高奖埃尔布朗自动推理杰出成就奖。2019年在中华人民共和国成立70周年之际，被授予“人民科学家”国家荣誉称号。