“古为今用”开创“吴方法”

1975年，中科院数学所的《数学学报》上发表了一篇题为《中国古代数学对世界文化的伟大贡献》的文章，署名为“顾今用”。“顾”即“古”，“顾今用”意为“古为今用”。“顾今用”正是吴文俊。

遵循这一理念，在充分研读中国古代数学史的基础上，吴文俊“古为今用”，创造性提出数学机械化的想法。

1974年以后的两年多时间里，吴文俊的主要经历集中在数学史研究。古代几何、古代代数、古证复原……他系统地梳理了中国古代数学的发展。

这段经历让他更加坚信，中国古代数学和中华文化一样博大精深，且中国人完全有理由感到骄傲而不是跟在外国人后面亦步亦趋。

他曾举例说，中国古代有本著作《九章算术》。其中的术，就是讲方法。比如求最大公约数，书里核心就一句话：“以少减多，求其等也”。大数减小数，一步步减下去直到两边相等，就得到两个数的最大公约数。还有方程章，古人想到了正负数，这说明那时中国人的抽象能力就很强。

他认为，相对于信息时代的数学，中国古代数学蕴含深厚的数学机械化思想，简单明了，有它的一套。不可想象中国人的祖先已创造出非常适合应用于计算机的数学。

“中国传统数学是最古老的数学，也是最现代化的数学，2000多年前的中国古代数学就注定适应现代计算机。”吴文俊反复强调，中国古代数学是他最欣赏的，也是最值得骄傲的。

吴文俊说，中国古代数学就是一部算法大全，有着世界最早的几何学、最早的方程、最古老的矩阵。其中包含着独特的机械化思想，能够把几何问题转化成代数，再编成程序，输入电脑，代替大量复杂的人工演算，这样就可以把数学家从繁重的脑力劳动中解放出来，进而推进科学发展。这就是“数学机械化”。

“文化大革命”结束后，吴文俊立即开始用笔和纸验证自己的方法。1977年农历新年的大年初一，他发现自己的方法行得通。“成了!”同年，他的《初等几何判定问题与机械化问题》论文在《中国科学》上发表。

“工业革命解放了生产力，因为机械化解放了体力劳动。数学是一种脑力劳动，我希望数学机械化能让重复的脑力劳动得到解放，让人们去做更多创造性的工作。”吴文俊说。

下一步，就要到机器上进行检验。那时候，简单的袖珍计算器成了吴文俊心爱的工具。他曾利用HP25型袖珍计算器，检验中国古代数学的求解三次方程的数值解法。这种计算器有8个存储单元可以存放数值，他利用这8个单元就可以编一个小时程序，求得最高至五次方程的数值解。

但袖珍计算器显然不能运算更为复杂的定理证明，吴文俊急需购买一台计算机。那个年代，计算机无疑是奢侈品，而且买计算机需要外汇，从哪里才能找到这些钱呢？

正当吴文俊为此事发愁时，他的一位老朋友告诉他，时任中国科学院副院长的李昌要去某个地方做报告，你可以参加，那时再写封信交给他，申请一笔买计算机的钱。

抱着试试看的心态，吴文俊将信交给了李昌。没想到李昌马上批给他大约2万美元。1979年年初，应华裔物理学家杨振宁邀请，吴文俊带着2万美元到美国做学术访问。“当时真正的计算机要几百万美元，我买不起，只能买放在桌子上的台式计算机。”在朋友的帮助下，吴文俊以2万美元挑选了一台最好的台式机带回了祖国。

在吴文俊准备用计算机验证想法的关键时刻，国内数学界对他提出了不同看法。有些人甚至提出，外国人搞机器证明都是用数理逻辑的方法，为什么他要用代数几何的方法呢？对此，他只能顶着压力单枪匹马地干。

1978年，中国科学院将数学所分出部分成员，成立了系统科学研究所，吴文俊到了这边。系统科学研究所成立后不久，所长关肇直就对吴文俊说：“你想干什么就干什么，你爱干什么就干什么。”

“正是关肇直同志的理解，给了我最大的自由，这是最珍贵的!”吴文俊多年后感叹道。

其实，在国内学术界还在争议吴文俊的工作时，他的研究领域已引起了国外同行的重视。1978年秋，吴文俊到中国科学院研究生院授课。课堂上一位名叫周咸青的旁听生对他的理论很感兴趣。不久，周咸青到美国得克萨斯大学读博士。得克萨斯州刚好有一批人正在搞机械证明，但没有成功，周咸青便将自己听课的情况告诉教授，并以这个题目做自己的博士论文。

当时，吴文俊的《几何定理机器证明的基本原理》还没有正式出版，但周咸青将校印本带到了国外，吴文俊的研究成果也随之被系统地介绍到了国外。“周咸青的博士论文就是用我的方法，而且用我的方法证明了几百条定理，他自己还发明了一些定理。”吴文俊说，“他用那里的计算机来算，很难的证明也只需要几微秒，非常快。”

吴文俊运用自己的方法，在电子计算机上完成了西姆森线、费尔巴哈定理、毛莱定理等一系列初等几何的证明。随后，他又把证明的范围扩大到非欧几何、仿射几何、圆几何、线几何、球几何等领域。目前，运用他的方法，已证明出600多条定理，许多定理的证明只需几秒甚至零点几秒就可在电子计算机上完成。这其中有一些定理证明相当繁杂，即便交给杰出的数学家来证，也是相当困难的。

在吴文俊的影响下，中科院数学所与系统科学研究院成立了数学机械化研究中心，对“吴方法”和“吴消元法”进行大量的后续性研究工作。在这个中心，吴文俊的成就被应用于若干高科技领域，得到一系列国际领先的成果，包括曲面造型、机器人机构的位置分析、智能计算机辅助设计、信息传输中的图像压缩等。

在吴文俊的带领和影响下，这个中心已经形成了一支高水平的数学机械化研究队伍，在国际上被称为“吴学派”。这改变了数学家“一支笔、一张纸、一个脑袋”的劳动方式，运用电子计算机来实现数学证明。

吴文俊从初等几何着手，在计算机上证明了一类高难度的定理，同时也发现了一些新定理，进一步探讨了微分几何的定理证明。提出了利用机器证明与发现几何定理的新方法。这项工作为数学研究开辟了一个新的领域，对数学的革命产生了深远的影响。

在吴文俊看来，数学机械化思想是一种思维模式，一些数学分支，正是由于踏上了机械化的道路而获得蓬勃发展，使之成为重要的研究方向，甚至成为数学的主流。

美国《自动推理杂志》编委穆尔认为，“吴方法”建立之前，几何定理机械化证明的研究处于一片黑暗，吴不仅冲破了这种沉寂的局面，而且带来了光辉的前景。