數(shù)學(xué)機(jī)械化的思想

1、1,從吳文俊和吳方法談起,數(shù)學(xué)機(jī)械化的思想 數(shù)學(xué)文化課程組 李軍,2,吳文俊 中國(guó)科學(xué)院院士 第三世界科學(xué)院院士 首屆國(guó)家最高科技獎(jiǎng) 國(guó)家第一屆自然科學(xué)獎(jiǎng) 最高獎(jiǎng)一等獎(jiǎng) 自動(dòng)推理的最高獎(jiǎng)herbrand獎(jiǎng) 2006邵逸夫數(shù)學(xué)獎(jiǎng),3,中央電視臺(tái)大家欄目：吳文俊我的不等式片斷,4,什么是數(shù)學(xué)機(jī)械化,所謂機(jī)械化，無(wú)非是刻板化和規(guī)格化。數(shù)學(xué)問(wèn)題的機(jī)械化，就要求在運(yùn)算或證明過(guò)程中，每前進(jìn)一步之后，都有一個(gè)確定的、必須選擇的下一步，這樣沿著一條有規(guī)律的、刻板的道路，一直達(dá)到結(jié)論。 使用一種機(jī)械化方法證明一類定理，才真正體現(xiàn)了機(jī)械化定理證明。1977年，吳文俊給出了初等幾何一類主要定理的機(jī)械化證明方法“吳方

2、法”。,5,數(shù)學(xué)機(jī)械化：從設(shè)想到實(shí)現(xiàn),笛卡爾 萊布尼茨 希爾伯特,6,數(shù)學(xué)機(jī)械化：從設(shè)想到實(shí)現(xiàn),哥德?tīng)?塔斯基 王浩 吳文俊,7,笛卡爾的設(shè)想,17 世紀(jì)法國(guó)的數(shù)學(xué)家 descartes 曾有過(guò)一個(gè)偉大的設(shè)想：“一切問(wèn)題化為數(shù)學(xué)問(wèn)題，一切數(shù)學(xué)問(wèn)題化為代數(shù)問(wèn)題，一切代數(shù)問(wèn)題化為代數(shù)方程求解問(wèn)題?！?descartes 把問(wèn)題想得太簡(jiǎn)單了，如果他的設(shè)想真能實(shí)現(xiàn)，那就不僅是數(shù)學(xué)的機(jī)械化，而是全部科學(xué)的機(jī)械化。因?yàn)榇鷶?shù)方程求解是可以機(jī)械化的。 但 descartes 沒(méi)有停留在空想，他所創(chuàng)立的解析幾何，在空間形式和數(shù)量關(guān)系之間架起了一座橋梁，實(shí)現(xiàn)了初等幾何問(wèn)題的代數(shù)化。,8,萊布尼茲之夢(mèng),德國(guó)數(shù)學(xué)家

3、leibniz 曾有過(guò)“推理機(jī)器”的設(shè)想。他研究過(guò)邏輯，設(shè)計(jì)并制造出能做乘法的計(jì)算機(jī)，進(jìn)而萌發(fā)了設(shè)計(jì)萬(wàn)能語(yǔ)言和造一臺(tái)通用機(jī)器的構(gòu)想。 他的努力促進(jìn)了 boole 代數(shù)、數(shù)理邏輯以及計(jì)算機(jī)科學(xué)的研究，正是沿著這一方向，經(jīng)后人的努力，形成了機(jī)器定理證明的邏輯方法。,9,希爾伯特的構(gòu)想,hilbert在幾何基礎(chǔ)中提出了從公理化走向機(jī)械化的數(shù)學(xué)構(gòu)想。hilbert計(jì)劃將數(shù)學(xué)知識(shí)納入嚴(yán)格的公理體系中，并著力在公理化基礎(chǔ)上尋找機(jī)械化的方法判定命題是否成立。hilbert同時(shí)指出，定理的判定問(wèn)題應(yīng)當(dāng)是分類解決的，解決方法要同時(shí)強(qiáng)調(diào)簡(jiǎn)單性和嚴(yán)格性。 在 hilbert 的名著幾何基礎(chǔ)一書(shū)中就提供了一條可以對(duì)一

4、類幾何命題進(jìn)行判定的定理 當(dāng)然，在那個(gè)時(shí)代，不僅 hilbert 本人，整個(gè)數(shù)學(xué)界都沒(méi)有意識(shí)到這一點(diǎn)。,10,哥德?tīng)柕闹Y(jié)果,gdel著名的不完全性定理指出一個(gè)不弱于初等數(shù)論的形式系統(tǒng)如果是無(wú)矛盾的，則是不完全的 ，即存在形式系統(tǒng)的一個(gè)命題，它和它的否定都不能由形式系統(tǒng)證明。 因此， hilbert 的要求太高了。上述的gdel不完全性定理斷言：即使在初等數(shù)論的范圍內(nèi)，對(duì)所有命題進(jìn)行判定的機(jī)械化方法也是不存在的！,11,塔斯基的判定法,波蘭數(shù)學(xué)家 tarski 在 1950 年推廣了關(guān)于代數(shù)方程實(shí)根數(shù)目的 sturm 法則，由此證明了一個(gè)引人注目的定理：“一切初等幾何和初等代數(shù)范圍的命題，都

5、可以用機(jī)械方法判定?！?tarski得出的結(jié)論給定理證明機(jī)械化的研究帶來(lái)了曙光?？上姆椒ㄌ珡?fù)雜，即使用高速計(jì)算機(jī)也證明不了稍難的幾何定理。,12,王浩：邁向數(shù)學(xué)機(jī)械化,1959 年，王浩設(shè)計(jì)了一個(gè)程序，用計(jì)算機(jī)證明了 russell 、 whitehead 的巨著數(shù)學(xué)原理中的幾百條有關(guān)命題邏輯的定理，僅用了 9 分鐘。王浩工作的意義在于宣告了用計(jì)算機(jī)進(jìn)行定理證明的可能性。 在1960年的ibm研究與發(fā)展年報(bào)（ibm journal），王浩發(fā)表了邁向數(shù)學(xué)機(jī)械化（toward mechanical mathematics），“數(shù)學(xué)機(jī)械化”一詞即出自此處。,13,吳文?。簷C(jī)器證明領(lǐng)域的新的一頁(yè),

6、1977 年，吳文俊在中國(guó)科學(xué)上發(fā)表論文初 等幾何判定問(wèn)題與機(jī)械化問(wèn)題。 1984 年，吳文俊的學(xué)術(shù)專著幾何定理機(jī)器證明的基本原理由科學(xué)出版社出版，這部專著著重闡明幾何定理機(jī)械化證明的基本原理。 1985 年，吳文俊的論文關(guān)于代數(shù)方程組的零點(diǎn)發(fā)表，具體討論了多項(xiàng)式方程組所確定的零點(diǎn)集。與國(guó)際上流行的代數(shù)理想論不同，明確提出了具有中國(guó)自己特色的、以多項(xiàng)式零點(diǎn)集為基本點(diǎn)的機(jī)械化方法。自此，“吳方法”宣告誕生，數(shù)學(xué)機(jī)械化研究揭開(kāi)了新的一幕。,14,對(duì)吳方法的評(píng)價(jià),吳方法遵循中國(guó)傳統(tǒng)數(shù)學(xué)中幾何代數(shù)化的思想，與通?；跀?shù)理邏輯的方法根本不同，首次實(shí)現(xiàn)了高效的幾何定理自動(dòng)證明，顯現(xiàn)了無(wú)比的優(yōu)越性。他的工作

7、被稱為自動(dòng)推理領(lǐng)域的先驅(qū)性工作，并于1997年獲得“herbrand自動(dòng)推理杰出成就獎(jiǎng)”。在授獎(jiǎng)辭中對(duì)他的工作給了這樣的介紹與評(píng)價(jià): “幾何定理自動(dòng)證明首先由赫伯特格蘭特(herbert gerlenter)于50年代開(kāi)始研究。雖然得到一些有意義的結(jié)果，但在吳方法出現(xiàn)之前的20年里，這一領(lǐng)域進(jìn)展甚微。在不多的自動(dòng)推理領(lǐng)域中，這種被動(dòng)局面是由一個(gè)人完全扭轉(zhuǎn)的。吳文俊很明顯是這樣一個(gè)人。他將幾何定理證明從一個(gè)不太成功的領(lǐng)域變?yōu)樽畛晒Φ念I(lǐng)域之一。”,15,2006年，著名數(shù)學(xué)家吳文俊榮獲邵逸夫數(shù)學(xué)科學(xué)獎(jiǎng)。邵逸夫數(shù)學(xué)科學(xué)獎(jiǎng)是一項(xiàng)國(guó)際性大獎(jiǎng)，它的評(píng)委是來(lái)自國(guó)際數(shù)學(xué)界的知名權(quán)威。吳文俊說(shuō)：這次邵逸夫獎(jiǎng)的評(píng)

8、委都是國(guó)際上有影響的大家，他們宣布我獲得邵逸夫獎(jiǎng)，是因?yàn)槲业臄?shù)學(xué)機(jī)械化問(wèn)題的研究，這實(shí)際上是國(guó)際數(shù)學(xué)界對(duì)數(shù)學(xué)機(jī)械化研究的承認(rèn)與肯定，它比獎(jiǎng)金重要得多。,數(shù)學(xué)機(jī)械化得到國(guó)際數(shù)學(xué)界承認(rèn),16,吳文俊我的不等式片斷,17,三角形三條高線交于一點(diǎn)的代數(shù)證明,d是bc和ca上高線交點(diǎn),18,定理的假設(shè)部分是,由吳方法，可得非退化條件是,. 定理的結(jié)論是 co經(jīng)過(guò)d點(diǎn),. 顯然在非退化條件下定理成立。,19,morley定理,任意三角形中，一個(gè)角的三等分線，與和它相鄰的角的三等分線相交，交點(diǎn)組成正三角形。,20,機(jī)器方法容易證明morley定理,任意三角形中，一個(gè)角的三等分線，與和它相鄰的角的三等分線相交

9、，按一定的規(guī)則選取交點(diǎn)，共可組成27個(gè)三角形，在這27個(gè)三角形中，一定有18個(gè)是正三角形。 用機(jī)器方法容易證明這個(gè)更一般的morley定理。在證明過(guò)程中，多次出現(xiàn)關(guān)于12個(gè)變量的含有一千多項(xiàng)的多項(xiàng)式。,21,吳方法概要,定理的假設(shè)相當(dāng)于一組多項(xiàng)式方程 定理的結(jié)論相當(dāng)于一個(gè)多項(xiàng)式方程 上面的諸fi稱為假設(shè)多項(xiàng)式，g稱為終結(jié)多項(xiàng)式。,22,吳方法概要（續(xù)）,吳方法是給出了一個(gè)機(jī)械化方法，在有限步內(nèi)給出一組非退化條件多項(xiàng)式d1, , dr 又根據(jù)這一機(jī)械化方法足以在有限步內(nèi)，判定在非退化條件 d10, , dr 0 下，g=0是否可從f1=0, , fs=0推出。,23,平行四邊形對(duì)角線互相平分,2

10、4,題設(shè)和結(jié)論表成代數(shù)形式,25,吳方法的處理,題設(shè)部分三角化，得到三個(gè)多項(xiàng)式： 再把結(jié)論左邊的多項(xiàng)式除以f3，所得的余式除以f2，所得的余式除以f1，看最后所得的余式是不是恒等于零。,26,中國(guó)古代數(shù)學(xué)的貢獻(xiàn),70 年代初，吳文俊開(kāi)始研讀中國(guó)數(shù)學(xué)史。1975 年，他撰寫(xiě)了中國(guó)古代數(shù)學(xué)對(duì)世界文化的偉大貢獻(xiàn)，文中詳細(xì)列舉在代數(shù)、幾何、三角、解析幾何和微積分等學(xué)科的發(fā)現(xiàn)和創(chuàng)立過(guò)程中，中國(guó)傳統(tǒng)數(shù)學(xué)所起的重大作用。 吳文俊指出，中國(guó)傳統(tǒng)數(shù)學(xué)注意解方程，在代數(shù)學(xué)、幾何學(xué)、極限概念等方面既有豐碩的成果，又有系統(tǒng)的理論。,27,中國(guó)古代數(shù)學(xué)的特色,中國(guó)傳統(tǒng)數(shù)學(xué)強(qiáng)調(diào)構(gòu)造性和算法化，注意解決科學(xué)實(shí)驗(yàn)和生產(chǎn)實(shí)踐中

11、提出的各類問(wèn)題，往往把所得到的結(jié)論以各種原理的形式予以表述。 在中國(guó)古代，求兩數(shù)最大公約數(shù)即等數(shù)用更相減損之術(shù)。如求24與15的等數(shù)，其逐步減損如下： （24，15）（9，15）（9，6）（3，6）（3，3） 其理由不證自明。 中國(guó)傳統(tǒng)數(shù)學(xué)在從問(wèn)題出發(fā)以解決問(wèn)題為主旨的發(fā)展過(guò)程中建立了以構(gòu)造性與機(jī)械化為其特色的算法體系， 九章算術(shù)與劉徽的九章算術(shù)注是這一機(jī)械化體系的代表作，這與西方數(shù)學(xué)以歐幾里得幾何原本為代表的所謂公理化演繹體系正好遙遙相對(duì)。,28,機(jī)械化思想是中國(guó)古代數(shù)學(xué)的精髓,吳文俊把中國(guó)傳統(tǒng)數(shù)學(xué)的思想概括為機(jī)械化思想，指出它是貫穿于中國(guó)古代數(shù)學(xué)的精髓。他列舉大量事實(shí)說(shuō)明，中國(guó)傳統(tǒng)數(shù)學(xué)的機(jī)

12、械化思想為近代數(shù)學(xué)的建立和發(fā)展做出了不可磨滅的貢獻(xiàn)。 這種機(jī)械化思想，不僅曾深刻影響了數(shù)學(xué)的歷史進(jìn)程，而且對(duì)數(shù)學(xué)的現(xiàn)狀也正在發(fā)揚(yáng)它日益顯著的影響。,29,數(shù)學(xué)機(jī)械化的廣泛應(yīng)用,吳文俊特別重視數(shù)學(xué)機(jī)械化方法的應(yīng)用，明確提出“數(shù)學(xué)機(jī)械化方法的成功應(yīng)用，是數(shù)學(xué)機(jī)械化研究的生命線”。他不斷開(kāi)拓新的應(yīng)用領(lǐng)域，如控制論、曲面拼接問(wèn)題、機(jī)構(gòu)設(shè)計(jì)、化學(xué)平衡問(wèn)題、平面天體運(yùn)行的中心構(gòu)形等，還建立了解決全局優(yōu)化問(wèn)題的新方法。 吳方法還被用于若干高科技領(lǐng)域，得到一系列國(guó)際領(lǐng)先的成果，包括曲面造型、機(jī)器人結(jié)構(gòu)的位置分析、智能計(jì)算機(jī)輔助設(shè)計(jì)(cad)、信息傳輸中的圖像壓縮等。,30,從開(kāi)普勒定律到牛頓定律,開(kāi)普勒定律為

13、 （1）行星繞太陽(yáng)以橢圓軌道運(yùn)行，太陽(yáng)為一焦點(diǎn) （2）太陽(yáng)到行星的向量在相同的時(shí)間掃過(guò)相同的 面積 牛頓定律為 （3）行星的加速度與太陽(yáng)到行星的距離的平方成反比 利用吳方法在微分域上的推廣，可以從開(kāi)普勒經(jīng)驗(yàn)公式自動(dòng)推導(dǎo)出牛頓定律。,31,機(jī)器人與連桿機(jī)構(gòu)的運(yùn)動(dòng)分析,如圖，綠色的平臺(tái)是活動(dòng)平臺(tái)，下面的平臺(tái)是固定的，六根連桿長(zhǎng)度可變，求連桿長(zhǎng)度變化時(shí)平臺(tái)上一點(diǎn)的 軌跡。,32,機(jī)器人與連桿機(jī)構(gòu)的運(yùn)動(dòng)分析,已知連桿機(jī)構(gòu)的構(gòu)成，求該機(jī)構(gòu)上某一點(diǎn)的軌跡及該點(diǎn)的位置與連桿機(jī)構(gòu)的關(guān)系，這類問(wèn)題稱為機(jī)械設(shè)計(jì)中的正解問(wèn)題。前面的例子就是一個(gè)正解問(wèn)題。 反過(guò)來(lái)，求解連桿機(jī)構(gòu)的參數(shù)使得連桿機(jī)構(gòu)上一點(diǎn)恰好位于空間指定

14、位置的問(wèn)題稱為機(jī)械設(shè)計(jì)中的逆解問(wèn)題。 這兩類問(wèn)題都可以看成方程求解問(wèn)題。 吳文俊用特征集方法解決了一般puma型機(jī)器人的逆解問(wèn)題，研究了四連桿的設(shè)計(jì)問(wèn)題。,33,曲面連接問(wèn)題,在幾何設(shè)計(jì)中，有一大類問(wèn)題要確定一給定次數(shù)的 代數(shù)曲面按一定要求連接已給的若干代數(shù)曲面。 這類問(wèn)題可以用吳方法解決。,左圖是一個(gè)連接 三根管道的例子。,34,腦力勞動(dòng)的機(jī)械化,在新的正在到來(lái)的工業(yè)革命中，可以認(rèn)為是以某種設(shè)備代替人腦。這將使人類艱苦思考的價(jià)值為之降低，是一種腦力勞動(dòng)的機(jī)械化。這種機(jī)械化由于上世紀(jì)中葉計(jì)算機(jī)的發(fā)明而有某種可能。 數(shù)學(xué)是一種典型的腦力勞動(dòng)。由于數(shù)學(xué)思維具有其它思維方式所沒(méi)有的簡(jiǎn)潔、明確、嚴(yán)密、清晰等優(yōu)點(diǎn)，因而數(shù)學(xué)的機(jī)械化比之其它思維的機(jī)械化，應(yīng)有它的優(yōu)越性與優(yōu)先性，而且應(yīng)更為容易。吳方法在幾何定理證明方面機(jī)械化的成功，正好說(shuō)明確是如此。,35,機(jī)械化思想促進(jìn)數(shù)學(xué)發(fā)展,線性方程組求解中的消去法是機(jī)械化思想的杰作。即使是現(xiàn)代純粹數(shù)學(xué)研究中，機(jī)械化思想也一直發(fā)揮重大的作用。例如，希爾伯特倡導(dǎo)的數(shù)理邏輯為計(jì)算機(jī)的設(shè)計(jì)原理作了準(zhǔn)備。h. cartan關(guān)于代數(shù)拓?fù)鋵W(xué)同調(diào)群計(jì)算的工作可以看作是機(jī)械化思想的成功范例。 運(yùn)用機(jī)械化思想考察數(shù)學(xué)，將會(huì)發(fā)現(xiàn)數(shù)學(xué)的不同側(cè)面，建立新的模式，活躍和啟迪數(shù)學(xué)家的思維，從而產(chǎn)生大量的原始創(chuàng)新。 機(jī)械化可以使得大量繁復(fù)的事情交給計(jì)算機(jī)去做，