一位数学家的传统节日

一

1976年冬天，基层的某计算机工厂来了一位客人。

“我们这是计算机厂，计算机，就是搞计算的——包括数值计算和逻辑计算。程序让它干什么他就干什么。这有一个好处，你让人干一个什么事情，人可能会马虎出错，或者故意给你偷工减料，但是计算机不会，这玩意能进行一些逻辑上的判断，靠谱着呢 。走，我先带您老转转。”

粉碎“四人帮”之后，科研工作再一次走上了正轨。事实上，1972年科研工作开始部分恢复，同时中美数学家开始交流，特别是陈省身等华裔数学家回国，带来国际上的许多新情况。

“这是什么？”吴先生停下来问道。

“这就是计算机。不过可能跟您想象不一样，这是微型计算机，叫‘长城203’。”

吴先生拿起它来仔细端详。

上世纪七十年代的计算机跟现在还大不相同，计算速度自然是比不上，很多还是软盘+纸带编程。长城203是中国第一款微型计算机，现在看来，是一款配置相当低的计算机。

“长城203。”吴先生喃喃自语。

“是。这同样可以进行高速计算，通过软盘实现存储记忆功能。这是先进的，比较小。王选老师研究激光排照的纸带机要比这个大很多，时不常的动不了还得踢一脚；咱这个新产品，小巧玲珑。”

“你之前介绍说，计算机会按照设定的程序、算法一丝不苟的执行验证计算。”

“是的。”

“那能不能用计算机证明数学定理呢？”

“不清楚，我没想过这件事。”

“这样，咱们来研究一下，你来教我怎么用计算机。”

“可……可您这年纪……”

“那有什么的？”

二

“吴老师，您找我？”

“快春节了，不回家吗？”

“我在厂里值班，今年就不回去了，我是革命一块砖嘛。”

“哈哈，那就陪我说说话——对于用计算机证明定理，你有什么想法？”

“用计算机证明定理听起来很玄乎，因为数学证明当中有很多构造性的东西，如果想要‘以算代证’还需要找到比较好的算法。”

“如果从比较简单初等的东西里入手，比如平面几何呢？”

“嗯……”

“笛卡尔和《九章算术》先前给了我许多灵感，我们可以尝试把几何问题代数化求解。”

“那么我们就要引进一个合理的数系、坐标系把各种几何关系用代数方程来描述。”

“对。假设我们在适当选取坐标系之后得到的方程组为【H】：p1=0，p2=0,...pr=0，几何定理的结论由C：g=0来表示，其中fi都是关于变元x1...xn的多项式，那么问题会变成什么呢？”

“所以实现数学机械化证明的关键应该是【H】和g的零点集进行描述，和求解方程时的消元。但是每一步消元未必行得通，即使行得通是否现实可行也是问题。”

屋内两个人继续交谈着，屋外刮起了独属于腊月的凛凛寒风。

三

“这一天，我们还在庆祝新春，期盼着粉碎四人帮之后新的一年能有一个新的气象。出门看到吴先生欢天喜地的跑来找我，跟我说了一些并不能听太懂的话。

“比如说，吴先生说，“设 CS ＝ 为多项式方程组 [H] 的特征列。如果多项式 g 对 [H] 的特征列 CS 的余式 R=0, 则在条件 I i ≠ 0, i=1,2,…,k 之下 , 可从 [H]=0 推出 g =0 。条件 I i ≠ 0, i=1,2,…,k 称为数学定理成立的非退化条件。这组非退化条件是在计算特征列过程中自动产生的。”非退化条件大概是伍先生首创的，我并没有听说过。他还说了“用他的算法，判定一个命题 , 要分三步进行 : 第一步是把所给命题化为代数形式，即判定一组多项式的公共零点集是否被包含于另一多项式的零点集的问题 ; 第二步是整序，即把刻划命题条件的多项式组 [H] 经整序化为升列 AS ；第三步是求余，即将刻划命题结论的多项式 g 对于升列 AS 约化求取余式 R 。 若 R=0 ，即可断定命题在非退化条件 I i ≠ 0, i=1,2,…,k 之下成立，或者说命题一般成立，其中 I 1, I 2,…, I k 是升列 AS 中各多项式的初式。若 R 不为 0, 则当 AS 为不可约升列时 , 可断定命题不真。”

“总之是一些云里雾里的东西吧。按照吴先生的说法，好像是是提出了一套完整的算法，使得代数方程组通过机械步骤消元变成一个代数方程；并且解代数方程组可扩大为解带微分的代数方程组，从而大大扩张研究问题的范围？我不明白。真是搞不懂他们学数学的。

“不过，这种方法貌似还能自己发现定理。这大概是其他算法不能比拟的吧？据他讲，一个什么西姆松定理被他用长城203证明了，那玩意不是用四点共圆的嘛。接下来，事情一定会越来越有意思了。”

四

“过完年以后，吴先生就回去了。再听说吴先生的事情是报纸上几年以后了。听说他把证明从平面几何推广到了仿射几何、非欧几何和微分几何，并且还发现了双曲几何的一些定理，还对代数几何有一定贡献。据说还把Ritt定理和零点分解定理推广到微分多项式组。我不知道他是如何完成的。感觉跟几何比起来他做的方程求解的工作要更有意义一些。既然如此，春节时顺便证明了一些不等式也就是不足为奇的。

“只是一个去法国留学受了什么布尔巴基学派熏陶的人，后来很喜欢中国数学史，迷上《九章算术》研究起了算法，确乎比较怪。许是‘所之既倦，情随事迁，感慨系之矣。向之所欣，俯仰之间已为陈迹’。不过想到自己能在工厂里和他有一面之缘，聊上那么两句，这倒是一段值得珍惜的回忆吧。”

跋

吴文俊，1919年5月12日生于上海，中科院院士，中国科学院数学与系统科学研究院研究员，系统科学研究所名誉所长。对拓扑和数学机械化有一定贡献。

1940年毕业于上海交通大学数学系。

1947—1951年公费在法国斯特拉斯堡及巴黎留学，期间因国民党腐败而拒绝了国民政府的经济补助。归国后先后在北京大学、中科院工作。

1966年注意到他对示嵌类的研究可用于印刷电路的布线问题，并于１９７３年完全解决。他的方法完全是可以算法化的，与以前在布尔巴基影响下的纯理论的方向完全不同。大约从这时开始，他完成自己数学思想上一次根本性的改变。

1972年科研工作开始部分恢复，同时中美数学家开始交流。

1973年数学所拓扑组开始讨论有理同伦论，据此提出Ｉ＊函子理论，其显著特点之一也是“可计算性”。

1974年，吴文俊转向中国数学史，用算法及可计算性的观点来分析中国古代数学，发现其与由古希腊延续下来的近现代西方数学传统的重要区别，在许多方面产生独到的见解。

1976年粉碎“四人帮”之后，科学研究开始走上正轨。年近花甲的吴文俊更加焕发出青春活力。他在中国古算研究的基础上，分析了西方Ｒ．笛卡儿（的思想，深入探讨Ｄ．希尔伯特（Ｈｉｌｂｅｒｔ）《几何基础》一书中隐藏的构造性思想，开拓机械化数学的崭新领域。

1977年 平面几何定理的机械化证明取得成功。

1978年 微分几何的定理机械化证明成功。

1979年任普林斯顿大学高等研究院研究员，并与关肇直、许国志等人筹建中科院系统科学研究所，次年该所正式成立，任副所长兼基础数学室室主任、学术委员会主任，１９８３年后任名誉所长。

1982年更在国际机器证明会议上详细报告吴方法，受国际瞩目。

2001年获国家最高科学技术奖。

谨以此文向数学家们致敬。

∑编辑|Gemini

算法数学之美微信公众号欢迎赐稿

稿件涉及数学、物理、算法、计算机、编程等相关领域

稿件一经采用，我们将奉上稿酬。