我國近現代數學的一項突出成就——數學機械化

中國近現代數學在世界處于什么地位呢？一些人嘆息中國數學落后于國外，甚至夸大其詞。事實上，我國近現代數學工作者在一些方面已經作出了突出成就，吳文俊院士和他的數學機械化研究就是其中的杰出代表. 2000年，吳文俊院士獲得首屆國家最高科學技術獎. 2006年，他獲得了被媒體譽為“21世紀東方諾貝爾獎”的香港邵逸夫數學科學獎. 兩次獲獎理由都是因為他對數學機械化這一新興交叉學科作出開創性的貢獻.

1 什么是數學機械化

“所謂數學機械化，其思想實質在于以構造性與算法化的方式從事數學研究，是數學的推理過程機械化以至自動化，以盡量減少聰明才智的要求，并由此減輕艱難的重腦力勞動. ”^[1]數學機械化主要有兩個特點：算法化，它遵循了一定的操作規則和程序；刻板化，所有的程序步驟都是據一定的法則按部就班地進行，不存在跳躍性.

數學機械化的思想在中小學數學學習中就已有體現. 比如，加減乘除四則運算、開方運算、冪的運算、絕對值運算、方程和方程組求解、不等式和不等式組求解等等，這些都是按部就班地依照一定的法則機械化進行的，蘊涵一定的數學機械化思想方法.

誠如吳文俊所言，“數學機械化”這一名詞最早取自美國洛克菲勒大學數理邏輯家王浩先生的著作《向機械化數學前進》(Woward Mechanical Mathematics).

2 國外數學家的早期工作

早在17世紀時，法國數學家笛卡兒(Descartes)和德國數學家萊布尼茲(Leibnize)就已經產生了數學機械化思想萌芽. 笛卡兒的解析幾何學即是努力建立幾何的代數化，把幾何問題的求解通過引入坐標轉化成代數方程的求解，從而開辟了幾何定理證明機械化的道路. 萊布尼茲設計了最原始的乘法計算器，并設想研制出推理機器，自動檢驗數學命題的正確性. 19世紀末，德國數學家希爾伯特(Hilbert)等人創立并發展了數理邏輯，至此，數學證明機械化思想初步形成. 對于希爾伯特的著作《幾何基礎》，吳文俊認為^[1]，“該書更重要處，是在于提供了一條從公理化出發，通過代數化以到達機械化的道路. ”而此時，數學機械化思想還僅是一種預示性的理論，還無法具體操作和實施. 20世紀40年代電子計算機問世，數學機械化思想有了現實的可能性. 1950年，波蘭數學家塔斯基(Tarski)從理論上證明了初等幾何以及初等代數范圍內的定理證明是可以證明的. 1959年，王浩設計了幾個計算機程序，僅用3分鐘就在IBM704型計算機上證明了數學家羅素(Russell)與懷特海(Whitehead)的數學著作《數學原理》中220條有關命題邏輯的定理，后來又擴展到400條. 這就宣告了數學定理證明的計算機操作的可行性. 王浩在《數理邏輯總覽》中多次提出要使數學成為機械化的數學.

3 吳文俊的研究工作

吳文俊早期從事拓撲學的研究工作，他所提出的“吳示性類”與“吳示嵌類”以及“吳公式”成為拓撲學中的經典成果，廣受國際數學同行們的贊譽.

1974年，因為當時社會現實的因素，他轉向中國古代數學史的研究. 在此之前他并不了解中國古代傳統數學成就，他說^[2]，“中國的數學家，除了專門從事中國古代數學史的專家以外，絕大多數的中國數學家，包括陳省身和我，由于所受教育以及西方史書的影響，對中國的古代數學都是比較輕視，認為不足道的. ”

隨著研究的深入，吳文俊逐漸認識到中國古代數學的特點是算法化和構造性. 例如，《周髀》中的日高公式主要是基于算法的考慮；漢初完成的《九章算術》在開平方、開立方運算過程中使用構造方法；宋元時代，探討高次線性方程組的求解，等等. 可以說，中國古代數學正是沿著這樣的數學機械化范式進行研究的，這不同于西方以希臘數學為傳統的邏輯演繹體系. 雖然在西方數學研究歷程中也曾有過諸多算法，但卻不如中國如此突出和鮮明. 他用“機械化”一詞高度概括了中國古代數學家解決數學問題的思路和方法.

專研中國古代數學史的同時，吳文俊也在計算機工廠勞動. 正是在這種情況下，他認識到計算機的原理與中國古代數學機械化思想是相通的，兩者可以有效地結合起來，并促進彼此的深入發展.

1977年，吳文俊發表了《初等幾何判定問題與機械化證明》. 與此同時，他提出了數學機械化綱領：在數學的各個學科選擇適當的范圍實現機械化，推動數學發展與腦力勞動機械化；應用數學機械化方法解決相關高科技領域的關鍵基礎理論問題. 1985年，他發表了《關于代數方程組的零點》，討論多項式方程組所確定的零點集. 至此，他正式確立了多項式方程組求解的吳文俊消元法，國際上簡稱為“吳方法”. “吳方法”的確立與廣泛應用，復興了國際數學機械化的研究.

吳文俊指出^[1]，“我們從事機械化定理證明工作獲得成果之前，對Tarski的已有工作并無接觸，更沒有想到Hilbert的《幾何基礎》會與機械化有任何關系. 我們是在中國古代數學的啟發之下提出問題并想出解決辦法來的. ”

4 吳方法的運用

1997年，吳文俊獲得“厄布朗(Herbrand)自動推理杰出成就獎”，在授獎詞中對他的工作給了這樣的介紹和評價^[3]：“幾何定理自動證明首先由赫博特格蘭特(Herbert Gerlenter)于50年代開始研究. 雖然得到一些有意義的結果，但在吳方法出現之前的20年里，這一領域進展甚微. 在不多的自動推理領域中，這種被動局面是由一個人完全扭轉的. 吳文俊很明顯是這樣一個人. ”數學機械化思想的核心就是方程求解的“吳特征列方法”，這一方法實現了幾何自動推理研究的突破，而推理的自動化正是計算機產生智能行為的一個關鍵. 以下簡單地舉幾個吳方法運用的事例.

4.1 證明已有的科學定理和規律

物理學史上，牛頓通過觀測和試驗，推廣了開普勒定律，推導出萬有引力定律. 上世紀八十年代末，當美國學者正為如何借助計算機和數學工具從開普勒定律推導出牛頓定律而一籌莫展時，吳文俊使用吳方法巧妙地解決了這個重要的問題. 從開普勒定律的微分代數方程描述出發，經過整序運算，計算機可以自動產生新的微分代數表達式，再加上一些技術性的處理，就可以得到牛頓定律的微分代數表達式.

吳方法的一個特點是在證明時不考慮定理中幾何元素的順序. 所以用吳方法證明的幾何定理實際上與定理的幾何圖形無關. 例如蝴蝶定理的證明：設A、B、C、D為圓上四點. E=AC∩BD，過點E與EO垂直的直線分別交AD、BC與M、N. 證明E是MN的中點. 這是高中數學中一個經典問題，一般來說，用正弦定理證明相對簡便. 但是事先需要確定圖形的形狀，比如這個定理可以是下圖三種情形中的任意一種. 而用吳方法證明此定理就不需要考慮命題中的幾何圖形. 定理一旦被證明是正確的，它的推論也自然成立，也就是對于所有的圖形都正確.

吳文俊明確指出^[1]，“目前我們所能證明的定理局限于已經發明的機械化方法的范圍，例如初等幾何與初等微分幾何之內. 而如何超出與擴大這些機械化的范圍，則是今后需要探索的長期的理論性工作. ”根據歌德爾的不完全定理，即使在初等數論的范圍內，對所有數學命題進行證明的機械化方法也是不存在的.

4.2 發現新的數學關系和規律

吳方法不僅可以自動證明幾何定理，還可以用來自動發現未知的幾何關系. 幾何中常見的關于面積、體積的公式可以用這個方法自動推導出來. 比如反映三角形面積與三條邊間關系的海倫 (Heron)—秦九韶公式k=[KF(]s(s-a)(s-b)(s-c)[KF)]，就可以根據吳方法由計算機自動推理得出.

一個金字塔形狀的幾何體，用一個平面去截它，截面能否是一個正五邊形？用吳方法解答這個問題時會得到一個令人意外的現象：上述平面和金字塔形狀幾何體的棱的延長線相交，有五個交點恰好是另一個正五邊形的頂點，就是說還有一個正五邊形存在，并且前一個正五邊形在某種意義上處于黃金分割的位置，而后一個五邊形處在于前一個在某種意義上相對偶的地方. 當然，這個發現在目前并沒有任何實用意義，但是它為純數學提供了一個和諧美妙的關系.

吳文俊強調^[1]，“我們應該著重指出，我們并不鼓勵以后人們將使用計算機來證明甚至發現一些有趣的幾何定理. 恰恰相反，我們希望人們不再從事這種雖然有趣卻即是對數學甚至幾何學本身也已意義不大的工作，而把自己從這種工作中解放出來，把自己的聰明才智與創造能力貫注到更有意義的腦力勞動上去. ”

4.3 代數方程求解

數學機械化理論研究的核心內容是方程求解. 方程求解不僅是重要的數學問題，而且在許多的領域存在著應用. 事實上，很多科學和工程中的問題都可以轉化為方程求解的問題. 無論是證明已有的定理和規律，還是發現新的數學關系和規律，實質上都是試圖把所研究的問題轉化成代數問題，列出方程組，進而求其零點解集. “求解代數方程組是數學上極為困難的問題，在理論上屬于代數幾何學. 但是，西方數學難以建立有效算法來真正去解這個方程組. 而吳文俊方法恰好能有效地做到這一點. ”^[4]

5 我國其他數學家的工作

在吳文俊數學機械化思想方法的啟發下，我國許多數學家在數學機械化領域也作出了許多卓越成就. 1992年，張景中院士根據面積法所創立的消點算法，成功地研制出幾何定理自動生成可讀的數學證明軟件. 2000年，他進一步發展，研制出與傳統幾何證明方法一致的第三代智能數學平臺軟件，又稱為“Z+Z”智能教育平臺. 這開創了世界智能性數學教學軟件的先河. 張景中院士和楊路、高小山、周咸青合作，把消點法用于非歐幾何可讀證明的自動生成也得到成功，并得到一批非歐幾何新定理.

1999年，數學家楊路創立了降維算法，并研制出實現這種算法的數學軟件. 通過這種軟件，在計算機上證明了二千多個不等式. 不等式的機械化證明，這是幾何定理機械化證明領域的又一個重大突破.

王梓坤院士指出，^[5]“我們可以自豪地說：幾何定理機械證明研究的重大成果大都是由我國數學家所取得的. ”

6 我國數學機械化研究方向與進展

“數學機械化是適應信息時代產生的基礎研究領域，具有中國特色且在國際上領先. ”^[6]中科院數學與系統科學研究院承擔一項國家重點基礎研究發展計劃項目——數學機械化方法及其在信息技術中的應用. 參與項目研究的有中科院、北京大學、清華大學、南開大學、中國科技大學等. 主要有七個研究方向：數學機械化理論與核心算法，差分與微分方程的機械化算法，實幾何與實代數的高效能算法，數學機械化與信息安全與編碼理論，數學機械化在生物特征識別中的應用，數學機械化在幾何建模中的應用，基于網絡的數學機械化軟件開發.

目前取得的一些研究成果無論是理論基礎還是實際應用都是十分豐碩的，下面主要是從應用價值的角度簡單地列舉幾項成就. 在信息安全方面，進行了密碼分析與密碼技術、協議的設計與分析，設計了能應用于電子現金系統的盲簽名方案；設計了能用于移動通信的代理簽名方案；設計了廣播加密協議. 在生物特征識別中的應用，對指紋圖象增強、奇異點檢測和指紋搜索等方面進行了研究；研究掌紋識別的基本方法，并建立了一個具有一定規模的掌紋庫. 基于網絡的數學機械化軟件開發方面，設計了包括《油田開發規劃優化系統》和《油藏數值模擬中病態方程組求解》等大型復雜應用軟件；根據哈爾濱電機廠提供的若干技術指標要求(例如，作業空間，加工效率，加工精度等)，設計了一臺大型串聯五軸數控機床.

參考文獻

[1] 吳文俊.數學機械化[M].北京：科學出版社，2003.

[2] 梁芳.幾何定理機器證明的方法——吳方法思想的形成[J].數學通報，2003，(6):4-6.

[3] 高小山，石赫.卓越的貢獻 高度的評價——吳文俊及其科學成就[J].中國科學院院刊，2001，(1):64-66.

[4] 胡作玄.吳文俊——從拓撲學到數學機械化[J].自然辯證法通訊，2003，(1):81-90.

[5] 孫熙椿.數學機械化與我國數學家所取得的巨大成就[J].中學數學研究，2004，(2):43-46.

[6] 高小山.數學機械化研究展望[J].中國基礎科學，1999，(1):26-28.

“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”