1、1從吳文俊和吳方法談起從吳文俊和吳方法談起 數(shù)學機械化的思想數(shù)學機械化的思想 數(shù)學文化課程組 李軍2 中國科學院院士中國科學院院士 第三世界科學院院士第三世界科學院院士 首屆國家最高科技獎首屆國家最高科技獎 國家第一屆自然科學獎國家第一屆自然科學獎 最高獎一等獎最高獎一等獎 自動推理的最高獎自動推理的最高獎Herbrand獎獎 2006邵逸夫數(shù)學獎邵逸夫數(shù)學獎 3中央電視臺中央電視臺大家大家欄目：欄目：吳文俊吳文俊我的不等式我的不等式片斷片斷 4什么是數(shù)學機械化什么是數(shù)學機械化 所謂機械化，無非是刻板化和規(guī)格化。所謂機械化，無非是刻板化和規(guī)格化。數(shù)學數(shù)學問題的機械化，就要求在運算或證明過程中，

2、問題的機械化，就要求在運算或證明過程中，每前進一步之后，都有一個確定的、必須選每前進一步之后，都有一個確定的、必須選擇的下一步，這樣沿著一條有規(guī)律的、刻板擇的下一步，這樣沿著一條有規(guī)律的、刻板的道路，一直達到結論。的道路，一直達到結論。 使用一種機械化方法證明一類定理，才真正使用一種機械化方法證明一類定理，才真正體現(xiàn)了機械化定理證明。體現(xiàn)了機械化定理證明。1977年，吳文俊給年，吳文俊給出了初等幾何一類主要定理的機械化證明方出了初等幾何一類主要定理的機械化證明方法法“吳方法吳方法”。5數(shù)學機械化：從設想到實現(xiàn)數(shù)學機械化：從設想到實現(xiàn) 笛卡爾笛卡爾 萊布尼茨萊布尼茨 希爾伯特希爾伯特 6數(shù)學機械

3、化：從設想到實現(xiàn)數(shù)學機械化：從設想到實現(xiàn) 哥德爾哥德爾 塔斯基塔斯基 王浩王浩 吳文俊吳文俊7笛卡爾的設想笛卡爾的設想 17 世紀法國的數(shù)學家世紀法國的數(shù)學家 Descartes 曾有過一個偉大曾有過一個偉大的設想：的設想：“一切問題化為數(shù)學問題，一切數(shù)學問題一切問題化為數(shù)學問題，一切數(shù)學問題化為代數(shù)問題，一切代數(shù)問題化為代數(shù)方程求解問化為代數(shù)問題，一切代數(shù)問題化為代數(shù)方程求解問題。題。” Descartes 把問題想得太簡單了，如果他的設想真把問題想得太簡單了，如果他的設想真能實現(xiàn)，那就不僅是數(shù)學的機械化，而是全部科學能實現(xiàn)，那就不僅是數(shù)學的機械化，而是全部科學的機械化。因為代數(shù)方程求解是可

4、以機械化的。的機械化。因為代數(shù)方程求解是可以機械化的。 但但 Descartes 沒有停留在空想，他所創(chuàng)立的解析沒有停留在空想，他所創(chuàng)立的解析幾何，在空間形式和數(shù)量關系之間架起了一座橋梁，幾何，在空間形式和數(shù)量關系之間架起了一座橋梁，實現(xiàn)了初等幾何問題的代數(shù)化實現(xiàn)了初等幾何問題的代數(shù)化。8萊布尼茲之夢萊布尼茲之夢 德國數(shù)學家德國數(shù)學家 Leibniz 曾有過曾有過“推理機器推理機器”的的設想。他研究過邏輯，設計并制造出能做乘設想。他研究過邏輯，設計并制造出能做乘法的計算機，進而萌發(fā)了法的計算機，進而萌發(fā)了設計萬能語言和造設計萬能語言和造一臺通用機器的構想。一臺通用機器的構想。 他的努力促進了他

5、的努力促進了 Boole 代數(shù)、數(shù)理邏輯以及代數(shù)、數(shù)理邏輯以及計算機科學的研究，正是沿著這一方向，經(jīng)計算機科學的研究，正是沿著這一方向，經(jīng)后人的努力，形成了機器定理證明的邏輯方后人的努力，形成了機器定理證明的邏輯方法。法。 9希爾伯特的構想希爾伯特的構想 Hilbert在在幾何基礎幾何基礎中提出了從公理化走向機械中提出了從公理化走向機械化的數(shù)學構想。化的數(shù)學構想。Hilbert計劃將數(shù)學知識納入嚴格的計劃將數(shù)學知識納入嚴格的公理體系中，并著力在公理化基礎上尋找機械化的公理體系中，并著力在公理化基礎上尋找機械化的方法判定命題是否成立。方法判定命題是否成立。Hilbert同時指出，定理的同時指出，

6、定理的判定問題應當是分類解決的，解決方法要同時強調(diào)判定問題應當是分類解決的，解決方法要同時強調(diào)簡單性和嚴格性。簡單性和嚴格性。 在在 Hilbert 的名著的名著幾何基礎幾何基礎一書中就提供了一一書中就提供了一條可以對一類幾何命題進行判定的定理條可以對一類幾何命題進行判定的定理 當然，當然，在那個時代，不僅在那個時代，不僅 Hilbert 本人，整個數(shù)學界都沒本人，整個數(shù)學界都沒有意識到這一點。有意識到這一點。 10哥德爾的著名結果哥德爾的著名結果 Gdel著名的不完全性定理指出一個不弱于初等數(shù)論的形式系統(tǒng)如果是無矛盾的，則是不完全的 ，即存在形式系統(tǒng)的一個命題，它和它的否定都不能由形式系統(tǒng)證

7、明。 因此， Hilbert 的要求太高了。上述的Gdel不完全性定理斷言：即使在初等數(shù)論的范圍內(nèi)，對所有命題進行判定的機械化方法也是不存在的！ 11塔斯基的判定法塔斯基的判定法 波蘭數(shù)學家波蘭數(shù)學家 Tarski 在在 1950 年推廣了關于代年推廣了關于代數(shù)方程實根數(shù)目的數(shù)方程實根數(shù)目的 Sturm 法則，由此證明了法則，由此證明了一個引人注目的定理：一個引人注目的定理：“一切初等幾何和初一切初等幾何和初等代數(shù)范圍的命題，都可以用機械方法判等代數(shù)范圍的命題，都可以用機械方法判定定。” Tarski得出的結論給定理證明機械化的研究得出的結論給定理證明機械化的研究帶來了曙光。可惜他的方法太復雜

8、，即使用帶來了曙光。可惜他的方法太復雜，即使用高速計算機也證明不了稍難的幾何定理。高速計算機也證明不了稍難的幾何定理。 12王浩：邁向數(shù)學機械化王浩：邁向數(shù)學機械化 1959 年，王浩設計了一個程序，用計算機證年，王浩設計了一個程序，用計算機證明了明了 Russell 、 Whitehead 的巨著的巨著數(shù)學數(shù)學原理原理中的幾百條有關命題邏輯的定理，僅中的幾百條有關命題邏輯的定理，僅用了用了 9 分鐘。分鐘。王浩工作的意義在于宣告了用王浩工作的意義在于宣告了用計算機進行定理證明的可能性計算機進行定理證明的可能性。 在在1960年的年的IBM研究與發(fā)展年報研究與發(fā)展年報（IBM Journal）

9、，王浩發(fā)表了），王浩發(fā)表了邁向數(shù)學機械化邁向數(shù)學機械化（Toward Mechanical Mathematics），），“數(shù)學機械化數(shù)學機械化”一詞即出自此處。一詞即出自此處。13吳文俊：吳文俊：機器證明領域的新的一頁機器證明領域的新的一頁 1977 年，吳文俊在年，吳文俊在中國科學中國科學上發(fā)表論文上發(fā)表論文初初 等幾何判定問題與機械化問題等幾何判定問題與機械化問題。 1984 年，吳文年，吳文俊的學術專著俊的學術專著幾何定理機器證明的基本原理幾何定理機器證明的基本原理由由科學出版社出版，這部專著著重闡明幾何定理機械科學出版社出版，這部專著著重闡明幾何定理機械化證明的基本原理。化證明的基本

10、原理。 1985 年，吳文俊的論文年，吳文俊的論文關關于代數(shù)方程組的零點于代數(shù)方程組的零點發(fā)表，具體討論了多項式方發(fā)表，具體討論了多項式方程組所確定的零點集。與國際上流行的代數(shù)理想論程組所確定的零點集。與國際上流行的代數(shù)理想論不同，明確提出了具有中國自己特色的、以多項式不同，明確提出了具有中國自己特色的、以多項式零點集為基本點的機械化方法。自此，零點集為基本點的機械化方法。自此，“吳方法吳方法”宣告誕生，數(shù)學機械化研究揭開了新的一幕。宣告誕生，數(shù)學機械化研究揭開了新的一幕。 14對吳方法的評價吳方法遵循中國傳統(tǒng)數(shù)學中幾何代數(shù)化的思想，與通常基于數(shù)理邏輯的方法根本不同，首次實現(xiàn)了高效的幾何定理自

11、動證明，顯現(xiàn)了無比的優(yōu)越性。他的工作被稱為自動推理領域的先驅性工作，并于1997年獲得“Herbrand自動推理杰出成就獎”。在授獎辭中對他的工作給了這樣的介紹與評價: “幾何定理自動證明首先由赫伯特格蘭特(Herbert Gerlenter)于50年代開始研究。雖然得到一些有意義的結果，但在吳方法出現(xiàn)之前的20年里，這一領域進展甚微。在不多的自動推理領域中，這種被動局面是由一個人完全扭轉的。吳文俊很明顯是這樣一個人。他將幾何定理證明從一個不太成功的領域變?yōu)樽畛晒Φ念I域之一。”15 20062006年，著名數(shù)學家吳文俊榮獲邵逸年，著名數(shù)學家吳文俊榮獲邵逸夫數(shù)學科學獎。邵逸夫數(shù)學科學獎是一項夫數(shù)

12、學科學獎。邵逸夫數(shù)學科學獎是一項國際性大獎，它的評委是來自國際數(shù)學界國際性大獎，它的評委是來自國際數(shù)學界的知名權威。吳文俊說：這次邵逸夫獎的的知名權威。吳文俊說：這次邵逸夫獎的評委都是國際上有影響的大家，他們宣布評委都是國際上有影響的大家，他們宣布我獲得邵逸夫獎，是因為我的數(shù)學機械化我獲得邵逸夫獎，是因為我的數(shù)學機械化問題的研究，這實際上是國際數(shù)學界對數(shù)問題的研究，這實際上是國際數(shù)學界對數(shù)學機械化研究的承認與肯定，它比獎金重學機械化研究的承認與肯定，它比獎金重要得多。要得多。 數(shù)學機械化得到國際數(shù)學界承認數(shù)學機械化得到國際數(shù)學界承認 16 吳文俊吳文俊我的不等式我的不等式片斷片斷 17三角形三

13、條高線交于一點的代數(shù)證明三角形三條高線交于一點的代數(shù)證明 D是是BC和和CA上高線交點上高線交點18 0)(14253xxxxxBCAD0)(24153xxxxxACBD0)(213 xxx04 x定理的假設部分是定理的假設部分是,由吳方法，可得非退化條件由吳方法，可得非退化條件是是.定理的結論是定理的結論是CO經(jīng)過經(jīng)過D點點.顯然在非退化條件下定理成立顯然在非退化條件下定理成立。19Morley定理定理 任意三角形中，一個角的三等分線，與和任意三角形中，一個角的三等分線，與和它相鄰的角的三等分線相交，交點組成正它相鄰的角的三等分線相交，交點組成正三角形。三角形。20機器方法容易證明機器方法容

14、易證明Morley定理定理 任意三角形中，一個角的三等分線，與和任意三角形中，一個角的三等分線，與和它相鄰的角的三等分線相交，按一定的規(guī)它相鄰的角的三等分線相交，按一定的規(guī)則選取交點，共可組成則選取交點，共可組成27個三角形，在這個三角形，在這27個三角形中，一定有個三角形中，一定有18個是正三角形。個是正三角形。用機器方法容易證明這個更一般的用機器方法容易證明這個更一般的Morley定理。在證明過程中，多次出現(xiàn)關于定理。在證明過程中，多次出現(xiàn)關于12個個變量的含有一千多項的多項式。變量的含有一千多項的多項式。21吳方法概要定理的假設相當于一組多項式方程定理的結論相當于一個多項式方程上面的諸F

15、i稱為假設多項式，G稱為終結多項式。0, 01sFF0G22吳方法概要（續(xù)） 吳方法是給出了一個機械化方法，在有限步內(nèi)給出一組非退化條件多項式D1, , Dr 又根據(jù)這一機械化方法足以在有限步內(nèi)，判定在非退化條件 D10, , Dr 0 下，G=0是否可從F1=0, , Fs=0推出。 23平行四邊形對角線互相平分24題設和結論表成代數(shù)形式0)(:/31123uxuuuBCAD0)()(123113uxuuxxBDE上：在03223uxuxACE上：在022:33232222xuuxuuECEA結論25吳方法的處理題設部分三角化，得到三個多項式： 再把結論左邊的多項式除以f3，所得的余式除以f

16、2，所得的余式除以f1，看最后所得的余式是不是恒等于零。1121xuuf3121132)(uuuuxxf32233uxuxf26中國古代數(shù)學的貢獻 70 年代初，吳文俊開始研讀中國數(shù)學史。1975 年，他撰寫了中國古代數(shù)學對世界文化的偉大貢獻，文中詳細列舉在代數(shù)、幾何、三角、解析幾何和微積分等學科的發(fā)現(xiàn)和創(chuàng)立過程中，中國傳統(tǒng)數(shù)學所起的重大作用。 吳文俊指出，中國傳統(tǒng)數(shù)學注意解方程，在代數(shù)學、幾何學、極限概念等方面既有豐碩的成果，又有系統(tǒng)的理論。27中國古代數(shù)學的特色 中國傳統(tǒng)數(shù)學強調(diào)構造性和算法化，注意解決科學實驗和生產(chǎn)實踐中提出的各類問題，往往把所得到的結論以各種原理的形式予以表述。 在中國

17、古代，求兩數(shù)最大公約數(shù)即等數(shù)用更相減損之術。如求24與15的等數(shù)，其逐步減損如下： （24，15）（9，15）（9，6）（3，6）（3，3） 其理由不證自明。 中國傳統(tǒng)數(shù)學在從問題出發(fā)以解決問題為主旨的發(fā)展過程中建立了以構造性與機械化為其特色的算法體系， 九章算術與劉徽的九章算術注是這一機械化體系的代表作，這與西方數(shù)學以歐幾里得幾何原本為代表的所謂公理化演繹體系正好遙遙相對。 28機械化思想是中國古代數(shù)學的精髓 吳文俊把中國傳統(tǒng)數(shù)學的思想概括為機械化思想，指出它是貫穿于中國古代數(shù)學的精髓。他列舉大量事實說明，中國傳統(tǒng)數(shù)學的機械化思想為近代數(shù)學的建立和發(fā)展做出了不可磨滅的貢獻。 這種機械化思想，

18、不僅曾深刻影響了數(shù)學的歷史進程，而且對數(shù)學的現(xiàn)狀也正在發(fā)揚它日益顯著的影響。 29數(shù)學機械化的廣泛應用 吳文俊特別重視數(shù)學機械化方法的應用，明確提出“數(shù)學機械化方法的成功應用，是數(shù)學機械化研究的生命線”。他不斷開拓新的應用領域，如控制論、曲面拼接問題、機構設計、化學平衡問題、平面天體運行的中心構形等，還建立了解決全局優(yōu)化問題的新方法。 吳方法還被用于若干高科技領域，得到一系列國際領先的成果，包括曲面造型、機器人結構的位置分析、智能計算機輔助設計(CAD)、信息傳輸中的圖像壓縮等。30從開普勒定律到牛頓定律 開普勒定律為（1）行星繞太陽以橢圓軌道運行，太陽為一焦點（2）太陽到行星的向量在相同的時

19、間掃過相同的 面積 牛頓定律為（3）行星的加速度與太陽到行星的距離的平方成反比 利用吳方法在微分域上的推廣，可以從開普勒經(jīng)驗公式自動推導出牛頓定律。31機器人與連桿機構的運動分析 如圖，綠色的平臺是活動平臺，下面的平臺是固定的，六根連桿長度可變，求連桿長度變化時平臺上一點的 軌跡。32機器人與連桿機構的運動分析 已知連桿機構的構成，求該機構上某一點的軌跡及該點的位置與連桿機構的關系，這類問題稱為機械設計中的正解問題。前面的例子就是一個正解問題。 反過來，求解連桿機構的參數(shù)使得連桿機構上一點恰好位于空間指定位置的問題稱為機械設計中的逆解問題。 這兩類問題都可以看成方程求解問題。 吳文俊用特征集方

20、法解決了一般PUMA型機器人的逆解問題，研究了四連桿的設計問題。33曲面連接問題 在幾何設計中，有一大類問題要確定一給定次數(shù)的 代數(shù)曲面按一定要求連接已給的若干代數(shù)曲面。 這類問題可以用吳方法解決。左圖是一個連接左圖是一個連接三根管道的例子。三根管道的例子。34腦力勞動的機械化 在在新的正在到來的工業(yè)革命新的正在到來的工業(yè)革命中，可以認為是以某中，可以認為是以某種設備代替人腦。這將使人類艱苦思考的價值為種設備代替人腦。這將使人類艱苦思考的價值為之降低，之降低，是一種腦力勞動的機械化是一種腦力勞動的機械化。這種機械化。這種機械化由于上世紀中葉計算機的發(fā)明而有某種可能。由于上世紀中葉計算機的發(fā)明而

21、有某種可能。數(shù)學是一種典型的腦力勞動。由于數(shù)學思維具有數(shù)學是一種典型的腦力勞動。由于數(shù)學思維具有其它思維方式所沒有的簡潔、明確、嚴密、清晰其它思維方式所沒有的簡潔、明確、嚴密、清晰等優(yōu)點，因而數(shù)學的機械化比之其它思維的機械等優(yōu)點，因而數(shù)學的機械化比之其它思維的機械化，應有它的優(yōu)越性與優(yōu)先性，而且應更為容易。化，應有它的優(yōu)越性與優(yōu)先性，而且應更為容易。吳方法在幾何定理證明方面機械化的成功，正好吳方法在幾何定理證明方面機械化的成功，正好說明確是如此。說明確是如此。 35機械化思想促進數(shù)學發(fā)展 線性方程組求解中的消去法是機械化思想的杰作。線性方程組求解中的消去法是機械化思想的杰作。即使是現(xiàn)代純粹數(shù)學研究中，機械化思想也一直即使是現(xiàn)代純粹數(shù)學研究中，機械化思想也一直發(fā)揮重大的作用。例如，希爾伯特倡導的數(shù)理邏