工作中的吳文俊（1919年5月12日－2017年5月7日）。圖源：中國科學院數學與系統科學研究院
撰文：《中國人工智能簡史：從1979到1993》作者林軍、岑峰
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年代到生産計算機的北京無線電一廠工作， 并在那個時候開始接觸計算機和機器定理證明。“如何發揮計算機的威力，将其應用到自己的數學研究上”成為吳文俊感興趣的内容。後來，吳文俊開始研究中國古代數學史，并總結出中國古代數學的幾何代數化傾向和算法化思想。在發現中國古代數學與西方數學的不同思路後，他決定換一種方法來做幾何定理的機器證明。
那個時候，吳文俊閱讀了很多國外的文章，充分了解了機器證明。當時，機器定理證明最前沿的研究來自數理邏輯學家王浩，他在西南聯大數學系讀書期間曾師從著名哲學家、“中國哲學界第一人”金嶽霖，後前往美國哈佛大學，在著名哲學家、邏輯學家威拉德·馮·奎因(W. V. Quine)門下學習奎因創立的形式公理系統并獲得博士學位。早在1953年，王浩就已經開始思考用機器證明數學定理的可能性了。
1958年，王浩在一台IBM 7041計算機上使用命題邏輯程式證明了《數學原理》中所有的一階邏輯定理，次年又完成了全部200條命題邏輯定理的證明。王浩之工作的意義在于宣告了用計算機進行定理證明的可能性。他在1977年回國時參加了多個影響大陸科技長遠發展的讨論會，并在中科院作了6次專題演講，對國内機器證明研究有着重大的影響。
言歸正傳，王浩此前對《數學原理》中命題邏輯定理的證明和吳文俊想要實作的幾何定理機器證明之間還存在着鴻溝，前者符号邏輯的成分更多，後者則有推理的成分在内。當時，國外有很多對幾何定理機器證明的研究，但都以失敗告終。
從中國古代數學思想的機械化到“吳方法”
在吳文俊看來，失敗的經驗也是很重要的，它會告訴你哪些路是走不通的。他受笛卡兒思想的啟發，通過引入坐标，把幾何問題轉化為代數問題，再按中國古代數學思想把它機械化了。吳文俊甚至把笛卡兒思想與中國古代數學思想結合起來，提出一個解決一般問題的路線：
所有的問題都可以轉變成數學問題，所有的數學問題都可以轉變成代數問題，所有的代數問題都可以轉變成解方程組的問題，所有解方程組的問題都可以轉變成解單變元的代數方程問題。
中國古代數學與西方的現代數學是兩套不同的體系。吳文俊在不借助現代數學中的三角函數、微積分、因式分解法、高次方程解法等“現代工具”的情況下，按古人當時的知識和慣用的思維推理複原了《周髀算經》《數書九章》中的“日高圖說”“大衍求一術”“增乘開方術”的證明方法。他認為中國古代數學有着自己的獨到之處，秦九韶的方法具有構造性和可機械化的特點，用小電腦即可求出高次代數方程的數值解。在當時缺乏高性能計算裝置的情況下，吳文俊能充分利用中國古代數學思想降維進行研究，也是難能可貴的事情。
吳文俊按照這一思路證明的第一個定理是費爾巴哈定理，即證明了“三角形的九點圓與其内切圓以及三個旁切圓相切”。這是平面幾何學中十分優美的定理之一，吳文俊的審美可見一斑。當時沒有計算機，吳文俊就自己用手算。“吳方法”的一個特點是會産生大量的多項式，證明過程中涉及的最大多項式有數百項，這一計算非常困難，任何一步出錯都會導緻後面的計算失敗。1977年春節，吳文俊首次用手算成功驗證了幾何定理機器證明的方法，後來，吳文俊又在一台由北京無線電一廠生産的長城203上證明了西姆森定理。
吳文俊将相關的研究文章《初等幾何判定問題與機械化證明》發表在1977年的《中國科學》上，并将文章寄給了王浩。王浩高度評價了吳文俊的工作，并複信建議吳文俊利用已有的代數包，考慮用計算機實作吳方法。王浩沒有意識到這個時候中美兩國最頂尖的學者所使用的計算機的差别：長城203可以使用機器語言，但不同計算機的指令系統并不通用，利用已有的代數包行不通。是以，後來吳文俊幹脆從中科院數學研究所裡借了一台來中科院數學研究所通路的外國人贈送的小電腦，把所給命題轉化為代數形式，再用秦九韶的方法來計算高階方程的解。
吳文俊幾何定理機器證明的研究得到了關肇直的大力支援。關肇直曾在法國留學，是中國科學工作者協會旅法分會的創辦人之一，團結了一批優秀的愛國知識分子，吳文俊就是其中之一。當時，吳文俊所在的中科院數學研究所關系複雜，有一派認為做機器證明是“離經叛道”，希望他繼續從事拓撲學研究；從拓撲學和泛函分析轉入控制理論的關肇直卻格外支援和了解他，放話說吳文俊想幹什麼就讓他幹什麼。後來，關肇直在1979年“另立山頭”，成立中科院系統科學研究所時，吳文俊也跟随關肇直到了中科院系統科學研究所。
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月的《人工智能》 特輯中，特輯的引言文章特别介紹了吳文俊提出的代數幾何新方法，認為該方法不僅為幾何推理的進步做出了巨大貢獻，在人工智能的三大應用問題（機器人和運動規劃、機器視覺、實體模組化）中也都具有重要的應用價值。霍普克羅夫特此後與中國多所高校密切合作，在上海交通大學、北京大學、香港中文大學(深圳)均有由他牽頭的研究機構，吳文俊和吳方法大概就是他有中國情結的開始。
1988 年《人工智能》特輯開篇對吳方法的概述
本文節選自人民郵件出版社2023年8月出版的《中國人工智能簡史：從1979到1993》（作者：林軍 / 岑峰）。刊發已獲人民郵件出版社授權。
本系列圖書全面講述中國人工智能40多年的發展史，幾乎覆寫了中國人工智能學科的所有領域，包括中國人工智能研究的起源、各個分支在中國的發展情況、當下與産業相結合的現狀以及未來的研究方向等。以宏觀的視野和生動的語言，對中國人工智能領域進行了全面回顧和深度剖析。
作者團隊深入采訪了全國十餘所主要高校、中科院多個研究所老中青三代人工智能研究者，重點介紹中國人工智能領域傑出的科學家，以及他們創造非凡成果的有趣故事。
《中國人工智能簡史：從1979到1993》為該系列第一卷，梳理了自1979年至1993年中國人工智能領域初期十多年的發展曆程，用輕松而真誠的筆觸，講述了為中國人工智能發展尋路的奠基者，并介紹了重要曆史事件的來龍去脈，帶領讀者深入了解中國人工智能發展早期鮮為人知的曆史。