來源：圖靈社區
作者：林軍岑峰
工作中的吳文俊（1919年5月12日－2017年5月7日）。圖源：中國科學院數學與系統科學研究院
1979 年在中國是一個重要的年份。這一年發生了諸多大事，也被視為中國在政治、經濟、科技、 文化等多個領域的一個重要轉折點和中國近現代歷史重要的時期斷代點之一。相比1979 年所開啟的波瀾壯闊的新時代，中國人工智能(Artificial Intelligence，AI)研究在1979 年的起步只能算歷史大潮中的一朵不起眼的浪花，但在中國人工智能的歷史裡，這是開天闢地的大事件。
人工智能最早的學派是符號主義學派，最早一批人工智能科學家多半是數學家和邏輯學家，他們在計算機誕生後把計算機與自己的研究結合起來，從而進入人工智能領域。在中國，同樣是由數學家翻開了人工智能研究的第一頁。在1979 年，無論是機器證明中的“吳方法”走向世界，還是堪比達特茅斯會議的計算機科學暑期討論會的舉辦，其背後都有著數學家的身影。也正是從這一年起，中國人工智能邁開了追趕世界的腳步。
“吳方法”的提出者，正是數學家吳文俊。他與王湘浩、曾憲昌並稱“機器證明三傑”。 1970年代後期，近花甲之年的吳文俊從研究中國古代數學出發，開創了嶄新的數學機械化領域，提出了用計算機證明幾何定理的“吳方法”，被認為是自動推理領域的先驅性工作。
一、吳文俊推開了中國人工智能走向世界的大門
1979 年1 月，應普林斯頓高等研究院的邀請，數學家吳文俊怀揣2.5 萬美元，登上了赴美交易所的班機。
與他同行的是數學家陳景潤。二人是中美正式建交後第一批應邀赴美學習訪問的科學家，將在普林斯頓高等研究院學習和交易所一段時間。陳景潤交易所的主題自然是“1+2”，而吳文俊此行交易所的主要內容，除了他的老本行拓撲學，更多的是中國古代數學史和數學機械化，他想用自己攜帶的2.5 萬美元購買一台計算機，用於數學機械化的研究。
吳文俊在1979 年獲得中國科學院(下稱“中科院”)自然科學一等獎時，數學機械化已經成為他的主要研究方向。這個研究方向也受到世人矚目，吳文俊的研究方法在機器定理證明界被稱為“吳方法”，中國智能科學技術最高獎“吳文俊人工智能科學技術獎”就使用了吳文俊的名字，以紀念吳文俊作為中國研究者在人工智能相關領域取得的成就。
不經意間，吳文俊推開了中國人工智能研究走向世界的大門。吳文俊對中國古代數學史的研究始於1974 年前後。當時中國科學院數學研究所(下稱“中科院數學研究所”)副所長關肇直讓吳文俊研究中國古代數學。吳文俊很快發現了中國古代數學傳統與由古希臘延續下來的近現代西方數學傳統的重要區別，對中國古代算術進行了正本清源的分析，在許多方面產生了獨到的見解。
20 世紀70 年代，對外學術交易所開始逐步恢復。 1975 年，吳文俊赴法交易所，並在法國高等科學研究所作了關於中國古代數學思想的報告。這時吳文俊已經復原了日高公式的古代證明，並註意到了中國古代數學的“構造性”和“機械化”的特點。 1977 年春節，吳文俊用手算驗證了幾何定理機器證明方法的可行性，這一過程歷時兩個月。
機器定理證明最初的思想源自戈特弗里德·威廉·萊布尼茨(Gottfried Wilhelm Leibniz)的演算推論器，以及之後演化而來的符號邏輯。後來，戴維·希爾伯特(David Hilbert)在此基礎上於1920 年推出了“希爾伯特計劃”，希望將整個數學體系嚴格公理化。簡單來講，如果這一計劃實現，就意味著對於任何一個數學猜想，不管它有多難，我們總能夠知道這個猜想是否正確，並且證明或否定它。希爾伯特說的“Wir müssen wissen,wir werden wissen”(我們必須知道，我們必將知道)便是這個意思。
然而，就在此後不久的1931 年，庫爾特·哥德爾(Kurt Gödel)就提出了哥德爾不完備定理，徹底粉碎了希爾伯特的形式主義理想。但不管怎麼說，哥德爾在關上這扇門的時候還是留了一扇窗。法國天才數學家雅克·埃爾布朗(Jacques Herbrand) 的博士論文為數理邏輯的證明論和遞歸論奠定了基礎，埃爾布朗在哥德爾不完備定理被提出後，檢查了自己的論文，留下一句話——哥德爾和我的結果並不矛盾，並向哥德爾寫了一封信請教。哥德爾回復了埃爾布朗，但埃爾布朗沒能等到這封信，他在哥德爾回信兩天后死於登山事故，年僅23 歲。後來，定理證明領域的最高獎項也以埃爾布朗的名字命名，吳文俊在1997 年獲得了第四屆埃爾布朗自動推理傑出成就獎。
其他數學家對哥德爾定理也進行了補充。就在哥德爾證明“一階整數(算術)是不可判定的”之後不久，阿爾弗萊德·塔爾斯基(Alfred Tarski)證明了“一階實數(幾何與代數)是可以判定的”，這也為機器證明奠定了基礎。
1936 年，圖靈在他的重要論文《論可計算數及其在判定問題上的應用》(On Computable Numbers, with an Application to the Entscheidungsproblem)中對哥德爾在1931 年證明和計算限制的結果重新進行了論述，並用現在叫作圖靈機的簡單形式的抽象裝置代替了哥德爾的以通用算術為基礎的形式語言，證明了一切可計算過程都可以用圖靈機模擬。這也是計算機科學和人工智能的重要理論基礎。人工智能最早的學派——符號學派也正是在形式邏輯運算的基礎上延伸而來的。
回過頭來說吳文俊，他在20 世紀70 年代到生產計算機的北京無線電一廠工作， 並在那個時候開始接觸計算機和機器定理證明。 “如何發揮計算機的威力，將其應用到自己的數學研究上”成為吳文俊感興趣的內容。後來，吳文俊開始研究中國古代數學史，並總結出中國古代數學的幾何代數化傾向和算法化思想。在發現中國古代數學與西方數學的不同思路後，他決定換一種方法來做幾何定理的機器證明。
那個時候，吳文俊閱讀了很多國外的文章，充分了解了機器證明。當時，機器定理證明最前沿的研究來自數理邏輯學家王浩，他在西南聯大數學系讀書期間曾師從著名哲學家、“中國哲學界第一人”金岳霖，後前往美國哈佛大學，在著名哲學家、邏輯學家威拉德·馮·奎因(WV Quine)門下學習奎因創立的形式公理系統並獲得博士學位。早在1953 年，王浩就已經開始思考用機器證明數學定理的可能性了。
1958 年，王浩在一台IBM 7041 計算機上使用命題邏輯程序證明了《數學原理》中所有的一階邏輯定理，次年又完成了全部200 條命題邏輯定理的證明。王浩之工作的意義在於宣告了用計算機進行定理證明的可能性。他在1977 年回國時參加了多個影響我國科技長遠發展的討論會，並在中科院作了6 次專題演講，對國內機器證明研究有著重大的影響。
言歸正傳，王浩此前對《數學原理》中命題邏輯定理的證明和吳文俊想要實現的幾何定理機器證明之間還存在著鴻溝，前者符號邏輯的成分更多，後者則有推理的成分在內。當時，國外有很多對幾何定理機器證明的研究，但都以失敗告終。
二、從中國古代數學思想的機械化到“吳方法”
在吳文俊看來，失敗的經驗也是很重要的，它會告訴你哪些路是走不通的。他受笛卡兒思想的啟發，通過引入坐標，把幾何問題轉化為代數問題，再按中國古代數學思想把它機械化了。吳文俊甚至把笛卡兒思想與中國古代數學思想結合起來，提出一個解決一般問題的路線：
所有的問題都可以轉變成數學問題，所有的數學問題都可以轉變成代數問題，所有的代數問題都可以轉變成解方程組的問題，所有解方程組的問題都可以轉變成解單變元的代數方程問題。
中國古代數學與西方的現代數學是兩套不同的體系。吳文俊在不借助現代數學中的三角函數、微積分、因式分解法、高次方程解法等“現代工具”的情況下，按古人當時的知識和慣用的思維推理復原了《周髀算經》 《數書九章》中的“日高圖說”“大衍求一術”“增乘開方術”的證明方法。他認為中國古代數學有著自己的獨到之處，秦九韶的方法具有構造性和可機械化的特點，用小計算器即可求出高次代數方程的數值解。在當時缺乏高性能計算設備的情況下，吳文俊能充分利用中國古代數學思想降維進行研究，也是難能可貴的事情。
吳文俊按照這一思路證明的第一個定理是費爾巴哈定理，即證明了“三角形的九點圓與其內切圓以及三個旁切圓相切”。這是平面幾何學中十分優美的定理之一，吳文俊的審美可見一斑。當時沒有計算機，吳文俊就自己用手算。 “吳方法”的一個特點是會產生大量的多項式，證明過程中涉及的最大多項式有數百項，這一計算非常困難，任何一步出錯都會導致後面的計算失敗。 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 年《人工智能》特輯開篇對吳方法的概述
資訊來源：由0x資訊編譯自8BTC。版權歸作者所有，未經許可，不得轉載