吳文俊與幾何定理機(jī)械化證明

【內(nèi)容摘要】吳文俊是我國當(dāng)代享譽(yù)世界的杰出數(shù)學(xué)家，人教版《普通高中課程標(biāo)準(zhǔn)實(shí)驗教科書數(shù)學(xué)（必修2）》第四章圓與方程中的閱讀材料“坐標(biāo)法與機(jī)器證明”一文中，簡單地介紹吳文俊和他的幾何定理機(jī)器證明的思想。本人在教學(xué)中發(fā)現(xiàn)，許多中學(xué)生并不知道這位數(shù)學(xué)家，更不用說幾何定理的機(jī)械化證明。本文旨在向廣大中學(xué)生宣傳吳文俊的學(xué)術(shù)成就和治學(xué)精神，說明幾何定理機(jī)械化證明的思想和方法，激發(fā)中學(xué)生科學(xué)探究的興趣和愛國主義情感，實(shí)現(xiàn)數(shù)學(xué)教材中閱讀材料的價值。

【關(guān)鍵詞】吳文俊 幾何定理 機(jī)械化證明

吳文俊教授，我國當(dāng)代享譽(yù)世界的著名數(shù)學(xué)家。1919年5月12日生于上海，1940年畢業(yè)于上海交通大學(xué)，1949年獲法國國家博士學(xué)位。中國科學(xué)院數(shù)學(xué)與系統(tǒng)科學(xué)研究院系統(tǒng)科學(xué)研究所研究員、名譽(yù)所長，中國數(shù)學(xué)會名譽(yù)理事長。中國數(shù)學(xué)機(jī)械化研究的創(chuàng)始人之一，現(xiàn)任中國科學(xué)院系統(tǒng)科學(xué)研究所名譽(yù)所長、研究員，中國科學(xué)院院士，第三世界科學(xué)院院士。曾任中國數(shù)學(xué)會理事長（1985-1987），中國科學(xué)院數(shù)理學(xué)部主任（1992-1994）。

曾獲得首屆國家自然科學(xué)一等獎（1956）、中國科學(xué)院自然科學(xué)一等獎（1979）、第三世界科學(xué)院數(shù)學(xué)獎（1990）、陳嘉庚數(shù)理科學(xué)獎（1993）、首屆香港求是科技基金會杰出科學(xué)家獎（1994）、Herbrand自動推理杰出成就獎（1997）、首屆國家最高科學(xué)技術(shù)獎（2000）、第三屆邵逸夫數(shù)學(xué)獎（2006）。

2010年5月4日，國際小行星中心先后發(fā)布公報通知國際社會，將國際永久編號第7683號小行星永久命名為“吳文俊星”。

1976年粉碎“四人幫”之后，中國迎來了科學(xué)的春天。年近花甲的吳文俊在中國古算研究的基礎(chǔ)上，分析了西方R.笛卡兒的思想，深入探討D.希爾伯特《幾何基礎(chǔ)》一書中隱藏的構(gòu)造性思想，開拓機(jī)械化數(shù)學(xué)的嶄新領(lǐng)域。數(shù)學(xué)機(jī)械化方法的思想是：從幾何公理體系出發(fā)，首先取適當(dāng)?shù)淖鴺?biāo)，于是幾何定理的假設(shè)與終結(jié)通常都成為多項式方程，稱之為假設(shè)方程與終結(jié)方程，滿足定理假設(shè)的幾何圖像就相當(dāng)于假設(shè)方程組的一個解答或零點(diǎn)。要證明定理成立，就是要證明假設(shè)方程的零點(diǎn)也是終結(jié)方程的零點(diǎn)。

1976年冬吳文俊開始研究，1977年春取得初步結(jié)果。證明初等幾何主要一類定理的證明可以機(jī)械化，問題分成三個步驟：

“第一步，從幾何的公理系統(tǒng)出發(fā)，引進(jìn)數(shù)系統(tǒng)及坐標(biāo)系統(tǒng)，使任意幾何定理的證明問題成為純代數(shù)問題。

第二步，將幾何定理假設(shè)部分的代數(shù)關(guān)系式進(jìn)行整理，然后依確定步驟驗證定理終結(jié)部分的代數(shù)關(guān)系式是否可以從假設(shè)部分已整理成序的代數(shù)關(guān)系式中推出。

第三步，依據(jù)第二步中的確定步驟編成程序，并在計算機(jī)上實(shí)施，以得出定理是否成立的最后結(jié)論。”

1977年吳文俊在一臺檔次很低的計算機(jī)（長城203型臺式計算機(jī)）上首先按上述步驟實(shí)現(xiàn)像西姆森線那樣不很簡單的定理的證明，然后又完成了西姆森線、費(fèi)爾巴哈定理、毛萊定理等一系列初等幾何的證明。并把機(jī)器定理證明的范圍推廣到非歐幾何、仿射幾何、圓幾何、線幾何、球幾何等等領(lǐng)域，先后與其同伴們陸續(xù)證明100多條定理。周咸青應(yīng)用吳氏算法證明600多條定理。1978年初吳文俊又證明初等微分幾何中的一些主要定理也可以機(jī)械化。

吳文俊的成就在于：

（1）提出一套完整的算法，使得代數(shù)方程組通過機(jī)械步驟消元變成一個代數(shù)方程。

（2）解代數(shù)方程組可擴(kuò)大為帶微分的代數(shù)方程組，從而大大擴(kuò)張研究問題的范圍。

（3）不僅能證明定理，而且能自動發(fā)現(xiàn)定理，這大大優(yōu)越于現(xiàn)有的任何方法。

（4）與許多以前的原則可行的方法相比較，吳文俊的方法完全是現(xiàn)實(shí)可行的。

（5）算法穩(wěn)定，能一舉同時得出多解，這是其他算法根本無法比擬的。

吳文俊幾何定理機(jī)械化證明的方法，被世界數(shù)學(xué)界譽(yù)為“吳方法”，給兩千多年的公理化演繹體系帶來了強(qiáng)烈沖擊。吳文俊的數(shù)學(xué)機(jī)械化思想不是一時心血來潮，而是長期思考導(dǎo)致的戰(zhàn)略轉(zhuǎn)變。他認(rèn)清計算機(jī)出現(xiàn)對人類工作和生活的巨大促進(jìn)，更認(rèn)識到計算機(jī)對于未來腦力勞動機(jī)械化的潛在影響。要知道，當(dāng)時還沒有微機(jī)，微軟也剛剛建立，沒人想到十年之后、二十年之后的變化。吳文俊想的更遠(yuǎn)，他不僅看到體力勞動的機(jī)械化，更高瞻遠(yuǎn)矚地看到腦力勞動的機(jī)械化。而數(shù)學(xué)正是最純粹的腦力勞動。腦力勞動的機(jī)械化當(dāng)然從數(shù)學(xué)做起，數(shù)學(xué)的兩大任務(wù)是證明定理及計算，數(shù)值計算不成問題。問題是如何把證明化為符號計算并且由計算機(jī)實(shí)現(xiàn)，這就是數(shù)學(xué)機(jī)械化中心思想。

到80年代，吳文俊不僅建立數(shù)學(xué)機(jī)械化證明的基礎(chǔ)，而且擴(kuò)張成廣泛的數(shù)學(xué)機(jī)械化綱領(lǐng)，解決一系列理論及實(shí)際問題。這僅僅是吳文俊數(shù)學(xué)成就的一小部分。此外他在拓?fù)鋵W(xué)、自動推理、代數(shù)幾何、中國數(shù)學(xué)史、對策論等研究領(lǐng)域均有杰出的貢獻(xiàn)，在國內(nèi)外享有崇高盛譽(yù)。

吳文俊取得這些成就完全是靠他一生積極進(jìn)取、鍥而不舍的治學(xué)精神。他讀龐特里亞金的俄文原文完全是靠字典一個字一個字查出來的，使用計算機(jī)完全靠自己長時間一點(diǎn)一點(diǎn)摸索出來，其刻苦精神由此可見一斑。他熱愛數(shù)學(xué)、獨(dú)立思考、富于創(chuàng)見，無論外界環(huán)境順利還是困難，都能始終如一地努力從事研究工作。吳文俊一生淡泊自守，對于名利看得很輕，從來不宣揚(yáng)自己，以至于他在國內(nèi)的知名度與他的成就顯得極不相稱。他不僅從未沾染學(xué)術(shù)界的一些不良作風(fēng)，恰恰相反，他平易近人，樂于助人，樂于宣傳其他人的成績，學(xué)術(shù)作風(fēng)民主。永遠(yuǎn)是青少年學(xué)習(xí)的榜樣，數(shù)學(xué)工作者的楷模，中國數(shù)學(xué)界的一面旗幟。

【參考文獻(xiàn)】

[1] 胡作玄.《吳文俊》.

[2] 人教版《普通高中課程標(biāo)準(zhǔn)實(shí)驗教科書數(shù)學(xué)（必修2）》.

（作者單位：安徽省天長中學(xué)）