愛(ài)華網(wǎng)一、機(jī)器證明：古老的夢(mèng)想
相傳 Ptolemy 王曾向 Euclid 請(qǐng)教學(xué)習(xí)幾何的捷徑， Euclid沒(méi)有屈從帝王的尊嚴(yán)，直率地說(shuō)：幾何中無(wú)王者之路 ( There is no royalway in geometry ) 。
以希臘的幾何學(xué)為代表的古代西方數(shù)學(xué)，其特點(diǎn)是在構(gòu)造公理體系的基礎(chǔ)上證明各式各樣的幾何命題。幾何題的證法，各具巧思，爭(zhēng)奇斗艷，無(wú)定法可循，只有依賴個(gè)人的經(jīng)驗(yàn)、技巧和靈感。學(xué)習(xí)幾何的孩子做夢(mèng)都在想：要是幾何題象解一元二次方程那樣多好。這種愿望由來(lái)已久，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ù)化。
比 Descartes 晚一些的德國(guó)數(shù)學(xué)家 Leibnize曾有過(guò)“推理機(jī)器”的設(shè)想。他研究過(guò)邏輯，設(shè)計(jì)并制造出能做乘法的計(jì)算機(jī)，進(jìn)而萌發(fā)了設(shè)計(jì)萬(wàn)能語(yǔ)言和造一臺(tái)通用機(jī)器的構(gòu)想。Leibnize認(rèn)為，他的方案一旦實(shí)現(xiàn)，人們之間的一切爭(zhēng)論都可以被心平氣和的機(jī)器推理所代替。他的努力促進(jìn)了Boole代數(shù)、數(shù)理邏輯以及計(jì)算機(jī)科學(xué)的研究，正是沿著這一方向，經(jīng)后人的努力，形成了機(jī)器定理證明的邏輯方法。
更晚一些，德國(guó)數(shù)學(xué)家 Hilbert明確提出了公理系統(tǒng)中的判定問(wèn)題：有了一個(gè)公理系統(tǒng)，就可以在這個(gè)系統(tǒng)基礎(chǔ)上提出各式各樣的命題，那么，有沒(méi)有一種機(jī)械的方法，即所謂算法，對(duì)每一個(gè)命題加以檢驗(yàn)，判明它是否成立呢？正是在Hilbert的名著《幾何基礎(chǔ)》一書中就提供了一條可以對(duì)一類幾何命題進(jìn)行判定的定理— 當(dāng)然，在那個(gè)時(shí)代，不僅 Hilbert本人，整個(gè)數(shù)學(xué)界都沒(méi)有意識(shí)到這一點(diǎn)。
數(shù)理邏輯的研究表明， Hilbert 的要求太高了。著名的 Godel不完全定理斷言：即使在初等數(shù)論的范圍內(nèi)，對(duì)所有命題進(jìn)行判定的機(jī)械化方法也是不存在的！
數(shù)學(xué)大師們堅(jiān)持不懈地求索，表明數(shù)學(xué)機(jī)械化的思想重要而深刻；而數(shù)學(xué)機(jī)械化在歷史上發(fā)展緩慢，同時(shí)也意味著這一方向道路漫長(zhǎng)而艱難。
證明的機(jī)械化，如果沒(méi)有可以進(jìn)行數(shù)學(xué)演算的機(jī)器，只能是紙上談兵。電子計(jì)算機(jī)的問(wèn)世，促使數(shù)學(xué)機(jī)械化的研究活躍起來(lái)。波蘭數(shù)學(xué)家Tarski 在 1950 年推廣了關(guān)于代數(shù)方程實(shí)根數(shù)目的 Sturm法則，由此證明了一個(gè)引人注目的定理：“一切初等幾何和初等代數(shù)范圍的命題，都可以用機(jī)械方法判定?！笨上姆椒ㄌ珡?fù)雜，即使用高速計(jì)算機(jī)也證明不了稍難的幾何定理。
1959年，著名數(shù)理邏輯學(xué)家，美國(guó)洛克菲勒大學(xué)王浩教授設(shè)計(jì)了一個(gè)程序，用計(jì)算機(jī)證明了Russell 、 Whitehead的巨著《數(shù)學(xué)原理》中的幾百條有關(guān)命題邏輯的定理，僅用了 9分鐘。王浩工作的意義在于宣告了用計(jì)算機(jī)進(jìn)行定理證明的可能性。特別的是，他第一次明確提出“走向數(shù)學(xué)的機(jī)械化”（Toward Mechanical Mathematics ）。 1976年，美國(guó)兩位年輕的數(shù)學(xué)家在高速電子計(jì)算機(jī)上耗費(fèi) 1 200小時(shí)的計(jì)算時(shí)間，證明了“四色定理”，使數(shù)學(xué)家們 100年來(lái)未能解決的難題得到肯定的回答。
在數(shù)學(xué)發(fā)展的漫長(zhǎng)歷史中，積累了無(wú)數(shù)的幾何定理。這里面有許多巧奪天功、趣味雋永的杰作。由于傳統(tǒng)的興趣和應(yīng)用的價(jià)值，初等幾何問(wèn)題的自動(dòng)求解遂為數(shù)學(xué)機(jī)械化的研究焦點(diǎn)。自Tarski 的引人注目的定理發(fā)表以來(lái)，已經(jīng) 26年過(guò)去了，初等幾何定理的機(jī)器證明，仍然沒(méi)有令人滿意的進(jìn)展。在經(jīng)過(guò)許多探索和失敗之后，人們?cè)诒瘒@：光靠機(jī)器，再過(guò)100 年也未必能證明出多少有意義的新定理來(lái)！
吳文俊的工作，揭開(kāi)了機(jī)器證明領(lǐng)域的新的一頁(yè)。
二、吳方法：王者之路
當(dāng)中國(guó)的歷史艱難地走出十年浩劫的磨難的時(shí)候， 1977年，吳文俊在《中國(guó)科學(xué)》上發(fā)表的論文《初等幾何判定問(wèn)題與機(jī)械化問(wèn)題》，為數(shù)學(xué)機(jī)械化領(lǐng)域送去了一縷清新的春風(fēng)。1984年，吳文俊的學(xué)術(shù)專著《幾何定理機(jī)器證明的基本原理》由科學(xué)出版社出版，這部專著遵循機(jī)械化思想引進(jìn)數(shù)系和公理，依照機(jī)械化觀點(diǎn)系統(tǒng)地分析了各類幾何體系，明確建立了各類幾何的機(jī)械化定理，著重闡明幾何定理機(jī)械化證明的基本原理。1985年，吳文俊的論文《關(guān)于代數(shù)方程組的零點(diǎn)》發(fā)表，具體討論了多項(xiàng)式方程組所確定的零點(diǎn)集。這篇重要文獻(xiàn)，是正式建立求解多項(xiàng)式方程組的吳文俊消元法的重要標(biāo)志。與國(guó)際上流行的代數(shù)理想論不同，明確提出了具有中國(guó)自己特色的、以多項(xiàng)式零點(diǎn)集為基本點(diǎn)的學(xué)術(shù)路線。自此，“吳方法”宣告誕生，數(shù)學(xué)機(jī)械化研究揭開(kāi)了她新的一幕。
幾何問(wèn)題的代數(shù)化是幾何問(wèn)題機(jī)械化的第一步，為此需要引進(jìn)數(shù)系，建立坐標(biāo)系，把幾何命題的圖中的各種關(guān)系利用代數(shù)方程來(lái)描述。在適當(dāng)選取坐標(biāo)系后，如果幾何定理的假設(shè)條件可表示為一組代數(shù)方程[H] ： f 1 = 0 ， f 2 = 0 ， …， f r= 0 ，而幾何定理的結(jié)論由代數(shù)方程C : g = 0 所刻畫，這里 f 1 , f 2 ,… , fr 和 g 都是變?cè)?x 1 ,x 2 ,…,x n的多項(xiàng)式，那么幾何定理的機(jī)械化證明就歸結(jié)為如下問(wèn)題：
機(jī)械化問(wèn)題構(gòu)造并提供一種確定的、機(jī)械的算法，使得依此算法進(jìn)行有限步之后即可判定：在若干附加條件之下，結(jié)論C 是否可由假設(shè) [H] 推出，即是否可由 f 1 = 0 ， f 2= 0 ， ……
f r= 0 推出 g = 0 。
由此可見(jiàn)，實(shí)現(xiàn)數(shù)學(xué)定理機(jī)械化證明的關(guān)鍵，在于必須對(duì)表示定理假設(shè)的多項(xiàng)式組[H] 的零點(diǎn)集給出構(gòu)造性的描述 , 以便區(qū)分多項(xiàng)式組 [H] 的零點(diǎn)集 ,從而可以確定在多項(xiàng)式組 [H] 零點(diǎn)集的哪部分之中 , 能夠保證多項(xiàng)式g =0.吳文俊消元法（吳方法）恰恰完成了這項(xiàng)任務(wù)。因此，吳方法是定理機(jī)器證明吳文俊原理的理論基礎(chǔ)，定理機(jī)器證明的機(jī)械化原理的建立是吳方法的成功運(yùn)用。
吳文俊原理 設(shè)數(shù)學(xué)定理的假設(shè)條件由多項(xiàng)式方程組[H] ＝ 0 表示，定理的結(jié)論由多項(xiàng)式方程 g =0 表示。并設(shè) CS＝ {A 1,A 2,….,A k} 為多項(xiàng)式方程組 [H] 的特征列。如果多項(xiàng)式g 對(duì) [H] 的特征列 CS 的余式 R=0, 則在條件 I i ≠0, i=1,2,…,k 之下 , 可從 [H]=0 推出 g =0 。
條件 I i ≠ 0, i=1,2,…,k稱為數(shù)學(xué)定理成立的非退化條件。這組非退化條件是在計(jì)算特征列過(guò)程中自動(dòng)產(chǎn)生的。非退化條件這一概念的發(fā)現(xiàn), 是吳文俊在數(shù)學(xué)機(jī)械化證明領(lǐng)域的突出貢獻(xiàn)。這一概念的引進(jìn) ,實(shí)現(xiàn)了數(shù)學(xué)定理機(jī)器證明的決定性突破。
一般說(shuō)來(lái) , 用吳方法判定一個(gè)命題 , 要分三步進(jìn)行 :第一步是把所給命題化為代數(shù)形式，即判定一組多項(xiàng)式的公共零點(diǎn)集是否被包含于另一多項(xiàng)式的零點(diǎn)集的問(wèn)題; 第二步是整序，即把刻劃命題條件的多項(xiàng)式組 [H] 經(jīng)整序化為升列 AS；第三步是求余，即將刻劃命題結(jié)論的多項(xiàng)式 g 對(duì)于升列 AS約化求取余式 R 。 若 R=0 ，即可斷定命題在非退化條件 I i ≠0, i=1,2,…,k 之下成立，或者說(shuō)命題一般成立，其中 I 1, I 2,…, I k是升列 AS 中各多項(xiàng)式的初式。若 R 不為 0, 則當(dāng) AS 為不可約升列時(shí) ,可斷定命題不真。
多項(xiàng)式方程組求解曾被認(rèn)為是極為困難的問(wèn)題 ,這已為它的研究歷史過(guò)程所證明。但是 ,吳文俊消元法的敘述簡(jiǎn)明自然，順理成章，結(jié)論易懂，方法易學(xué)?？梢杂孟喈?dāng)短的時(shí)間向初學(xué)者介紹吳方法，并在計(jì)算機(jī)上具體操作吳方法的計(jì)算過(guò)程。初學(xué)者往往驚奇的發(fā)現(xiàn)：吳方法竟是這樣的簡(jiǎn)單自然，感嘆為什么別人沒(méi)有發(fā)現(xiàn)它！事實(shí)上，將公認(rèn)的難題，應(yīng)用初等方法簡(jiǎn)樸自然地加以解決，是數(shù)學(xué)科學(xué)返璞歸真的最高境界。
三、《九章算術(shù)》：惟有源頭活水來(lái)
50年代，拓?fù)鋵W(xué)剛剛從艱難遲緩的發(fā)展中走向突飛猛進(jìn)，吳文俊敏銳地抓住了拓?fù)鋵W(xué)的核心問(wèn)題，在示性類與示嵌類的研究上取得了國(guó)際數(shù)學(xué)界交相稱譽(yù)的突出成就。1956 年榮獲國(guó)家自然科學(xué)一等獎(jiǎng)， 1957年當(dāng)選為中國(guó)科學(xué)院學(xué)部委員（現(xiàn)稱院士）。那時(shí)他才 38歲。作為一位年輕的數(shù)學(xué)家，這已是莫大的榮譽(yù)了。而對(duì)吳文俊來(lái)說(shuō)，這只是在西方人開(kāi)創(chuàng)的方向上做出的工作，新中國(guó)的數(shù)學(xué)家應(yīng)該開(kāi)拓出屬于自己的研究領(lǐng)域。
但是，路在何方呢？那就是數(shù)學(xué)機(jī)械化！是什么力量使得吳文俊從一位卓有成就的拓?fù)鋵W(xué)家，走上數(shù)學(xué)機(jī)械化的研究道路呢？吳文俊在《吳文俊文集》前言中有過(guò)動(dòng)情的敘述：
作者關(guān)于機(jī)械化思想的形成，決非一朝一夕，至少在 70年代以前，機(jī)械化的概念在作者腦海里還毫無(wú)蹤影。經(jīng)過(guò)對(duì)中國(guó)古代數(shù)學(xué)的學(xué)習(xí)和觸發(fā)，結(jié)合著幾十年來(lái)在數(shù)學(xué)研究道路上探索實(shí)踐的回顧與分析，終于形成了這種數(shù)學(xué)機(jī)械化的思想。這種思想一旦形成，就自然地化成一股頑強(qiáng)的動(dòng)力。十幾年來(lái)，作者一直在這一方向道路上摸索前進(jìn)，艱苦奮斗，義無(wú)反顧。
70年代初，吳文俊開(kāi)始研讀中國(guó)數(shù)學(xué)史。中國(guó)古代數(shù)學(xué)曾有過(guò)輝煌的歷史，直到14世紀(jì)，在許多數(shù)學(xué)領(lǐng)域都保持西方望塵莫及的水平。但是，西方一些數(shù)學(xué)史家不了解也不承認(rèn)中國(guó)古代數(shù)學(xué)的光輝成就，將其排斥于“數(shù)學(xué)主流”之外。吳文俊對(duì)此作了正本清源的研究。1975年，他撰寫了《中國(guó)古代數(shù)學(xué)對(duì)世界文化的偉大貢獻(xiàn)》，文中詳細(xì)列舉在代數(shù)、幾何、三角、解析幾何和微積分等學(xué)科的發(fā)現(xiàn)和創(chuàng)立過(guò)程中，中國(guó)傳統(tǒng)數(shù)學(xué)所起的重大作用，吳文俊認(rèn)為：近代數(shù)學(xué)之所以能夠發(fā)展到今天，主要是靠中國(guó)的數(shù)學(xué)，而非希臘的數(shù)學(xué)，決定數(shù)學(xué)歷史發(fā)展進(jìn)程的主要是中國(guó)的數(shù)學(xué)而非希臘的數(shù)學(xué)。這一論斷在當(dāng)時(shí)真可謂空谷驚雷，振聾發(fā)聵。此后，吳文俊對(duì)中國(guó)數(shù)學(xué)史的研究一發(fā)而不可收。大約在 1976年，他的論文《我國(guó)古代測(cè)望之學(xué)重差理論評(píng)價(jià)—兼評(píng)數(shù)學(xué)史研究中某些方法問(wèn)題》洋洋灑灑3 萬(wàn)余言，列舉參考文獻(xiàn)達(dá) 48種，從古代“重差理論”入手，見(jiàn)微知著，批判了數(shù)學(xué)史研究中“以今代古”所產(chǎn)生的巴比倫神話、印度神話以及丟番圖神話；正是在此文中，吳文俊意識(shí)到“幾何與代數(shù)的配合、代數(shù)的幾何應(yīng)用與幾何的代數(shù)化正是宋元天元術(shù)的主要含義”，指出“在宋元數(shù)學(xué)家的手里為了發(fā)展天元術(shù)而建立了一整套的代數(shù)機(jī)器”。這為他日后機(jī)器證明思想埋下了伏筆。隨后的另一篇文章《〈海島算經(jīng)〉古證探源》，提出了古證復(fù)原的三項(xiàng)原則，在數(shù)學(xué)史界引起了強(qiáng)烈反響。1986 年，吳文俊應(yīng)邀在國(guó)際數(shù)學(xué)家大會(huì)做 45分鐘報(bào)告，作為國(guó)際著名的數(shù)學(xué)家，吳文俊的報(bào)告卻是“近年來(lái)中國(guó)數(shù)學(xué)史的研究”。吳文俊熱情謳歌中國(guó)古代數(shù)學(xué)的代表作《九章算術(shù)》。在他主編的《〈九章算術(shù)〉與劉徽》的前言中，他寫到：“《九章算術(shù)》是我國(guó)數(shù)學(xué)方面流傳至今最早也是最重要的一部經(jīng)典著作。它承前啟后，一方面總結(jié)了秦漢以前的數(shù)學(xué)成就，另一方面又成為漢代以來(lái)達(dá)兩千年之久數(shù)學(xué)研究與創(chuàng)造的源泉。特別是三國(guó)時(shí)期劉徽的《九章算術(shù)注》，對(duì)數(shù)學(xué)理論多所闡發(fā)，影響深遠(yuǎn)。總之，《九章算術(shù)》與劉徽《九章算術(shù)注》，對(duì)數(shù)學(xué)發(fā)展在歷史上的崇高地位，足以與古希臘的歐幾里得《幾何原本》東西輝映，各具特色”。他進(jìn)一步指出：“作為一名中國(guó)的數(shù)學(xué)工作者，首先應(yīng)該對(duì)自己的數(shù)學(xué)歷史有深刻的認(rèn)識(shí)，為此必須首先對(duì)《九章算術(shù)》與劉徽《九章算術(shù)注》有確切的了解?！薄耙A(yù)見(jiàn)數(shù)學(xué)的將來(lái)，不能不研究《九章算術(shù)》與《九章算術(shù)注》所蘊(yùn)含的深邃的思想在數(shù)學(xué)發(fā)展過(guò)程中的歷史功績(jī)，也不能不正視正在展露頭角的這種思想對(duì)數(shù)學(xué)現(xiàn)狀的影響”。
吳文俊以一位數(shù)學(xué)家的素養(yǎng)敏銳地感受到中國(guó)傳統(tǒng)數(shù)學(xué)“寓理于算”鮮明特點(diǎn)表現(xiàn)在它的機(jī)械化和構(gòu)造性，他在論文《從〈數(shù)書九章〉看中國(guó)傳統(tǒng)數(shù)學(xué)構(gòu)造性與機(jī)械化的特色》中著力闡明了這一點(diǎn)。后來(lái)在為數(shù)學(xué)史家李繼閔先生的著作《〈九章算術(shù)〉及其劉徽注研究》作序時(shí)，他把自己多年研究數(shù)學(xué)史的體會(huì)系統(tǒng)完整地表述出來(lái)，他指出：
我國(guó)傳統(tǒng)數(shù)學(xué)在從問(wèn)題出發(fā)以解決問(wèn)題為主旨的發(fā)展過(guò)程中建立了以構(gòu)造性與機(jī)械化為其特色的算法體系，這與西方數(shù)學(xué)以歐幾里得《幾何原本》為代表的所謂公理化演繹體系正好遙遙相對(duì)?！毒耪隆放c《劉注》是這一機(jī)械化體系的代表作，與公理化的代表作歐幾里得《幾何原本》可謂東西輝映，在數(shù)學(xué)發(fā)展的歷史長(zhǎng)河中，數(shù)學(xué)機(jī)械化算法體系與數(shù)學(xué)公理化演繹體系曾多次反復(fù)互為消長(zhǎng)，交替成為數(shù)學(xué)發(fā)展中的主流。肇始于我國(guó)的這種機(jī)械化體系，在經(jīng)過(guò)明代以來(lái)近幾百年的相對(duì)消沉后，勢(shì)必重新登上歷史舞臺(tái)?！毒耪隆放c《劉注》所貫穿的機(jī)械化思想，不僅曾深刻影響了數(shù)學(xué)的歷史進(jìn)程，而且對(duì)數(shù)學(xué)的現(xiàn)狀也正在發(fā)揚(yáng)它日益顯著的影響。它在進(jìn)入21 世紀(jì)后在數(shù)學(xué)中的地位，幾乎可以預(yù)卜。
也就是在這個(gè)時(shí)期，吳文俊到計(jì)算機(jī)工廠勞動(dòng)，通過(guò)接觸計(jì)算機(jī)，切身體會(huì)到了計(jì)算機(jī)的巨大威力，敏銳地覺(jué)察到計(jì)算機(jī)有極大的發(fā)展?jié)撃堋Ｋ活^扎進(jìn)機(jī)房，從HP-1000機(jī)型開(kāi)始，學(xué)習(xí)算法語(yǔ)言，編制算法程序。就這樣，中國(guó)數(shù)學(xué)史的啟發(fā)，“玩”計(jì)算機(jī)的感受，更是幾十年在數(shù)學(xué)研究道路上的探索與實(shí)踐，終于在吳文俊的腦海里升華為數(shù)學(xué)機(jī)械化的思想。1977年，吳文俊的論文《初等幾何判定問(wèn)題與機(jī)械化證明》發(fā)表于《中國(guó)科學(xué)》，吳文俊特地為此文寫了一個(gè)附注，闡明機(jī)械化思想起源：
我們關(guān)于初等幾何定理機(jī)械化證明所用的算法，主要牽涉到一些多項(xiàng)式的運(yùn)用技術(shù)，例如算術(shù)運(yùn)算與簡(jiǎn)單消元法之類。應(yīng)該指出，這些都是12 至 14 世紀(jì)宋元時(shí)期中國(guó)數(shù)學(xué)家的創(chuàng)造，在那時(shí)已由相當(dāng)高度的發(fā)展?！?事實(shí)上 , 幾何問(wèn)題的代數(shù)化與用代數(shù)方法系統(tǒng)求解 ,乃是當(dāng)時(shí)中國(guó)數(shù)學(xué)家主要成就之一 , 其時(shí)間遠(yuǎn)在 17世紀(jì)出現(xiàn)解析幾何之前。
吳文俊汲取中華民族燦爛文化之精華，發(fā)揚(yáng)中國(guó)古代數(shù)學(xué)的優(yōu)良傳統(tǒng)，創(chuàng)造了世所公認(rèn)的機(jī)器證明的“吳方法”，徹底改變了數(shù)學(xué)機(jī)械化領(lǐng)域的面貌。吳文俊的卓越建樹(shù)，生動(dòng)的證明了這樣一個(gè)真理：正確認(rèn)識(shí)和研究數(shù)學(xué)的歷史，不僅是數(shù)學(xué)發(fā)展的必然要求，也是一個(gè)數(shù)學(xué)家永葆學(xué)術(shù)青春的重要源泉之一。
四、數(shù)學(xué)機(jī)械化：無(wú)盡的前沿
Fourier曾有過(guò)這樣的名言“對(duì)自然的深入研究，是數(shù)學(xué)發(fā)現(xiàn)最豐富的源泉”。然而，這還是不夠的，還應(yīng)該加上這樣的續(xù)言：數(shù)學(xué)內(nèi)容的不斷豐富和在更深層次的成熟發(fā)展，必然對(duì)自然界的認(rèn)識(shí)、理解和改造產(chǎn)生更大的作用。
吳文俊所倡導(dǎo)的數(shù)學(xué)機(jī)械化研究，一方面繼承了古代中國(guó)數(shù)學(xué)思想的精華，一方面適應(yīng)了現(xiàn)代科學(xué)技術(shù)的發(fā)展。數(shù)學(xué)機(jī)械化的研究最先在幾何定理機(jī)器證明取得了突破性的成果，隨著時(shí)間的推移、工作的積累和方向的拓展，數(shù)學(xué)機(jī)械化必將為中國(guó)乃至世界數(shù)學(xué)的發(fā)展做出積極的貢獻(xiàn)，也必將使數(shù)學(xué)更好地為科學(xué)技術(shù)服務(wù)，尤其是為高科技提供理論武器和有效的工具。從幾何的機(jī)器證明到內(nèi)容更為豐富的數(shù)學(xué)機(jī)械化是一種必然的趨勢(shì)。這里采擷幾朵絢麗的奇葩，以展示數(shù)學(xué)機(jī)械化的應(yīng)用和它對(duì)當(dāng)代高科技的影響。
物理規(guī)律的發(fā)現(xiàn)數(shù)學(xué)在解釋物理現(xiàn)象、解決物理問(wèn)題方面所處的重要地位是毋庸置疑的。今天，科學(xué)家們對(duì)于借助計(jì)算機(jī)和數(shù)學(xué)理論來(lái)發(fā)現(xiàn)物理規(guī)律的熱情依舊不減。
在科學(xué)史上， Newton 通過(guò)觀測(cè)和試驗(yàn)從 Kepler定律導(dǎo)出萬(wàn)有引力定律是一個(gè)重要的歷史事件。但是如何通過(guò)理論推導(dǎo)來(lái)重現(xiàn)Newton的偉大發(fā)現(xiàn)，這一點(diǎn)在現(xiàn)行的教科書里幾乎沒(méi)有觸及。相反地，教科書中大量介紹了如何從Newton 定律推導(dǎo) Kepler 定律。
1986 年吳文俊訪問(wèn)美國(guó) Argonne 國(guó)家試驗(yàn)室， Gabriel教授正為如何借助計(jì)算機(jī)和數(shù)學(xué)工具，從 Kepler 定律推導(dǎo)出 Newton定律而絞盡腦汁?；貒?guó)后，吳文俊用自己的方法，通過(guò)計(jì)算機(jī)，完成了這一推導(dǎo)工作，并因此博得了許多科學(xué)家的稱贊。國(guó)際自動(dòng)推理研究領(lǐng)域的著名科學(xué)家，Argonne 實(shí)驗(yàn)室的 Wos教授認(rèn)為，吳的這一貢獻(xiàn)對(duì)自動(dòng)定理證明領(lǐng)域是一次極為重要的拓廣，表現(xiàn)了吳的非凡的洞察力和卓越的智慧。進(jìn)一步的工作揭示，假設(shè)對(duì)Newton 定律一無(wú)所知，僅僅從 Kepler定律的微分代數(shù)方程描述出發(fā)，經(jīng)過(guò)整序運(yùn)算，計(jì)算機(jī)自動(dòng)產(chǎn)生了新的微分代數(shù)表達(dá)式，再加上一些技術(shù)性的分析，可以得到表達(dá)Newton 定律的微分代數(shù)表達(dá)式蘊(yùn)含在其中——也就是說(shuō)，在假設(shè) Kepler定律的前提下，用計(jì)算機(jī)自動(dòng)地發(fā)現(xiàn)了 Newton 定律， Newton多年的心血，現(xiàn)在只需一刻鐘的功夫，就重現(xiàn)于眼前，這真是一個(gè)激動(dòng)人心的結(jié)果！
機(jī)器人與機(jī)構(gòu)學(xué)機(jī)器人的制造是多學(xué)科共同發(fā)揮作用的復(fù)雜的系統(tǒng)工程。工業(yè)機(jī)器人的主體基本上是一只類似于人的上肢功能的機(jī)械手臂，或是無(wú)關(guān)節(jié)結(jié)構(gòu)，或是關(guān)節(jié)式結(jié)構(gòu)。如果要在三維空間對(duì)物體進(jìn)行作業(yè)，一般則需要具有六個(gè)自由度，即沿三個(gè)坐標(biāo)軸的直線移動(dòng)和繞這三軸的轉(zhuǎn)動(dòng)。例如，PUMA560機(jī)器人，就是六自由度關(guān)節(jié)型電動(dòng)機(jī)械手臂。對(duì)于這個(gè)具體的機(jī)器人，求解運(yùn)動(dòng)學(xué)方程，就是要決定各關(guān)節(jié)應(yīng)轉(zhuǎn)動(dòng)的角度q 1 , q 2 ,…, q 6 , 分別是多少 ?這需要解一組非線性方程組如果采用數(shù)值迭代方法，求解過(guò)程很慢，同時(shí)也不能保證求出所有的解。一個(gè)自然的問(wèn)題就是能否找出q i 的封閉解。雖然就 PUMA560來(lái)說(shuō)，封閉解已被決定，但是對(duì)于一般的 PUMA型機(jī)器人時(shí)，用吳文俊方法，依然可以求出特征列意義下的封閉解。而這是以往的方法很難達(dá)到的。
機(jī)構(gòu)學(xué)是現(xiàn)代各種機(jī)械設(shè)計(jì)的基礎(chǔ)，平面機(jī)構(gòu)運(yùn)動(dòng)學(xué)分析與綜合又是機(jī)構(gòu)學(xué)的基礎(chǔ)。此類問(wèn)題研究主要是依據(jù)德國(guó)學(xué)者L.Burmester 所建立的運(yùn)動(dòng)幾何學(xué)方法 ,按照這個(gè)理論，平面機(jī)構(gòu)綜合問(wèn)題有圖解法和解析法兩類。圖解法過(guò)程繁復(fù)，工作量很大且不精確；解析法建模復(fù)雜，求解也復(fù)雜；若用數(shù)值法求解，又不易得到全部解?，F(xiàn)在，借助于吳文俊整序方法，這類問(wèn)題已獲得了特征列形式的封閉解。
計(jì)算機(jī)科學(xué)中的應(yīng)用數(shù)學(xué)機(jī)械化在中國(guó)得以迅速發(fā)展，一個(gè)很重要的因素是計(jì)算機(jī)的介入?，F(xiàn)在，一個(gè)可喜的良性循環(huán)已經(jīng)形成，即數(shù)學(xué)機(jī)械化對(duì)于促進(jìn)計(jì)算機(jī)科學(xué)自身的發(fā)展，對(duì)于計(jì)算機(jī)科學(xué)中的一些應(yīng)用領(lǐng)域都產(chǎn)生了積極的影響,形成了投桃報(bào)李的局面。計(jì)算機(jī)視覺(jué)是一個(gè)重要的應(yīng)用研究領(lǐng)域。這一方面，任何有意義的新結(jié)果，必然會(huì)促進(jìn)機(jī)器人的發(fā)展。1988 年和 1991 年，紐約大學(xué)的 Kapur 教授和通用電氣公司的 Mundy博士，敏銳而快速的把中國(guó)人創(chuàng)立和發(fā)展的特征列方法引入高科技的應(yīng)用當(dāng)中。用Mundy博士自己的話“最近我們發(fā)覺(jué)把吳文俊三角化方法和求根技術(shù)結(jié)合起來(lái)，可以形成解非線性約束問(wèn)題的有效方法。我們?cè)诎堰@一方法用于機(jī)器視覺(jué)和過(guò)程控制”。
數(shù)學(xué)機(jī)械化與數(shù)學(xué)機(jī)械化數(shù)學(xué)是數(shù)學(xué)的一部分，隨著計(jì)算機(jī)大規(guī)模的滲透人們的生活，自然也改變了人們的學(xué)習(xí)、工作和從事研究的方式，一張紙、一支筆的情景基本上已成為歷史。機(jī)械化數(shù)學(xué)的努力就是要將數(shù)學(xué)的各個(gè)領(lǐng)域一部分一部分的機(jī)械化，從而使傳統(tǒng)數(shù)學(xué)的許多方面，由于有了數(shù)學(xué)機(jī)械化而面貌一新。這里僅列舉一二。
微分幾何、代數(shù)幾何是引人入勝的數(shù)學(xué)分支，它們不但在理論的發(fā)展長(zhǎng)河中考驗(yàn)了一大批杰出的數(shù)學(xué)家，在許多工程應(yīng)用中也起到了不可替代的作用。Clifford 代數(shù)與重要的 E.Cartan外微分運(yùn)算向結(jié)合，形成了局部微分幾何定理的機(jī)器證明的新算法，利用這一結(jié)果可以給出陳省身關(guān)于曲面論中一個(gè)十分深刻的定理的非常簡(jiǎn)單的證明。代數(shù)幾何中，在等價(jià)的意義下做分類，是非常重要且基本的問(wèn)題。在一維情形下，用機(jī)械化數(shù)學(xué)的方法，做出了同構(gòu)意義下的分類處理，是值得繼續(xù)擴(kuò)展成果的方向。
非線性發(fā)展方程的解，不僅僅是偏微分方程立論中關(guān)心的重要問(wèn)題，同時(shí)它還具有十分明顯的物理應(yīng)用背景，一些著名方程，如力學(xué)，固態(tài)物理、等離子體物理和化學(xué)物理等領(lǐng)域中出現(xiàn)的一類非線性波方程，需要求物理上有興趣的鐘狀、紐結(jié)狀的孤立波解?，F(xiàn)在已經(jīng)應(yīng)用特征列方法解過(guò)幾十個(gè)非線性波方程，非線性發(fā)展方程。所得結(jié)果除涵蓋已知解外，還發(fā)現(xiàn)了許多新解。
相輔相成、互惠互利，是機(jī)械化數(shù)學(xué)與一般數(shù)學(xué)關(guān)系的絕妙寫照。
1981年吳文俊在《數(shù)學(xué)的機(jī)械化與機(jī)械化的數(shù)學(xué)》一文中指出：“我們的研究工作還只是一個(gè)開(kāi)端。如何繼續(xù)發(fā)揚(yáng)中國(guó)古代傳統(tǒng)數(shù)學(xué)的機(jī)械特色，對(duì)數(shù)學(xué)各個(gè)不同領(lǐng)域探索實(shí)現(xiàn)機(jī)械化的數(shù)學(xué)，則是本世紀(jì)以致可能綿亙整個(gè)21 世紀(jì)才能大體趨于完善的事?！苯?20 年來(lái) ,在吳文俊的積極倡導(dǎo)下，中國(guó)的數(shù)學(xué)機(jī)械化研究已初現(xiàn)豐富多彩之勢(shì)。展望21世紀(jì)，我們有理由相信，機(jī)械化數(shù)學(xué)和數(shù)學(xué)機(jī)械化必將為數(shù)學(xué)以致整個(gè)科學(xué)注入新的活力。
參考文獻(xiàn)
- 吳文俊 . 吳文俊文集 . 濟(jì)南 : 山東教育出版社 , 1986
- 吳文俊 . 吳文俊論數(shù)學(xué)機(jī)械化 . 濟(jì)南 : 山東教育出版社 , 1996
- 吳文俊 . 初等幾何判定問(wèn)題與機(jī)械化證明 . 中國(guó)科學(xué) ,1977,507
- 吳文俊 . 幾何定理機(jī)器證明的基本原理 ( 初等幾何部分 ). 北京 :科學(xué)出版社 ,1984
- Wu Wen-tsun. Mathematics Mechanization. Beijing, SciencePress,China & Dordrecht, Kluwer Academic Publishers, TheNetherlands, 2000
- 吳文俊主編 . 王者之路 — 機(jī)器證明機(jī)器應(yīng)用 . 長(zhǎng)沙 :湖南科學(xué)技術(shù)出版社 ,1999
- 張景中 . 計(jì)算機(jī)怎樣解幾何題 — 談?wù)勛詣?dòng)推理 . 北京 :清華大學(xué)出版社 & 廣州 : 暨南大學(xué)出版社 ,2000
- 石赫 . 機(jī)械化數(shù)學(xué)引論 . 長(zhǎng)沙 : 湖南教育出版社 ,1998
- 程民德主編 . 中國(guó)數(shù)學(xué)發(fā)展的若干主攻方向 . 南京 : 江蘇教育出版社,1994
- 李繼閔 . 《九章算術(shù)》及其劉徽注研究 . 西安 : 陜西人民教育出版社,1990
愛(ài)華網(wǎng)本文地址 » http://www.klfzs.com/a/25101017/357519.html
