“古为今用”开创“吴方法”
1975年,中科院数学所的《数学学报》上发表了一篇题为《中国古代数学对世界文化的伟大贡献》的文章,署名为“顾今用”。“顾”即“古”,“顾今用”意为“古为今用”。“顾今用”正是吴文俊。
遵循这一理念,在充分研读中国古代数学史的基础上,吴文俊“古为今用”,创造性提出数学机械化的想法。
1974年以后的两年多时间里,吴文俊的主要经历集中在数学史研究。古代几何、古代代数、古证复原……他系统地梳理了中国古代数学的发展。
这段经历让他更加坚信,中国古代数学和中华文化一样博大精深,且中国人完全有理由感到骄傲而不是跟在外国人后面亦步亦趋。
他曾举例说,中国古代有本著作《九章算术》。其中的术,就是讲方法。比如求最大公约数,书里核心就一句话:“以少减多,求其等也”。大数减小数,一步步减下去直到两边相等,就得到两个数的最大公约数。还有方程章,古人想到了正负数,这说明那时中国人的抽象能力就很强。
他认为,相对于信息时代的数学,中国古代数学蕴含深厚的数学机械化思想,简单明了,有它的一套。不可想象中国人的祖先已创造出非常适合应用于计算机的数学。
“中国传统数学是最古老的数学,也是最现代化的数学,2000多年前的中国古代数学就注定适应现代计算机。”吴文俊反复强调,中国古代数学是他最欣赏的,也是最值得骄傲的。
吴文俊说,中国古代数学就是一部算法大全,有着世界最早的几何学、最早的方程、最古老的矩阵。其中包含着独特的机械化思想,能够把几何问题转化成代数,再编成程序,输入电脑,代替大量复杂的人工演算,这样就可以把数学家从繁重的脑力劳动中解放出来,进而推进科学发展。这就是“数学机械化”。
“文化大革命”结束后,吴文俊立即开始用笔和纸验证自己的方法。1977年农历新年的大年初一,他发现自己的方法行得通。“成了!”同年,他的《初等几何判定问题与机械化问题》论文在《中国科学》上发表。
“工业革命解放了生产力,因为机械化解放了体力劳动。数学是一种脑力劳动,我希望数学机械化能让重复的脑力劳动得到解放,让人们去做更多创造性的工作。”吴文俊说。
下一步,就要到机器上进行检验。那时候,简单的袖珍计算器成了吴文俊心爱的工具。他曾利用HP25型袖珍计算器,检验中国古代数学的求解三次方程的数值解法。这种计算器有8个存储单元可以存放数值,他利用这8个单元就可以编一个小时程序,求得最高至五次方程的数值解。
但袖珍计算器显然不能运算更为复杂的定理证明,吴文俊急需购买一台计算机。那个年代,计算机无疑是奢侈品,而且买计算机需要外汇,从哪里才能找到这些钱呢?
正当吴文俊为此事发愁时,他的一位老朋友告诉他,时任中国科学院副院长的李昌要去某个地方做报告,你可以参加,那时再写封信交给他,申请一笔买计算机的钱。
抱着试试看的心态,吴文俊将信交给了李昌。没想到李昌马上批给他大约2万美元。1979年年初,应华裔物理学家杨振宁邀请,吴文俊带着2万美元到美国做学术访问。“当时真正的计算机要几百万美元,我买不起,只能买放在桌子上的台式计算机。”在朋友的帮助下,吴文俊以2万美元挑选了一台最好的台式机带回了祖国。
在吴文俊准备用计算机验证想法的关键时刻,国内数学界对他提出了不同看法。有些人甚至提出,外国人搞机器证明都是用数理逻辑的方法,为什么他要用代数几何的方法呢?对此,他只能顶着压力单枪匹马地干。
1978年,中国科学院将数学所分出部分成员,成立了系统科学研究所,吴文俊到了这边。系统科学研究所成立后不久,所长关肇直就对吴文俊说:“你想干什么就干什么,你爱干什么就干什么。”
“正是关肇直同志的理解,给了我最大的自由,这是最珍贵的!”吴文俊多年后感叹道。
其实,在国内学术界还在争议吴文俊的工作时,他的研究领域已引起了国外同行的重视。1978年秋,吴文俊到中国科学院研究生院授课。课堂上一位名叫周咸青的旁听生对他的理论很感兴趣。不久,周咸青到美国得克萨斯大学读博士。得克萨斯州刚好有一批人正在搞机械证明,但没有成功,周咸青便将自己听课的情况告诉教授,并以这个题目做自己的博士论文。
当时,吴文俊的《几何定理机器证明的基本原理》还没有正式出版,但周咸青将校印本带到了国外,吴文俊的研究成果也随之被系统地介绍到了国外。“周咸青的博士论文就是用我的方法,而且用我的方法证明了几百条定理,他自己还发明了一些定理。”吴文俊说,“他用那里的计算机来算,很难的证明也只需要几微秒,非常快。”
吴文俊运用自己的方法,在电子计算机上完成了西姆森线、费尔巴哈定理、毛莱定理等一系列初等几何的证明。随后,他又把证明的范围扩大到非欧几何、仿射几何、圆几何、线几何、球几何等领域。目前,运用他的方法,已证明出600多条定理,许多定理的证明只需几秒甚至零点几秒就可在电子计算机上完成。这其中有一些定理证明相当繁杂,即便交给杰出的数学家来证,也是相当困难的。
在吴文俊的影响下,中科院数学所与系统科学研究院成立了数学机械化研究中心,对“吴方法”和“吴消元法”进行大量的后续性研究工作。在这个中心,吴文俊的成就被应用于若干高科技领域,得到一系列国际领先的成果,包括曲面造型、机器人机构的位置分析、智能计算机辅助设计、信息传输中的图像压缩等。
在吴文俊的带领和影响下,这个中心已经形成了一支高水平的数学机械化研究队伍,在国际上被称为“吴学派”。这改变了数学家“一支笔、一张纸、一个脑袋”的劳动方式,运用电子计算机来实现数学证明。
吴文俊从初等几何着手,在计算机上证明了一类高难度的定理,同时也发现了一些新定理,进一步探讨了微分几何的定理证明。提出了利用机器证明与发现几何定理的新方法。这项工作为数学研究开辟了一个新的领域,对数学的革命产生了深远的影响。
在吴文俊看来,数学机械化思想是一种思维模式,一些数学分支,正是由于踏上了机械化的道路而获得蓬勃发展,使之成为重要的研究方向,甚至成为数学的主流。
美国《自动推理杂志》编委穆尔认为,“吴方法”建立之前,几何定理机械化证明的研究处于一片黑暗,吴不仅冲破了这种沉寂的局面,而且带来了光辉的前景。