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

從吳文俊和吳方法談起一

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

1中國科學(xué)院院士第三世界科學(xué)院院士首屆國家最高科技獎(jiǎng)國家第一屆自然科學(xué)獎(jiǎng)

最高獎(jiǎng)一等獎(jiǎng)自動推理的最高獎(jiǎng)

Herbrand

獎(jiǎng)2006邵逸夫數(shù)學(xué)獎(jiǎng)吳文俊2中央電視臺《大家》欄目：《吳文俊

·我的不等式》片斷3什么是數(shù)學(xué)機(jī)械化所謂機(jī)械化，無非是刻板化和規(guī)格化。

數(shù)學(xué)

問題的機(jī)械化，就要求在運(yùn)算或證明過程中，

每前進(jìn)一步之后，都有一個(gè)確定的、必須選

擇的下一步，這樣沿著一條有規(guī)律的、刻板

的道路，

一直達(dá)到結(jié)論。使用一種機(jī)械化方法證明一類定理，才真正

體現(xiàn)了機(jī)械化定理證明。1977年，吳文俊給

出了初等幾何一類主要定理的機(jī)械化證明方法一“吳方法”。4數(shù)學(xué)機(jī)械化

：

從設(shè)想到實(shí)現(xiàn)希爾伯特萊布尼茨笛卡爾5數(shù)學(xué)機(jī)械化：從設(shè)想到實(shí)現(xiàn)吳文俊哥德爾塔斯基王浩6笛卡爾的設(shè)想17世紀(jì)法國的數(shù)學(xué)家

Descartes

曾有過一個(gè)偉大

的設(shè)想：

“一切問題化為數(shù)學(xué)問題，

一切數(shù)學(xué)問題

化為代數(shù)問題，

一切代數(shù)問題化為代數(shù)方程求解問

題。"Descartes

把問題想得太簡單了，如果他的設(shè)想真

能實(shí)現(xiàn)，那就不僅是數(shù)學(xué)的機(jī)械化，而是全部科學(xué)

的機(jī)械化。因?yàn)榇鷶?shù)方程求解是可以機(jī)械化的。但

Descartes

沒有停留在空想，他所創(chuàng)立的解析

幾何，在空間形式和數(shù)量關(guān)系之間架起了一座橋梁，實(shí)現(xiàn)了初等幾何問題的代數(shù)化。7萊布尼茲之夢德國數(shù)學(xué)家

Leibniz

曾有過“推理機(jī)器”的設(shè)想。他研究過邏輯，設(shè)計(jì)并制造出能做乘法的計(jì)算機(jī)，進(jìn)而萌發(fā)了設(shè)計(jì)萬能語言和造

一臺通用機(jī)器的構(gòu)想。他的努力促進(jìn)了

Boole

代數(shù)、數(shù)理邏輯以及計(jì)算機(jī)科學(xué)的研究，正是沿著這一方向，經(jīng)后人的努力，形成了機(jī)器定理證明的邏輯方法。8希爾伯特的構(gòu)想Hilbert在

《幾何基礎(chǔ)》中提出了從公理化走向機(jī)械

化的數(shù)學(xué)構(gòu)想。

Hilbert

計(jì)劃將數(shù)學(xué)知識納入嚴(yán)格的

公理體系中，并著力在公理化基礎(chǔ)上尋找機(jī)械化的

方法判定命題是否成立。

Hilbert

同時(shí)指出，定理的

判定問題應(yīng)當(dāng)是分類解決的，解決方法要同時(shí)強(qiáng)調(diào)

簡單性和嚴(yán)格性。在

Hilbert

的名著《幾何基礎(chǔ)》

一書中就提供了一

條可以對一類幾何命題進(jìn)行判定的定理一當(dāng)然，在那個(gè)時(shí)代，不僅

Hilbert

本人，整個(gè)數(shù)學(xué)界都沒

有意識到這一點(diǎn)。9哥德爾的著名結(jié)果G?del

著名的不完全性定理指出一個(gè)不弱于初等數(shù)論的形式系統(tǒng)如果是無矛盾的，則是

不完全的

，即存在形式系統(tǒng)的一個(gè)命題，它

和它的否定都不能由形式系統(tǒng)證明。因此，

Hilbert

的要求太高了。上述的Godel不完全性定理斷言：即使在初等數(shù)論的范圍

內(nèi)，對所有命題進(jìn)行判定的機(jī)械化方法也是

不存在的!10塔斯基的判定法波蘭數(shù)學(xué)家

Tarski

在

1950

年推廣了關(guān)于代

數(shù)方程實(shí)根數(shù)目的

Sturm

法則，由此證明了

一個(gè)引人注目的定理：

“一切初等幾何和初

等代數(shù)范圍的命題，都可以用機(jī)械方法判定。"Tarski

得出的結(jié)論給定理證明機(jī)械化的研究帶來了曙光。可惜他的方法太復(fù)雜，即使用

高速計(jì)算機(jī)也證明不了稍難的幾何定理。11王浩：邁向數(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)》

(IBMJournal),

王浩發(fā)表了《邁向數(shù)學(xué)機(jī)械化》(Toward

Mechanical

Mathemat

ics

),

“數(shù)學(xué)機(jī)械化”一詞即出自此處。12吳文?。簷C(jī)器證明領(lǐng)域的新的一頁1977

年，吳文俊在《中國科學(xué)》上發(fā)表論文《初等幾何判定問題與機(jī)械化問題》。

1984

年，吳文

俊的學(xué)術(shù)專著《幾何定理機(jī)器證明的基本原理》由

科學(xué)出版社出版，這部專著著重闡明幾何定理機(jī)械

化證明的基本原理。

1985

年，吳文俊的論文《關(guān)

于代數(shù)方程組的零點(diǎn)》發(fā)表，具體討論了多項(xiàng)式方

程組所確定的零點(diǎn)集。與國際上流行的代數(shù)理想論

不同，明確提出了具有中國自己特色的、以多項(xiàng)式

零點(diǎn)集為基本點(diǎn)的機(jī)械化方法。自此，

“吳方法”

宣告誕生，數(shù)學(xué)機(jī)械化研究揭開了新的一幕。13對吳方法的評價(jià)吳方法遵循中國傳統(tǒng)數(shù)學(xué)中幾何代數(shù)化的思想，與通?；?/p>

數(shù)理邏輯的方法根本不同，

首次實(shí)現(xiàn)了高效的幾何定理自動

證明，顯現(xiàn)了無比的優(yōu)越性。他的工作被稱為自動推理領(lǐng)域

的先驅(qū)性工作，并于1997年獲得

“Herbrand

自動推理杰出

成就獎(jiǎng)"。在授獎(jiǎng)辭中對他的工作給了這樣的介紹與評價(jià)："幾何定理自動證明首先由赫伯特"格蘭特(HerbertGerlenter)于50年代開始研究。雖然得到一些有意義的結(jié)果，

但在吳方法出現(xiàn)之前的20

年里，這一領(lǐng)域進(jìn)展甚微。在不多

的自動推理領(lǐng)域中，這種被動局面是由一個(gè)人完全扭轉(zhuǎn)的。

吳文俊很明顯是這樣一個(gè)人。他將幾何定理證明從一個(gè)不太

成功的領(lǐng)域變?yōu)樽畛晒Φ念I(lǐng)域之一。”14數(shù)學(xué)機(jī)械化得到國際數(shù)學(xué)界承認(rèn)2006年，著名數(shù)學(xué)家吳文俊榮獲邵逸

夫數(shù)學(xué)科學(xué)獎(jiǎng)。邵逸夫數(shù)學(xué)科學(xué)獎(jiǎng)是一項(xiàng)國際性大獎(jiǎng)，它的評委是來自國際數(shù)學(xué)界

的知名權(quán)威。吳文俊說：這次邵逸夫獎(jiǎng)的評委都是國際上有影響的大家，他們宣布我獲得邵逸夫獎(jiǎng)，是因?yàn)槲业臄?shù)學(xué)機(jī)械化

問題的研究，這實(shí)際上是國際數(shù)學(xué)界對數(shù)

學(xué)機(jī)械化研究的承認(rèn)與肯定，它比獎(jiǎng)金重要得多。15《吳文俊

·我的不等式》片斷16三角形三條高線交于一點(diǎn)的代數(shù)證明D是BC

和CA

上高線交點(diǎn)B(x?,0)A(x?,O)0(0,0)17定理的假設(shè)部分是AD

⊥BC

?x?x?-x?(x?-x?)=0BD

⊥AC

?x?x?-x?(x?-x?)=0由吳方法，可得非退化條件是

x?

(x?-x?)≠0定理的結(jié)論是CO

經(jīng)過D

點(diǎn)

?

x?=0顯然在非退化條件下定理成立。18任意三角形中，

一個(gè)角的三等分線，與和

它相鄰的角的三等分線相交，交點(diǎn)組成正

三角形。Morley定理19機(jī)器方法容易證明Morley定理任意三角形中，

一個(gè)角的三等分線，與和

它相鄰的角的三等分線相交，按一定的規(guī)

則選取交點(diǎn)，共可組成27個(gè)三角形，在這

27個(gè)三角形中，

一定有18個(gè)是正三角形。用機(jī)器方法容易證明這個(gè)更一般的Morley

定理。在證明過程中，多次出現(xiàn)關(guān)于12個(gè)

變量的含有一千多項(xiàng)的多項(xiàng)式。20定理的假設(shè)相當(dāng)于一組

多項(xiàng)式方程定理的結(jié)論相當(dāng)于一個(gè)

多項(xiàng)式方程上面的諸F

稱為假設(shè)多

項(xiàng)式，

G

稱為終結(jié)多項(xiàng)

式。F?=0,..,Fs=0G=0吳方法概要21吳方法概要(續(xù))吳方法是給出了一個(gè)機(jī)械化方法，在有限步內(nèi)給出一組非退化條件多項(xiàng)式D1,.,D,又根據(jù)這一機(jī)械化方法足以在有限步內(nèi)，判定在

非退化條件D?≠0,..,D,≠0下，

G=0是否可從F?=0,.,Fs=0

推出。22C(u?,u?)E(x?,x?)B(u1,0)平行四邊形對角線互相平分D(x?,2?)A(0,0)23題設(shè)和結(jié)論表成代數(shù)形式AD//BC:u?(u?-u?)-xu?=0E

在BD

上：

x?

(x?-u?)-u?

(x?-u?)=0E

在AC

上：x?U?-x?U?=0結(jié)論EA=EC:u2-2u?x?+u3-2u?x?=024吳方法的處理題設(shè)部分三角化，得到三個(gè)多項(xiàng)式：f?=u?-u?-xf?=x?(x?-u?-u?)+uu?f?=x?U?-x?U?再把結(jié)論左邊的多項(xiàng)式除以f3,所得的余式除以左，所得的余式除以f,

看最后所得的余式是不是恒等于

零。25中國古代數(shù)學(xué)的貢獻(xiàn)70年代初，吳文俊開始研讀中國數(shù)學(xué)史。1975年，他撰寫了《中國古代數(shù)學(xué)對世界文化的偉大

貢獻(xiàn)》,文中詳細(xì)列舉在代數(shù)、幾何、三角、解

析幾何和微積分等學(xué)科的發(fā)現(xiàn)和創(chuàng)立過程中，中

國傳統(tǒng)數(shù)學(xué)所起的重大作用。吳文俊指出，

中國傳統(tǒng)數(shù)學(xué)注意解方程，在代數(shù)學(xué)、幾何學(xué)、極限概念等方面既有豐碩的成果，

又有系統(tǒng)的理論。26中國古代數(shù)學(xué)的特色中國傳統(tǒng)數(shù)學(xué)強(qiáng)調(diào)構(gòu)造性和算法化，注意解決科學(xué)實(shí)驗(yàn)

和生產(chǎn)實(shí)踐中提出的各類問題，往往把所得到的結(jié)論以

各種原理的形式予以表述。在中國古代，求兩數(shù)最大公約數(shù)即等數(shù)用更相減損之術(shù)。

如求24與15的等數(shù)，其逐步減損如下：(24,15)→

(9,15)→

(9,6)→

(3,6)→

(3,3)其理由不證自明。中國傳統(tǒng)數(shù)學(xué)在從問題出發(fā)以解決問題為主旨的發(fā)展過

程中建立了以構(gòu)造性與機(jī)械化為其特色的算法體系，《九章算術(shù)》與劉徽的《九章算術(shù)注》是這一機(jī)械化體

系的代表作，這與西方數(shù)學(xué)以歐幾里得《幾何原本》為

代表的所謂公理化演繹體系正好遙遙相對。27機(jī)械化思想是中國古代數(shù)學(xué)的精髓吳文俊把中國傳統(tǒng)數(shù)學(xué)的思想概括為機(jī)械

化思想，指出它是貫穿于中國古代數(shù)學(xué)的

精髓。他列舉大量事實(shí)說明，中國傳統(tǒng)數(shù)

學(xué)的機(jī)械化思想為近代數(shù)學(xué)的建立和發(fā)展做出了不可磨滅的貢獻(xiàn)。這種機(jī)械化思想，不僅曾深刻影響了數(shù)學(xué)

的歷史進(jìn)程，而且對數(shù)學(xué)的現(xiàn)狀也正在發(fā)

揚(yáng)它日益顯著的影響。28數(shù)

學(xué)機(jī)械化的廣泛應(yīng)用吳文俊特別重視數(shù)學(xué)機(jī)械化方法的應(yīng)用，明確提出“數(shù)學(xué)機(jī)械化方法的成功應(yīng)用，是數(shù)學(xué)機(jī)械化

研究的生命線"

。他不斷開拓新的應(yīng)用領(lǐng)域，如

控制論、曲面拼接問題、機(jī)構(gòu)設(shè)計(jì)、化學(xué)平衡問

題、平面天體運(yùn)行的中心構(gòu)形等，還建立了解決全局優(yōu)化問題的新方法。吳方法還被用于若干高科技領(lǐng)域，得到一系列國際領(lǐng)先的成果，包括曲面造型、機(jī)器人結(jié)構(gòu)的位

置分析、智能計(jì)算機(jī)輔助設(shè)計(jì)(CAD)

、信息傳輸

中的圖像壓縮等。29從開普勒定律到牛頓定律開普勒定律為(1)行星繞太陽以橢圓軌道運(yùn)行，太陽為一焦點(diǎn)(2)太陽到行星的向量在相同的時(shí)間掃過相同的

面積牛頓定律為(3)行星的加速度與太陽到行星的距離的平方成

反比利用吳方法在微分域上的推廣，可以從開普勒經(jīng)驗(yàn)公式自動推導(dǎo)出牛頓定律。30機(jī)器人與連桿機(jī)構(gòu)的運(yùn)動分析如圖，綠色的平臺是活動平臺，下面的平臺是固定的，

六根連桿長度可變，求連桿長度變化時(shí)平臺上一點(diǎn)的 軌跡。31機(jī)器人與連桿機(jī)構(gòu)的運(yùn)動分析已知連桿機(jī)構(gòu)的構(gòu)成，求該機(jī)構(gòu)上某一點(diǎn)的軌跡

及該點(diǎn)的位置與連桿機(jī)構(gòu)的關(guān)系，這類問題稱為

機(jī)械設(shè)計(jì)中的正解問題。前面的例子就是一個(gè)正

解問題。反過來，求解連桿機(jī)構(gòu)的參數(shù)使得連桿機(jī)構(gòu)上一

點(diǎn)恰好位于空間指定位置的問題稱為機(jī)械設(shè)計(jì)中

的逆解問題。這兩類問題都可以看成方程求解問題。吳文俊用特征集方法解決了一般PUMA型機(jī)器人的逆解問題，研究了四連桿的設(shè)計(jì)問題。

32在幾何設(shè)計(jì)中，有一大類問題要確定一給定次數(shù)的代數(shù)曲面按一定要求連接已給的若干代數(shù)曲面。這類問題可以用吳方法解決。左圖是一個(gè)連接三根管道的例子。曲面連接問題33腦力勞動的機(jī)械化在新的正在到來的工業(yè)革命中，可以認(rèn)為是以某

種設(shè)備代替人腦。這將使人類艱苦思考的價(jià)值為

之降低，

是一種腦力勞動的機(jī)械化。這種機(jī)械化由于上世紀(jì)中葉計(jì)算機(jī)的發(fā)明而有某種可能。數(shù)學(xué)是一種典型的腦力勞動。由于數(shù)學(xué)思維具有

其它思維方式所沒有的簡潔、明確、嚴(yán)密、清晰

等優(yōu)點(diǎn)，因而數(shù)學(xué)的機(jī)