當我們望向未來的時候，不要忘了來路，100級台階上站着99個科學奠基人。

“談談你最仰慕的中國科學家”。關注公號粉絲走心評論互動轉發，挑選一位粉絲送出圖書《中國人工智能簡史第一部》1本。

撰文｜林軍  岑峰

工作中的吳文俊（1919年5月12日－2017年5月7日）

圖源：中國科學院數學與系統科學研究院

1979年在中國是一個重要的年份。這一年發生了諸多大事，也被視爲中國在政治、經濟、科技、 文化等多個領域的一個重要轉折點和中國近現代歷史重要的時期斷代點之一。相比1979年所开啓的波瀾壯闊的新時代，中國人工智能(Artificial Intelligence，AI)研究在1979年的起步只能算歷史大潮中的一朵不起眼的浪花，但在中國人工智能的歷史裏，這是开天闢地的大事件。

人工智能最早的學派是符號主義學派，最早一批人工智能科學家多半是數學家和邏輯學家，他們在計算機誕生後把計算機與自己的研究結合起來，從而進入人工智能領域。在中國，同樣是由數學家翻开了人工智能研究的第一頁。在1979年，無論是機器證明中的“吳方法”走向世界，還是堪比達特茅斯會議的計算機科學暑期討論會的舉辦，其背後都有着數學家的身影。也正是從這一年起，中國人工智能邁开了追趕世界的腳步。

“吳方法”的提出者，正是數學家吳文俊。他與王湘浩、曾憲昌並稱“機器證明三傑”。1970年代後期，近花甲之年的吳文俊從研究中國古代數學出發，开創了嶄新的數學機械化領域，提出了用計算機證明幾何定理的“吳方法”，被認爲是自動推理領域的先驅性工作。

01

吳文俊推开了中國人工智能

走向世界的大門

1979年1月，應普林斯頓高等研究院的邀請，數學家吳文俊懷揣2.5萬美元，登上了赴美交流的班機。

與他同行的是數學家陳景潤。二人是中美正式建交後第一批應邀赴美學習訪問的科學家，將在普林斯頓高等研究院學習和交流一段時間。陳景潤交流的主題自然是 “1+2”，而吳文俊此行交流的主要內容，除了他的老本行拓撲學，更多的是中國古代數學史和數學機械化，他想用自己攜帶的2.5萬美元購买一台計算機，用於數學機械化的研究。

吳文俊在1979年獲得中國科學院(下稱“中科院”)自然科學一等獎時，數學機械化已經成爲他的主要研究方向。這個研究方向也受到世人矚目，吳文俊的研究方法在機器定理證明界被稱爲“吳方法”，中國智能科學技術最高獎“吳文俊人工智能科學技術獎”就使用了吳文俊的名字，以紀念吳文俊作爲中國研究者在人工智能相關領域取得的成就。

不經意間，吳文俊推开了中國人工智能研究走向世界的大門。吳文俊對中國古代數學史的研究始於1974年前後。當時中國科學院數學研究所(下稱“中科院數學研究所”)副所長關肇直讓吳文俊研究中國古代數學。吳文俊很快發現了中國古代數學傳統與由古希臘延續下來的近現代西方數學傳統的重要區別，對中國古代算術進行了正本清源的分析，在許多方面產生了獨到的見解。

20世紀70年代，對外學術交流开始逐步恢復。1975年，吳文俊赴法交流，並在法國高等科學研究所作了關於中國古代數學思想的報告。這時吳文俊已經復原了日高公式的古代證明，並注意到了中國古代數學的“構造性”和“機械化”的特點。1977年春節，吳文俊用手算驗證了幾何定理機器證明方法的可行性，這一過程歷時兩個月。

機器定理證明最初的思想源自戈特弗裏德·威廉·萊布尼茨(Gottfried Wilhelm Leibniz)的演算推論器，以及之後演化而來的符號邏輯。後來，戴維·希爾伯特 (David Hilbert)在此基礎上於1920年推出了“希爾伯特計劃”，希望將整個數學體系嚴格公理化。簡單來講，如果這一計劃實現，就意味着對於任何一個數學猜想，不管它有多難，我們總能夠知道這個猜想是否正確，並且證明或否定它。希爾伯特說的“Wir mussen wissen,wir werden wissen”(我們必須知道，我們必將知道)便是這個意思。

然而，就在此後不久的1931年，庫爾特·哥德爾(Kurt Godel)就提出了哥德爾不完備定理，徹底粉碎了希爾伯特的形式主義理想。但不管怎么說，哥德爾在關上這扇門的時候還是留了一扇窗。法國天才數學家雅克·埃爾布朗(Jacques Herbrand) 的博士論文爲數理邏輯的證明論和遞歸論奠定了基礎，埃爾布朗在哥德爾不完備定理被提出後，檢查了自己的論文，留下一句話——哥德爾和我的結果並不矛盾，並向哥德爾寫了一封信請教。哥德爾回復了埃爾布朗，但埃爾布朗沒能等到這封信，他在哥德爾回信兩天後死於登山事故，年僅23歲。後來，定理證明領域的最高獎項也以埃爾布朗的名字命名，吳文俊在1997年獲得了第四屆埃爾布朗自動推理傑出成就獎。

其他數學家對哥德爾定理也進行了補充。就在哥德爾證明“一階整數(算術)是不可判定的”之後不久，阿爾弗萊德·塔爾斯基(Alfred Tarski)證明了“一階實數(幾何與代數)是可以判定的”，這也爲機器證明奠定了基礎。

1936年，圖靈在他的重要論文《論可計算數及其在判定問題上的應用》(On Computable Numbers, with an Application to the Entscheidungsproblem)中對哥德爾在1931年證明和計算限制的結果重新進行了論述，並用現在叫作圖靈機的簡單形式的抽象裝置代替了哥德爾的以通用算術爲基礎的形式語言，證明了一切可計算過程都可以用圖靈機模擬。這也是計算機科學和人工智能的重要理論基礎。人工智能最早的學派——符號學派也正是在形式邏輯運算的基礎上延伸而來的。

回過頭來說吳文俊，他在20世紀70年代到生產計算機的北京無线電一廠工作， 並在那個時候开始接觸計算機和機器定理證明。“如何發揮計算機的威力，將其應用到自己的數學研究上”成爲吳文俊感興趣的內容。後來，吳文俊开始研究中國古代數學史，並總結出中國古代數學的幾何代數化傾向和算法化思想。在發現中國古代數學與西方數學的不同思路後，他決定換一種方法來做幾何定理的機器證明。

那個時候，吳文俊閱讀了很多國外的文章，充分了解了機器證明。當時，機器定理證明最前沿的研究來自數理邏輯學家王浩，他在西南聯大數學系讀書期間曾師從著名哲學家、“中國哲學界第一人”金岳霖，後前往美國哈佛大學，在著名哲學家、邏輯學家威拉德·馮·奎因(W. V. Quine)門下學習奎因創立的形式公理系統並獲得博士學位。早在1953年，王浩就已經开始思考用機器證明數學定理的可能性了。

1958年，王浩在一台IBM 7041計算機上使用命題邏輯程序證明了《數學原理》中所有的一階邏輯定理，次年又完成了全部200條命題邏輯定理的證明。王浩之工作的意義在於宣告了用計算機進行定理證明的可能性。他在1977年回國時參加了多個影響我國科技長遠發展的討論會，並在中科院作了 6 次專題演講，對國內機器證明研究有着重大的影響。

言歸正傳，王浩此前對《數學原理》中命題邏輯定理的證明和吳文俊想要實現的幾何定理機器證明之間還存在着鴻溝，前者符號邏輯的成分更多，後者則有推理的成分在內。當時，國外有很多對幾何定理機器證明的研究，但都以失敗告終。

02

從中國古代數學思想的機械化到“吳方法”

在吳文俊看來，失敗的經驗也是很重要的，它會告訴你哪些路是走不通的。他受笛卡兒思想的啓發，通過引入坐標，把幾何問題轉化爲代數問題，再按中國古代數學思想把它機械化了。吳文俊甚至把笛卡兒思想與中國古代數學思想結合起來，提出一個解決一般問題的路线：

所有的問題都可以轉變成數學問題，所有的數學問題都可以轉變成代數問題，所有的代數問題都可以轉變成解方程組的問題，所有解方程組的問題都可以轉變成解單變元的代數方程問題。

中國古代數學與西方的現代數學是兩套不同的體系。吳文俊在不借助現代數學中的三角函數、微積分、因式分解法、高次方程解法等“現代工具”的情況下，按古人當時的知識和慣用的思維推理復原了《周髀算經》《數書九章》中的“日高圖說”“大衍求一術”“增乘开方術”的證明方法。他認爲中國古代數學有着自己的獨到之處，秦九韶的方法具有構造性和可機械化的特點，用小計算器即可求出高次代數方程的數值解。在當時缺乏高性能計算設備的情況下，吳文俊能充分利用中國古代數學思想降維進行研究，也是難能可貴的事情。

吳文俊按照這一思路證明的第一個定理是費爾巴哈定理，即證明了“三角形的九點圓與其內切圓以及三個旁切圓相切”。這是平面幾何學中十分優美的定理之一，吳文俊的審美可見一斑。當時沒有計算機，吳文俊就自己用手算。“吳方法”的一個特點是會產生大量的多項式，證明過程中涉及的最大多項式有數百項，這一計算非常困難，任何一步出錯都會導致後面的計算失敗。1977年春節，吳文俊首次用手算成功驗證了幾何定理機器證明的方法，後來，吳文俊又在一台由北京無线電一廠生產的長城203上證明了西姆森定理。

吳文俊將相關的研究文章《初等幾何判定問題與機械化證明》發表在1977年的《中國科學》上，並將文章寄給了王浩。王浩高度評價了吳文俊的工作，並復信建議吳文俊利用已有的代數包，考慮用計算機實現吳方法。王浩沒有意識到這個時候中美兩國最頂尖的學者所使用的計算機的差別：長城 203可以使用機器語言，但不同計算機的指令系統並不通用，利用已有的代數包行不通。所以，後來吳文俊幹脆從中科院數學研究所裏借了一台來中科院數學研究所訪問的外國人贈送的小計算器，把所給命題轉化爲代數形式，再用秦九韶的方法來計算高階方程的解。 

吳文俊幾何定理機器證明的研究得到了關肇直的大力支持。關肇直曾在法國留學，是中國科學工作者協會旅法分會的創辦人之一，團結了一批優秀的愛國知識分子，吳文俊就是其中之一。當時，吳文俊所在的中科院數學研究所關系復雜，有一派認爲做機器證明是“離經叛道”，希望他繼續從事拓撲學研究；從拓撲學和泛函分析轉入控制理論的關肇直卻格外支持和理解他，放話說吳文俊想幹什么就讓他幹什么。後來，關肇直在1979年“另立山頭”，成立中科院系統科學研究所時，吳文俊也跟隨關肇直到了中科院系統科學研究所(圖1-1)。 

圖 1-1 20世紀80年代初中科院系統科學研究所原辦公樓(現融科大廈) (左起：許國志、吳文俊、印度學者、關肇直)

要證明更復雜的定理，需要有更好的機器。時任中科院聲學研究所所長的汪德昭院士指點了吳文俊。他告訴吳文俊中科院黨組書記、副院長李昌何時何地會出現，結果真被吳文俊守到了。李昌非常开明，在20世紀50年代擔任哈爾濱工業大學(下稱“哈工大”)校長期間把哈工大辦成了全國一流大學。在1954年確定的全國六所重點大學中，哈工大是唯一一所不在北京的大學。李昌對吳文俊的工作同樣給予了很大支持，吳文俊去美國买計算機的2.5萬美元外匯就是由李昌特批的。有了這台計算機，很多定理很快被證明出來了。

20世紀70年代也是機器定理證明的黃金時代。1976年，兩位美國數學家用高速電子計算機耗費1200小時的計算時間證明了四色定理，數學家們100多年來未能解決的難題得到解決。四色定理之所以能被證明，是因爲不可約集和不可避免集是有限的，四色定理的“地圖塗色”問題看似有無窮多的地圖，實際上可以把它們歸結爲 2000多種基本形狀，之後利用計算機的計算能力暴力窮舉，一個個去證明即可。打個比方，這種方法如同復原魔方——將魔方拆散並重新拼好——雖不優雅但確實有效。我們現在說GPT-3“大力出奇跡”，其實四色定理的證明才是“大力出奇跡”的始祖。

然而，這種利用計算機計算能力暴力破解定理證明的做法並不能得到推廣。定理證明的第一步，即定理的形式化，需要完整和嚴謹的表述。關於這一點，有一個關於數學家的小故事。一個天文學家、一個物理學家和一個數學家乘坐火車到蘇格蘭旅行，他們看到窗外有一只黑色的羊，天文學家开始感慨：“怎么蘇格蘭的羊都是黑色的？”物理學家糾正：“應該說蘇格蘭的一些羊是黑色的。”而最嚴謹的表達則來自數學家：“在蘇格蘭至少存在着一塊天地，至少有一只羊，這只羊至少有一側是黑色的。”還有一個段子，說數學問題分兩類：一類是“這也要證？”，一類是“這也能證？”。由此可知，一個證明要得到其他數學家的認可是多么不容易。同樣，要在一個交互式定理證明器裏形式化一個定理，需要填補所有的技術細節，才能完成推理的“自動化”，最終用一種可行但是計算量很大的解題思路來代替對定理的證明。換言之，這種方式仍然依賴數學家對定理的理解，只能做到“一理一證”，只能算定理的計算機輔助證明。

所以，在四色定理被計算機證明後，包括王浩在內的一批邏輯學家提出了不同意見：四色定理算被證明了嗎？這種證明方式算傳統證明，計算機只是起到了輔助計算的作用。一直到 2005 年，喬治·貢蒂爾(Georges Gonthier) 才完成了四色定理的全部計算機化證明，其每一步邏輯推導都是由計算機完成的。目前人們已經用計算機證明了數百條數學定理，但這些定理大多是已知的，“機器智能”還未對數學有真正意義上的貢獻。

機器定理證明依賴於算法。在早期階段，研究者們往往試圖找到一個超級算法去解決所有問題，而吳文俊則將中國古代數學思想應用於幾何定理的機器證明領域，做到了“一類一證”。這一點也得到了王浩的贊同，他認爲自己的早期工作和吳文俊使用的方法具有共同點，即先找到一個相對可控的子領域，然後根據這個子領域的特點找出最有效的算法。吳文俊在1979年訪美的時候還特地去洛克菲勒大學拜訪了王浩，他的工作在機器定理界受到重視也和王浩的力薦有着一定的關系。 

“吳方法”真正傳播开來，讓機器定理證明在20世紀80年代第一次取得突破性進展，還有賴於曾經聽過吳文俊機器定理證明課程的一位在美留學生——周鹹青。周鹹青本想考吳文俊機器證明方向的研究生，不過他認爲微分幾何是自己的弱項，害怕考不上，最終考到中國科學技術大學(下稱“中科大”)，後來到中科院計算技術研究所代培，就此旁聽了吳文俊的幾何證明的課程。

1981年，周鹹青到得克薩斯大學奧斯汀分校留學，當時得克薩斯大學奧斯汀分校堪稱定理證明界的王者，該校的兩個研究小組都曾獲得定理證明的最高獎赫布蘭德獎。周鹹青向羅伯特·博耶(Robert Boyer)提及了吳文俊的工作，博耶覺得很新鮮，便繼續追問，但周鹹青只知道是將幾何轉化爲代數，具體細節則講不出所以然。 

之後，伍迪·布萊索(Woody Bledsoe)便讓周鹹青和另一位學生王鐵城去搜集資料，周鹹青的博士論文便是吳方法的實現。吳文俊很快寄來了兩篇文章，文章上都有他給布萊索的籤名。在此後兩年，這兩篇文章被得克薩斯大學奧斯汀分校復印了近百次寄往世界各地，吳方法开始廣爲人知。

1983年，全美定理機器證明學術會議在美國科羅拉多州舉行，周鹹青在會議上作了題爲“用吳方法證明幾何定理”的報告。周鹹青开發的通用程序能自動證明130 多條幾何定理，其中包含莫勒定理、西姆森定理、費爾巴哈九點圓定理和笛沙格定理等難度較大的定理的證明。之後，這次會議的論文集作爲美國《當代數學》系列叢書第 29 卷於1984 年正式發表，吳文俊寄來的兩篇相關論文也被收錄其中。

1986年6月，圖靈獎獲得者約翰·霍普克羅夫特(John Hopcroft)等人組織了一場幾何自動推理的研討會，討論會的部分報告被收錄在1988年12月的《人工智能》 特輯中，特輯的引言文章特別介紹了吳文俊提出的代數幾何新方法，認爲該方法不僅爲幾何推理的進步做出了巨大貢獻，在人工智能的三大應用問題（機器人和運動規劃、機器視覺、實體建模）中也都具有重要的應用價值(圖1-2)。霍普克羅夫特此後與中國多所高校密切合作，在上海交通大學、北京大學、香港中文大學(深圳)均有由他牽頭的研究機構，吳文俊和吳方法大概就是他有中國情結的开始。

圖 1-2 1988 年《人工智能》特輯开篇對吳方法的概述 

03

《中國人工智能簡史：從1979到1993》

本系列圖書全面講述中國人工智能40多年的發展史，幾乎覆蓋了中國人工智能學科的所有領域，包括中國人工智能研究的起源、各個分支在中國的發展情況、當下與產業相結合的現狀以及未來的研究方向等。以宏觀的視野和生動的語言，對中國人工智能領域進行了全面回顧和深度剖析。 

作者團隊深入採訪了全國十余所主要高校、中科院多個研究所老中青三代人工智能研究者，重點介紹中國人工智能領域傑出的科學家，以及他們創造非凡成果的有趣故事。 

本書爲該系列第一卷，梳理了自1979年至1993年中國人工智能領域初期十多年的發展歷程，用輕松而真誠的筆觸，講述了爲中國人工智能發展尋路的奠基者，並介紹了重要歷史事件的來龍去脈，帶領讀者深入了解中國人工智能發展早期鮮爲人知的歷史。

本文作者可以追加內容哦 !