1979年在中國是一個重要的年份。這一年發生了諸多大事，也被視為中國在政治、經濟、科技、文化等多個領域的一個重要轉折點和中國近現代曆史重要的時期斷代點之一。相比1979年所開啟的波瀾壯闊的新時代，中國人工智能（Artifcial Intelligence，AI）研究在1979年的起步隻能算曆史大潮中的一朵不起眼的浪花，但在中國人工智能的曆史裡，這是開天辟地的大事件。
紀錄片《地平線系列：尋找人工智能》（2012）劇照。
人工智能最早的學派是符号主義學派，最早一批人工智能科學家多半是數學家和邏輯學家，他們在計算機誕生後把計算機與自己的研究結合起來，進而進入人工智能領域。在中國，同樣是由數學家翻開了人工智能研究的第一頁。在1979年，無論是機器證明中的“吳方法”走向世界，還是堪比達特茅斯會議的計算機科學暑期讨論會的舉辦，其背後都有着數學家的身影。也正是從這一年起，中國人工智能邁開了追趕世界的腳步。
《中國人工智能簡史：從1979到1993》，林軍岑峰著，人民郵電出版社2023年8月版。
吳文俊推開了中國人工智能研究走向世界的大門
1979年1月，應普林斯頓高等研究院的邀請，數學家吳文俊懷揣2.5萬美元，登上了赴美交流的班機。
與他同行的是數學家陳景潤。二人是中美正式建交後第一批應邀赴美學習通路的科學家，将在普林斯頓高等研究院學習和交流一段時間。陳景潤交流的主題自然是“1+2”，而吳文俊此行交流的主要内容，除了他的老本行拓撲學，更多的是中國古代數學史和數學機械化，他想用自己攜帶的2.5萬美元購買一台計算機，用于數學機械化的研究。
吳文俊在1979年獲得中國科學院（下稱“中科院”）自然科學一等獎時，數學機械化已經成為他的主要研究方向。這個研究方向也受到世人矚目，吳文俊的研究方法在機器定理證明界被稱為“吳方法”，中國智能科學技術最高獎“吳文俊人工智能科學技術獎”就使用了吳文俊的名字，以紀念吳文俊作為中國研究者在人工智能相關領域取得的成就。
不經意間，吳文俊推開了中國人工智能研究走向世界的大門。吳文俊對中國古代數學史的研究始于1974年前後。當時中國科學院數學研究所（下稱“中科院數學研究所”）副所長關肇直讓吳文俊研究中國古代數學。吳文俊很快發現了中國古代數學傳統與由古希臘延續下來的近現代西方數學傳統的重要差別，對中國古代算術進行了正本清源的分析，在許多方面産生了獨到的見解。
20世紀70年代，對外學術交流開始逐漸恢複。1975年，吳文俊赴法交流，并在法國高等科學研究所作了關于中國古代數學思想的報告。這時吳文俊已經複原了日高公式的古代證明，并注意到了中國古代數學的“構造性”和“機械化”的特點。1977年春節，吳文俊用手算驗證了幾何定理機器證明方法的可行性，這一過程曆時兩個月。
機器定理證明最初的思想源自戈特弗裡德·威廉·萊布尼茨（Gottfried Wilhelm Leibniz）的演算推論器，以及之後演化而來的符号邏輯。後來，戴維·希爾伯特（David Hilbert）在此基礎上于1920年推出了“希爾伯特計劃”，希望将整個數學體系嚴格公理化。簡單來講，如果這一計劃實作，就意味着對于任何一個數學猜想，不管它有多難，我們總能夠知道這個猜想是否正确，并且證明或否定它。希爾伯特說的“Wirmüssen wissen,wir warden 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年，王浩在一台IBM7041計算機上使用命題邏輯程式證明了《數學原理》中所有的一階邏輯定理，次年又完成了全部200條命題邏輯定理的證明。王浩之工作的意義在于宣告了用計算機進行定理證明的可能性。他在1977年回國時參加了多個影響大陸科技長遠發展的讨論會，并在中科院作了6次專題演講，對國内機器證明研究有着重大的影響。言歸正傳，王浩此前對《數學原理》中命題邏輯定理的證明和吳文俊想要實作的幾何定理機器證明之間還存在着鴻溝，前者符号邏輯的成分更多，後者則有推理的成分在内。當時，國外有很多對幾何定理機器證明的研究，但都以失敗告終。
從中國古代數學思想的機械化到“吳方法”
在吳文俊看來，失敗的經驗也是很重要的，它會告訴你哪些路是走不通的。他受笛卡兒思想的啟發，通過引入坐标，把幾何問題轉化為代數問題，再按中國古代數學思想把它機械化了。吳文俊甚至把笛卡兒思想與中國古代數學思想結合起來，提出一個解決一般問題的路線：
所有的問題都可以轉變成數學問題，所有的數學問題都可以轉變成代數問題，所有的代數問題都可以轉變成解方程組的問題，所有解方程組的問題都可以轉變成解單變元的代數方程問題。
中國古代數學與西方的現代數學是兩套不同的體系。吳文俊在不借助現代數學中的三角函數、微積分、因式分解法、高次方程解法等“現代工具”的情況下，按古人當時的知識和慣用的思維推理複原了《周髀算經》《數書九章》中的“日高圖說”“大衍求一術”“增乘開方術”的證明方法。他認為中國古代數學有着自己的獨到之處，秦九韶的方法具有構造性和可機械化的特點，用小電腦即可求出高次代數方程的數值解。在當時缺乏高性能計算裝置的情況下，吳文俊能充分利用中國古代數學思想降維進行研究，也是難能可貴的事情。
吳文俊按照這一思路證明的第一個定理是費爾巴哈定理，即證明了“三角形的九點圓與其内切圓以及三個旁切圓相切”。這是平面幾何學中十分優美的定理之一，吳文俊的審美可見一斑。當時沒有計算機，吳文俊就自己用手算。“吳方法”的一個特點是會産生大量的多項式，證明過程中涉及的最大多項式有數百項，這一計算非常困難，任何一步出錯都會導緻後面的計算失敗。1977年春節，吳文俊首次用手算成功驗證了幾何定理機器證明的方法，後來，吳文俊又在一台由北京無線電一廠生産的長城2031上證明了西姆森定理。
吳文俊将相關的研究文章《初等幾何判定問題與機械化證明》發表在1977年的《中國科學》上，并将文章寄給了王浩。王浩高度評價了吳文俊的工作，并複信建議吳文俊利用已有的代數包，考慮用計算機實作吳方法。王浩沒有意識到這個時候中美兩國最頂尖的學者所使用的計算機的差别：長城203可以使用機器語言，但不同計算機的指令系統并不通用，利用已有的代數包行不通。是以，後來吳文俊幹脆從中科院數學研究所裡借了一台來中科院數學研究所通路的外國人贈送的小電腦，把所給命題轉化為代數形式，再用秦九韶的方法來計算高階方程的解。
吳文俊幾何定理機器證明的研究得到了關肇直的大力支援。關肇直曾在法國留學，是中國科學工作者協會旅法分會的創辦人之一，團結了一批優秀的愛國知識分子，吳文俊就是其中之一。當時，吳文俊所在的中科院數學研究所關系複雜，有一派認為做機器證明是“離經叛道”，希望他繼續從事拓撲學研究；從拓撲學和泛函分析轉入控制理論的關肇直卻格外支援和了解他，放話說吳文俊想幹什麼就讓他幹什麼。後來，關肇直在1979年“另立山頭”，成立中科院系統科學研究所時，吳文俊也跟随關肇直到了中科院系統科學研究所。
20世紀80年代國中科院系統科學研究所原辦公樓（現融科大廈）（左起：許國志、吳文俊、印度學者、關肇直，《中國人工
智能簡史：從1979到1993》内文插圖）。
要證明更複雜的定理，需要有更好的機器。時任中科院聲學研究所所長的汪德昭院士指點了吳文俊。他告訴吳文俊中科院黨組書記、副院長李昌何時何地會出現，結果真被吳文俊守到了。李昌非常開明，在20世紀50年代擔任哈爾濱工業大學（下稱“哈工大”）校長期間把哈工大辦成了全國一流大學。在1954年确定的全國六所重點大學中，哈工大是唯一一所不在北京的大學。李昌對吳文俊的工作同樣給予了很大支援，吳文俊去美國買計算機的2.5萬美元外彙就是由李昌特批的。有了這台計算機，很多定理很快被證明出來了。
20世紀70年代也是機器定理證明的黃金時代。1976年，兩位美國數學家用高速電子計算機耗費1200小時的計算時間證明了四色定理，數學家們100多年來未能解決的難題得到解決。四色定理之是以能被證明，是因為不可約集和不可避免集是有限的，四色定理的“地圖塗色”問題看似有無窮多的地圖，實際上可以把它們歸結為2000多種基本形狀，之後利用計算機的計算能力暴力窮舉，一個個去證明即可。打個比方，這種方法如同複原魔方——将魔方拆散并重新拼好——雖不優雅但确實有效。我們現在說GPT-31“大力出奇迹”，其實四色定理的證明才是“大力出奇迹”的始祖。
然而，這種利用計算機計算能力暴力破解定理證明的做法并不能得到推廣。定理證明的第一步，即定理的形式化，需要完整和嚴謹的表述。關于這一點，有一個關于數學家的小故事。一個天文學家、一個實體學家和一個數學家乘坐火車到蘇格蘭旅行，他們看到窗外有一隻黑色的羊，天文學家開始感慨：“怎麼蘇格蘭的羊都是黑色的？”實體學家糾正：“應該說蘇格蘭的一些羊是黑色的。”而最嚴謹的表達則來自數學家：“在蘇格蘭至少存在着一塊天地，至少有一隻羊，這隻羊至少有一側是黑色的。”還有一個段子，說數學問題分兩類：一類是“這也要證？”，一類是“這也能證？”。
由此可知，一個證明要得到其他數學家的認可是多麼不容易。同樣，要在一個互動式定理證明器裡形式化一個定理，需要填補所有的技術細節，才能完成推理的“自動化”，最終用一種可行但是計算量很大的解題思路來代替對定理的證明。
換言之，這種方式仍然依賴數學家對定理的了解，隻能做到“一理一證”，隻能算定理的計算機輔助證明。是以，在四色定理被計算機證明後，包括王浩在内的一批邏輯學家提出了不同意見：四色定理算被證明了嗎？這種證明方式算傳統證明，計算機隻是起到了輔助計算的作用。一直到2005年，喬治·貢蒂爾（Georges Gonthier）才完成了四色定理的全部計算機化證明，其每一步邏輯推導都是由計算機完成的。
目前人們已經用計算機證明了數百條數學定理，但這些定理大多是已知的，“機器智能”還未對數學有真正意義上的貢獻。機器定理證明依賴于算法。在早期階段，研究者們往往試圖找到一個超級算法去解決所有問題，而吳文俊則将中國古代數學思想應用于幾何定理的機器證明領域，做到了“一類一證”。這一點也得到了王浩的贊同，他認為自己的早期工作和吳文俊使用的方法具有共同點，即先找到一個相對可控的子領域，然後根據這個子領域的特點找出最有效的算法。吳文俊在1979年訪美的時候還特地去洛克菲勒大學拜訪了王浩，他的工作在機器定理界受到重視也和王浩的力薦有着一定的關系。
“吳方法”真正傳播開來，讓機器定理證明在20世紀80年代第一次取得突破性進展，還有賴于曾經聽過吳文俊機器定理證明課程的一位在美留學生——周鹹青。周鹹青本想考吳文俊機器證明方向的研究所學生，不過他認為微分幾何是自己的弱項，害怕考不上，最終考到中國科學技術大學（下稱“中科大”），後來到中科院計算技術研究所代培，就此旁聽了吳文俊的幾何證明的課程。
1981年，周鹹青到得克薩斯大學奧斯汀分校留學，當時得克薩斯大學奧斯汀分校堪稱定理證明界的王者，該校的兩個研究小組都曾獲得定理證明的最高獎赫布蘭德獎。周鹹青向羅伯特·博耶（Robert Boyer）提及了吳文俊的工作，博耶覺得很新鮮，便繼續追問，但周鹹青隻知道是将幾何轉化為代數，具體細節則講不出是以然。
之後，伍迪·布萊索（Woody Bledsoe）便讓周鹹青和另一位學生王鐵城去搜集資料，周鹹青的博士論文便是吳方法的實作。吳文俊很快寄來了兩篇文章，文章上都有他給布萊索的簽名。在此後兩年，這兩篇文章被得克薩斯大學奧斯汀分校影印了近百次寄往世界各地，吳方法開始廣為人知。
1983年，全美定理機器證明學術會議在美國科羅拉多州舉行，周鹹青在會議上作了題為“用吳方法證明幾何定理”的報告。周鹹青開發的通用程式能自動證明130多條幾何定理，其中包含莫勒定理、西姆森定理、費爾巴哈九點圓定理和笛沙格定理等難度較大的定理的證明。之後，這次會議的論文集作為美國《當代數學》系列叢書第29卷于1984年正式發表，吳文俊寄來的兩篇相關論文也被收錄其中。
1986年6月，圖靈獎獲得者約翰·霍普克羅夫特（John Hopcroft）等人組織了一場幾何自動推理的研讨會，讨論會的部分報告被收錄在1988年12月的《人工智能》特輯中，特輯的引言文章特别介紹了吳文俊提出的代數幾何新方法，認為該方法不僅為幾何推理的進步做出了巨大貢獻，在人工智能的三大應用問題（機器人和運動規劃、機器視覺、實體模組化）中也都具有重要的應用價值。霍普克羅夫特此後與中國多所高校密切合作，在上海交通大學、北京大學、香港中文大學（深圳）均有由他牽頭的研究機構，吳文俊和“吳方法”大概就是他有中國情結的開始。
1988年《人工智能》特輯開篇對吳方法的概述（《中國人工智能簡史：從1979到1993》内文插圖）。
對人工智能的保留：數學機械化學派
盡管這些學術活動把吳文俊的名字與人工智能的概念自然而緊密地聯系在了一起，但吳文俊自己依然對“人工智能”的提法有所保留。按他的說法就是：“人工智能的程式是我親手一條一條編寫的，每一條指令都是必須機械執行的動作，它根本沒有智能，所謂‘人工智能’就是機械化執行人的思維過程，并不是計算機有了智能。”是以，吳文俊用王浩提出的“數學機械化”來描述自己的工作。在1977年發表于《中國科學》的論文《初等幾何判定問題與機械化證明》中，吳文俊特地寫了一個附注，闡明機械化思想的起源：
我們關于初等幾何定理機械化證明所用的算法，主要牽涉到一些多項式的運用技術，例如算術運算與簡單消元法之類。應該指出，這些都是12至14世紀宋元時期中國數學家的創造，在那時已有相當高度的發展。……事實上，幾何問題機械化與用代數方法系統求解，乃是當時中國數學家的主要成就之一，其時間遠在17世紀出現解析幾何之前。
人工智能是一門交叉學科，數學自然也是與人工智能相關的基礎學科之一。但從上述表述看，吳文俊機器證明的目的還是更好地去證明和輔助發現數學新定理，這和人工智能的研究是兩個圈子。在當時人工智能被批判和質疑的背景下，吳文俊對人工智能的保留實際上是他的一種自保政策，烏鎮智庫的尼克就曾說吳文俊先生是數學家中的“人精”。
在1979年吉林大學舉辦的“計算機科學暑期讨論會”上，雖然分組讨論的是人工智能的内容，但對外還是叫“智能模拟”。讷于言而敏于行，這或許也是吳文俊未受重大沖擊的原因。“吳方法”開啟了自動推理與方程求解的數學機械化中國學派。從1983年起，吳文俊開始陸續招收研究所學生從事機器證明的研習。較早的幾位學生包括胡森（1983—1986，獲碩士學位）、王東明（1983—1987，獲博士學位）、高小山（1984—1988，獲博士學位）、劉卓軍（1986—1988，獲博士學位）、李子明（1985—1988，獲碩士學位）等。這批學生後來成為國内數學機械化研究的中堅力量。
受吳方法影響的，還有兩位北大數力系才子洪加威和張景中。當時，吳文俊最早的兩位研究所學生胡森和王東明發現，許多圖形若畫出來是對的，就可能是定理。這一點不久被洪加威變成定理，洪加威使用的方法是用一個例子去證明一個幾何定理，也稱單點例證法。張景中是群英荟萃的北大數力系1954級的學生，比洪加威高一級（其實北大數力系1955級也人才濟濟）。張洪兩人交情頗深，張景中在1957年被調往新疆，後來北大的老師尋找張景中時，還是從洪加威那裡知道的消息。
另一個與張景中交情頗深的數學家是楊路。在二十世紀六七十年代，張景中就和楊路一起讨論幾何算法和函數疊代，楊路提出通過點與點的距離關系，不建立坐标系而直接研究幾何圖形的性質。這與吳文俊将中國古代數學思路與笛卡兒思想相結合有一定的相通之處。1979年，張景中調往中科大工作，1985年又調往中科院成都數理科學研究室，楊路也幾乎同時完成自己的工作調動，兩個人正是張不離楊，楊不離張。也就是在20世紀70年代末，張景中和楊路開始進入機器定理證明領域。
1984年洪加威構思例證法的時候，張景中就和他建議，用一組例子比一個例子更容易實作。1989年，張景中和楊路發展了洪加威的方法，提出了數值并行法，舉例的思路有所不同。張景中的工作得到吳文俊的指點和支援，1992年5月，張景中到美國威奇塔州立大學遊學，吳文俊給張景中寫了三頁紙的英文推薦信。張景中對中國人工智能的又一貢獻，是和成都七中1990年數學綜合實驗班的帶隊老師謝晉超合作做吳方法的機器定理證明的實作，具體做這個工作的，正是謝晉超當時的得意門生王小川，他是IOI11996年金牌得主，後來創辦了搜狗公司，任首席執行官。
回過頭說吳文俊，吳文俊從20世紀80年代起一直緻力于數學機械化的研究與推廣，并得到了北大教授程民德的支援。程民德、吳文俊和另兩位數學大家陳省身、胡國定是“中國數學要在21世紀率先趕上世界先進水準”的提出者，是數學天元基金的創始人，程民德的另一身份是中科院資訊技術科學部資訊學組的副組長，他和資訊學組的組長常迵對中國資訊化以及人工智能的發展有着不小的貢獻。
1990年年初，程民德指導編寫了一份關于機器證明研究的國際回報材料呈交國家科學技術委員會（下稱“科委”）上司。當時，日本第五代智能計算機的研究一度呈現出火熱的狀态，但最終因數學理論和方法存在重大缺陷而放棄，而吳方法的研究有望給智能計算機的研制提供新的數學理念。6月，國家科委基礎研究高技術司（下稱“基礎司”）上司到中科院系統科學研究所座談，就如何進一步支援吳文俊的機器證明工作聽取了意見，吳文俊、程民德等人參與了座談會。座談會結束後不久，基礎司撥出100萬元專款支援機器證明的研究。有了這筆撥款，吳文俊很快在中科院系統科學研究所成立了數學機械化研究中心，吳文俊任主任，程民德任學術委員會主任，日常工作由北京市計算中心的吳文達主持。程民德還和石青雲院士合作将吳方法應用于整體視覺，并指導研究所學生李洪波開創了幾何定理機器證明的新方向。
《人工智能：伏羲覺醒》（2016）劇照。
數學機械化研究中心成立之後，吳文俊又從應用出發，對符号和數值混合算法進行進一步研究。他在20世紀90年代初指出，符号計算和數值計算是兩種不同的解決科學和技術發展中問題的計算方法，符号計算可以得到問題精确的完備解，但計算量大且表現形式往往十分複雜；數值計算可以快速處理許多實際應用問題，但一般隻能得到局部近似解。
吳文俊曾提出一切工程問題最終都要轉化為數學問題，一切數學問題最終都要轉化為方程求解的問題，混合算法的研究也為數學機械化研究中心在後續負責的數學機械化與自動推理平台及國家重點基礎研究發展計劃（973計劃）項目“機構學及數控技術中的數學機械化方法”中提出求解最優化問題等提供了有效的綜合方法。近年來，機器證明不僅應用在證明和輔助發現數學新定理方面，還創造或發展出一些新的方法和代數工具，用來解決計算機輔助設計、機器人控制、計算機視覺以及其他有關的數學問題。
跳出數學圈子，緻力于發揮計算機的威力
除吳文俊外，當時國内還有一位數學家在機器定理證明領域聞名，他就是吉林大學的王湘浩。與吳文俊不同的是，王湘浩并沒有局限于将計算機應用于數學研究，而是跳出數學圈子，緻力于發揮計算機的威力，對人工智能的體系化發展起到了關鍵作用。
王湘浩1915年出生于河北省安平縣，從小喜歡數學。1946年夏天，王湘浩獲得美國國務院獎學金赴普林斯頓大學留學。他選擇代數學作為研究方向，導師是當代著名代數學家埃米爾·阿廷（Emil Artin），是以他與沃爾夫獎、阿貝爾獎獲得者約翰·泰特（John Tate）是師兄弟。王湘浩僅用一年時間就取得了碩士學位。在剩下的兩年時間裡，他又拿下了博士學位。能在如此短的時間拿到碩士、博士學位，除了比常人更加勤奮和努力，另一個原因大概是助學金不夠用（這也是當時留美的學生常見的狀态），想趕緊念完書。可見，人在壓力下的潛力是無窮的。
王湘浩通過博士論文答辯後于1949年回國，被母校北京大學數學系聘為副教授，講授代數數論等專業課及其他基礎課程。當時的學生中就包含後來的北大校長丁石孫。吳文俊于1951年回國後一開始也在北京大學數學系任教，兩人從那時便相熟起來。後來，王湘浩到吉林大學主持工作，博士生論文答辯一般會邀請吳文俊進入答辯委員會，其他常被邀請的還有陸汝钤、董蘊美等。加上王湘浩，一場博士答辯，四個院士坐鎮，陣容十分豪華。
1952年全國院系大重組，吳文俊被調往中科院數學研究所，王湘浩則北上吉林大學，先後成為吉林大學數學系和計算機系的首任系主任，并任副校長之職。1955年，憑借此前在代數數論方面的研究與對格倫瓦爾德定理的補充，王湘浩當選為中國科學院第一批學部委員（也就是後來的科學院院士），是數學方向最早的9位學部委員之一，而吳文俊則是數學方向第10位學部委員，是以說王湘浩比吳文俊還要資深一些。
紀錄片《現代生活的秘密規則：算法》（2015）劇照。
王湘浩也是最早從數學方向轉向計算機方向的院士。1955年，王湘浩在吉林大學數學系制定了研究規劃，其中就包含了計算數學。次年，國務院完成了《1956—1967年科學技術發展遠景規劃》（簡稱《十二年科技規劃》）的制定，将計算機、自動化、電子學、半導體列為需要重點快速發展的領域，這也加速了吉林大學計算數學專業建設的步伐。
1957至1959年，吉林大學聘請蘇聯專家梅索夫斯基赫開辦了計算數學講義班，參加的老師包括北京大學的徐卓群和徐萃薇、複旦大學的蔣爾雄、武漢大學的康立山等人。兩年的講義班讓李榮華、李嶽生、馮果忱等一批本土教師成長起來，再加上有王湘浩坐鎮，已經足以奠定吉林大學在國内計算數學領域的領先地位。在這一時期，王湘浩兼任計算數學教研室的主任，他也從數學轉到計算機領域，成了吉林大學計算機學科的創始人。
王湘浩當時主要研究的是歸結原理，這也是定理證明的三種算法之一。歸結原理由約翰·阿蘭·羅賓遜（John Alan Robinson）在1965年改進埃爾布朗定理後提出，但其應用範圍比較窄，王湘浩和他的學生劉叙華在此基礎上對歸結原理進行了很多改進，提出了廣義歸結和鎖語義歸結，并指出了國外提出的有序線性歸結（OL歸結）的錯誤，提出了修改後的有序線性歸結（MOL歸結）。
王湘浩在吉林大學建立了多個研究小組，成果最豐碩的當數他領頭的多值邏輯小組，自動機小組、計算機代數小組等也都發展得不錯。後來，吉林大學在1976年成立計算機系，計算機系的幾個主要研究方向也都是從之前的小組演化而來的，并且在向人工智能靠攏的過程中又逐漸形成了兩大方向：自動推理模型及其證明、專家系統與知識工程，前者由劉叙華擔綱，後者由管紀文負責。這些基礎理論研究的重要成果也為王湘浩之後在國内首先倡導人工智能研究打下了基礎。
20世紀70年代的吉林大學由于計算數學研究開展得早，老中青三代師資力量齊備，又有這一領域資曆最老的學部委員王湘浩坐鎮群組織，已然成為當時計算機與人工智能研究的中心。當時正值國内多所院校建立計算機系，吉林大學也接待了不少來“取經”的老師，這也為1979年的“計算機科學暑期讨論會”的召開打下了基礎。
20世紀70年代數學與邏輯學是人工智能的主流
1979年7月23日到30日，剛剛恢複活動不久的中國電子學會計算機學會（中國計算機學會的前身）在吉林大學召開了“計算機科學暑期讨論會”，會議由吉林大學、北京大學、中科院計算技術研究所、吉林省計算機技術研究所共同籌辦，王湘浩擔任會議上司小組組長，會議小組其他成員包括吳允曾、吳文俊、劉聲烈、陸汝钤、曹履冰、吳治衡、張兆慶、羅鑄楷、陳炳從、金淳兆、張鳴華、許孔時等，吳文俊、吳允曾、陸汝钤、張鳴華在全體會議上作了專題學術報告。會議分為智能模拟（人工智能）、計算機科學基本理論與作業系統、形式語言及編譯理論、硬體理論及應用四個專題。
人工智能是這次讨論會最重要的一個方向——1978年3月全國科學大會制定了《1978—1985年全國科學技術發展規劃綱要》（簡稱《八年規劃綱要》），将“智能模拟”列為計算機科學的重要研究方向，也帶動了一批研究者涉足人工智能領域。而吳文俊剛剛完成幾何定理機器證明的吳方法，這一突破引起國内外諸多研究者的興趣。在1979年7月25日上午的大會報告環節，吳文俊作了關于幾何定理機器證明的報告。在分組讨論中，他親自擔任智能模拟組的組長。有吳文俊坐鎮，智能模拟組的讨論也比其他幾個組要熱鬧幾分。
計算機科學暑期讨論會代表證（提供者為何華燦，《中國人工智能簡史：從1979到1993》内文插圖）。
在吳文俊之後作報告的是中科院計算技術研究所的陸汝钤，報告主題是“軟體移植的工程實作”。陸汝钤也是數學家出身，1959年畢業于德國耶拿大學數學系，1972年“轉行”進入計算機科學領域，在1975—1981年倡導并主持旨在軟體機械生成和自動移植的系列軟體計劃（下稱“XR計劃”）。當時，計算機研究在國内逐漸展開，但軟體數量少，編寫成本高（按陸汝钤的統計，一條計算機指令的開發成本大概在10美元），軟體成了阻礙計算機普及的絆腳石。XR計劃以大陸廣泛使用的幾類計算機為對象，解決了不同平台之間的軟體移植問題，推動了當時國産機軟體缺乏問題的解決。陸汝钤之後将這種基于知識的智能化軟體工程思想進一步延伸到知識工程語言TUILI（推理）和國家七五攻關項目“專家系統開發環境”中，并因在人工智能領域的突出貢獻獲得了首屆吳文俊人工智能科學技術獎。
第二天上午的另兩個大會報告也和人工智能有關。吳允曾來自主辦方之一的北京大學，他是著名的數理邏輯學家和計算機科學家，先後在北京大學哲學系、數學系和計算機專業任教，由哲學到數學，從數理邏輯到計算機，在每一個領域均取得相當大的成就。吳允曾很早就意識到哲學和數理邏輯是計算機科學的基礎，在本次大會上，他的報告主題是“希爾伯特第十問題與計算機化”。希爾伯特第十問題是一個與解方程有關的問題，哥德爾、丘奇、圖靈等大師對這一問題均有關鍵性的研究，這一問題的計算機化正是對計算本質的了解與探索，頗具指導意義。
最後一名報告嘉賓是來自清華大學的張鳴華。張鳴華1952年從清華大學數學系畢業後留校，是清華大學開展計算數學教學時最早的任課教師之一。他之後專攻計算理論和計算機科學基本理論的研究，著有《可計算性理論》一書。可計算性不僅是計算機科學的基礎，也是人工智能的關鍵。可計算理論的基本思想被用于程式設計，産生了遞歸過程和遞歸資料結構，他在大會所做的報告主題是“資料流分析”。張鳴華在本屆大會上還有一篇名為《框圖格式的等價問題》的論文發表，該論文被評為大會在優秀論文并被推薦到全國計算機年會。
這場會議實際上也是中國人工智能研究的一個“摸底會”。不少參會者是從“智能模拟”被列為計算機科學的重要方向之後才開始接觸人工智能的，到這場會議召開時不過一年時間，很難有深入的了解和研究，而吉林大學則顯示出在人工智能研究上的先發優勢，王湘浩的《廣義歸結》、管紀文的《線性自動機的極大周期定理》和《線性自動機的奇偶性》、劉叙華的《鎖語義歸結原理和模糊邏輯》均入選大會優秀論文。
另外一所表現突出的學校是武漢大學。曾憲昌的兩個學生劉初長和代大為的論文（分别為《代德景問題的機械算法》和《Dedekind問題的圖表算法》）也入選大會優秀論文。與吳文俊、王湘浩并稱“機器證明三傑”的曾憲昌也是從數學轉向計算機的。曾憲昌出生于數學世家，父親是頗有影響力的數學史專家和曆算專家、中國數學會的建立人之一曾昭安。1928年國立武昌中山大學改建為“國立武漢大學”時，曾昭安就是籌備委員會委員。曾憲昌是數學家湯璪真的學生，他在20世紀40年代末留美，和父親一樣在哥倫比亞大學學習數學，并遵照父親曾昭安的囑咐，對20世紀40年代末出現在美國費城的世界上第一台電子計算機進行實地考察。曾憲昌回國時帶回一批有關計算機科學的資料，這批資料在20世紀70年代創設武漢大學計算機系時發揮了重要的參考作用。
紀錄片《現代生活的秘密規則：算法》（2015）劇照。
曾憲昌長期從事數學和計算機科學的教學工作，他學識淵博，功力深厚，通曉英、俄、德、法、日五種語言，在數學系和計算機科學系為大學生主講過數論、高等代數、方程式論、代數整數論、近世代數、方程式的機械求解等課程，為研究所學生開設過定理機器證明、機器學習、智能軟體工程等課程，編寫出版了《方程式論》《高等代數》《代數數論》《代數結構》等重要教材。由于在數學理論和計算機科學的定理證明方面取得了突出的學術成就，他被教育部任命為中國代表團團長，出席了在美國華盛頓召開的國際計算機1979年年會；同年底，又出席了在美國底特律近郊舉行的1979年國際并行處理會議，發表了兩篇論文，刊登在該會的論文集上，受到國内外同行的矚目。
武漢大學曆史上出過不少學術世家，曾家父子算是其中的佼佼者。1958年武大在新三區馬路對面修了兩棟“校長樓”，一号門住的就是曾昭安、曾憲昌父子。20世紀70年代，武漢上馬“一米七軋機”工程，項目召集武漢各高校相關研究者協同攻關，前期的不少技術文檔就是由曾昭安翻譯的，曾憲昌也參與了用計算機對“一米七軋機”工程進行優化的工作。1978年，武漢大學成立計算機系，曾憲昌也成了武漢大學計算機系首批招收研究所學生的導師。當時成立計算機系時武漢大學的研究所學生招生已經結束，學生已到校報到，數學系臨時從這一批已經學習了兩個多月的學生中調配了三個人去計算機系讀曾憲昌的研究所學生，曾憲昌為這一批研究所學生標明的研究主題，正是機器定理證明。
王湘浩和曾憲昌研究機器定理證明的終極目标是實作自動推理，這也是很多數學家研究到一定程度後自然而然關注的方向。菲爾茲獎得主弗拉基米爾·沃沃斯基（VladimirVoevodsky）從代數幾何轉向研究自動推理、形式化驗證，就是因為他的一些工作被人構造出反例後，他對自己的很多工作、很多證明産生懷疑，于是開始試圖用可靠的機器驗證代替不可靠的人工檢查。吳文俊自認依然是數學家，但王湘浩、曾憲昌跳出了數學研究本身，從自動推理入手，并将自動推理的能力應用到其他場景中去實作智能化。
由于具有相同的目标和類似的背景，王湘浩和曾憲昌兩個團隊之間也多有合作。如研究所學生畢業答辯，按規定必須有校外專家參加，武漢大學計算機系和吉林大學計算機系便商定，兩個學校的研究所學生一起答辯，這樣就不用再從别的機關請人了。曾憲昌在計算機系最早招收的研究所學生劉初長向筆者回憶稱，當時兩校成立了5人答辯委員會，吉林大學有王湘浩教授、管紀文教授和劉叙華教授，武漢大學有曾憲昌教授和胡久清教授。由于吉林大學計算機系研究所學生多，是以答辯總是安排在吉林大學進行。之後，劉叙華、管紀文、劉初長等還共同組織舉辦高校人工智能學術會議、全國首屆自動推理學術讨論會等多個學術活動，這是後話。
除此之外，值得一提的是來自西北大學的何華燦。何華燦在大會上有一篇名為《仿智學概論》的論文發表，在諸多剛進入人工智能領域的研究者中算是比較突出的。何華燦也是以被王湘浩和吳文俊選中擔任人工智能小組的副組長，輔助吳文俊進行小組成員的召集工作。
從上述論文的内容看，這一時期的人工智能仍然是狹義的人工智能，研究者們研究的重點也大多局限在定理證明和形式邏輯上——這并不奇怪，20世紀70年代是符号主義的時代，數學與邏輯學是人工智能的主流。
這場大會幫助吉林大學樹立了人工智能研究執牛耳的地位，吉林大學的人工智能研究也進入一個空前繁榮的時期。除在中國早期人工智能領域起到積極的推動作用外，吉林大學也培養了幾代優秀學者，管紀文、劉叙華、劉大有等均在其中；在海外開花結果的校友包括美國工程院院士、中國工程院外籍院士、普林斯頓大學教授李凱，以及《人工智能》雜志第一篇華人文章作者、澳洲人工智能理事會主席張成奇，他們均出自吉林大學，受過王湘浩的指點。大會後到吉林大學了解人工智能的姊妹校越來越多。1980年，教育部委托吉林大學舉辦人工智能研究班，清華大學、北京航空學院等16所高校派出老師來到吉林大學學習人工智能。在這個研究班上，何華燦作為西北工業大學教師代表也參加了學習，并是以引出另一段故事。
本文選自《中國人工智能簡史：從1979到1993》，部分小标題為摘編者所加，非原文所有。已獲得出版社授權刊發。
原文作者/林軍 岑峰
摘編/何也
編輯/張進
導語校對/趙琳