數(shù)學(xué)是“科學(xué)的皇后”，不僅代表著人類智力的最高挑戰(zhàn)，同時也在人類社會和歷史發(fā)展中起著不可替代的推動作用，可以毫不夸張的說數(shù)學(xué)已經(jīng)成為人類現(xiàn)代文明的基石。
數(shù)理邏輯是人工智能三大學(xué)派之一符號學(xué)派的思想源頭和理論基礎(chǔ)，因此用人工智能方法解決所有數(shù)學(xué)問題成為了早期人工智能專家關(guān)注的重要目標(biāo)之一。數(shù)學(xué)的計算機(jī)證明與人工智能的發(fā)展關(guān)系密切，我國著名數(shù)學(xué)家吳文俊院士從中國數(shù)學(xué)史的研究中汲取了靈感，是這一領(lǐng)域的早期推動者之一，做出了巨大貢獻(xiàn)。
人工智能證明數(shù)學(xué)定理
1956年，在美國漢諾斯小鎮(zhèn)寧靜的達(dá)特茅斯學(xué)院召開了一次用機(jī)器來模仿人類學(xué)習(xí)以及其他方面的智能的會議，這次會議被認(rèn)為是人工智能的開端，紐厄爾(Allen Newell)和西蒙(Herbert Simon) 在會議上公布了一款被稱為“邏輯理論家” 程序(Logic Theorist)，成功證明了羅素和懷特海所著的《數(shù)學(xué)原理》第二章52 條定理中的38條, 從而開創(chuàng)了人工智能方法證明數(shù)學(xué)定理的開端。
達(dá)特茅斯學(xué)院（圖片來源：中國人工智能學(xué)會https://mp.weixin.qq.com/s/5uJKqu2Xv3LVM2ZFpfsOMg）
僅僅2年之后的1958年，美籍華裔哲學(xué)家王浩在一臺IBM704計算機(jī)上，只用9 分鐘就證明了《數(shù)學(xué)原理》中的一階邏輯部分的全部350 多條定理, 在當(dāng)時數(shù)學(xué)與數(shù)理邏輯界引起轟動。當(dāng)然，紐厄爾和西蒙的“邏輯理論家” 程序使用了“啟發(fā)式搜索”技術(shù)，他們的目標(biāo)是使用計算機(jī)程序模擬出人類智能，而王浩作為數(shù)理邏輯學(xué)家，他的目標(biāo)則是通過計算機(jī)方法證明數(shù)學(xué)定理，后來機(jī)器定理證明成為早期人工智能發(fā)展的一個重要分支。
吳文俊與“吳方法”
在機(jī)器定理證明方面，如果說王浩是邏輯系定理證明的先驅(qū)，吳文俊院士則開創(chuàng)了幾何系定理證明的先河。
吳文俊1919年出生于上海，畢業(yè)于交通大學(xué)數(shù)學(xué)系，后獲法國斯特拉斯堡大學(xué)博士學(xué)位。吳文俊首先受陳省身的指導(dǎo)，從事拓?fù)鋵W(xué)方面的研究。由于在拓?fù)鋵W(xué)中的示性類及示嵌類突出成就，吳文俊被授予首屆國家自然科學(xué)一等獎（同時獲獎的人員為華羅庚以及錢學(xué)森）。1976年開始，吳文俊汲取了中國古代數(shù)學(xué)的精髓，開始了邁向數(shù)學(xué)機(jī)械化證明的全新征程。
初等幾何的傳統(tǒng)證明不是機(jī)械化的，從公理推到最后的結(jié)論往往需要借助靈感，比如證明者需要創(chuàng)造性地畫上許多條輔助線，從而給證明者帶來了很大麻煩。有沒有可能通過算法機(jī)械化地對初等幾何進(jìn)行證明呢？塔爾斯基曾給出結(jié)論說一階實(shí)數(shù)（初等幾何和代數(shù)）是可判定的，這說明，找出算法對所有初等幾何和代數(shù)問題給出證明是有可能做到的。
吳文俊通過研究中國古代數(shù)學(xué)史發(fā)現(xiàn)，中國古代數(shù)學(xué)雖然沒有發(fā)展出希臘歐幾里得公理化的演繹推理體系，卻有非常好的實(shí)際應(yīng)用效果，中國古代數(shù)學(xué)體系包含了高度實(shí)用的算法。我們知道算法是現(xiàn)代計算機(jī)的靈魂，機(jī)械化恰是其最大特點(diǎn)之一。1977年，吳文俊將中國數(shù)學(xué)思想運(yùn)用到初等幾何定理的判定上，提出了平面幾何及微分幾何的判定法,證明了初等幾何主要一類定理的證明可以機(jī)械化。
其證明方法分為3個主要步驟。第一步, 從幾何的公理系統(tǒng)出發(fā), 引進(jìn)數(shù)系統(tǒng)與坐標(biāo)系統(tǒng), 使任意幾何定理的證明問題成為純代數(shù)問題；第二步, 將幾何定理假設(shè)部分的代數(shù)關(guān)系式進(jìn)行整理, 然后依據(jù)確定步驟驗(yàn)證定理終結(jié)部分的代數(shù)關(guān)系是否可以從假設(shè)部分已整理成序的代數(shù)關(guān)系式中推出；第三步, 依據(jù)第二步中的確定步驟編成程序,并在計算機(jī)上實(shí)施, 以得出定理是否成立的最后結(jié)論。吳文俊給出的實(shí)現(xiàn)機(jī)器證明方法被稱為“吳文俊消元法” 或“吳方法”。
吳文俊借鑒了王浩的說法，將這種用機(jī)器證明定理方法稱為“數(shù)學(xué)機(jī)械化”，并在中國科學(xué)院開設(shè)了幾何定理證明課程，中科院計算所的研究生周咸青旁聽了吳文俊的課程，并拿到了吳文俊還未出版的《幾何定理機(jī)器證明的基本原理》的手稿。后來，周咸青在美國德克薩斯大學(xué)奧斯汀分校留學(xué)，周咸青運(yùn)用“吳方法”得出了一些研究成果，使得“吳方法”和吳文俊的名字出現(xiàn)在機(jī)器定理證明界，并引發(fā)關(guān)注。
吳文俊在數(shù)學(xué)所作報告（圖片來源：http://www.amss.ac.cn/wwj/mtbd2017/index_4.html）
60歲開始學(xué)編程，20年不到獲最高獎項
1979年，吳文俊的工作得到了楊振寧的關(guān)注，普林斯頓高等研究院邀請吳文俊訪美，先后在普林斯頓高等研究院、加州大學(xué)伯克利分校以及王浩所在的洛克菲勒大學(xué)講授中國數(shù)學(xué)史和機(jī)器定理證明。普林斯頓的聽眾沒有表現(xiàn)出對機(jī)器定理證明的興趣，但是在加州大學(xué)伯克利分校，著名數(shù)學(xué)家、菲爾茨獎得主斯梅爾（Steve Smale）高度評價了吳文俊的工作，令吳文俊感到欣慰，王浩也積極地將吳文俊的工作成果推向定理證明界的同行，最終使得“吳方法”在國際定理證明界引起重視。
在吳文俊訪美的同一年，當(dāng)時的中科院副院長李昌以及系統(tǒng)科學(xué)研究所關(guān)肇直院士為吳文俊申請到了兩萬五千美元的外匯到美國買了一臺家用電腦，已經(jīng)60歲高齡的他開始學(xué)習(xí)計算機(jī)編程語言，從BASIC語言開始，吳文俊在這臺家用電腦上繼續(xù)開展他的“數(shù)學(xué)機(jī)械化工作”，并取得了豐富的成果，他的“吳方法”也得到進(jìn)一步發(fā)展。1997年，在周咸青的導(dǎo)師博耶爾（Robert Boyer）和華人計算機(jī)科學(xué)家項潔(Jie Hsiang)的提名下，吳文俊獲得機(jī)器定理證明領(lǐng)域的最高獎項Herbrand獎，這是該獎項首次頒發(fā)給中國科學(xué)家。
吳文俊在電腦前工作（圖片來源：中國科學(xué)院數(shù)學(xué)與系統(tǒng)科學(xué)研究院網(wǎng)站http://www.amss.cas.cn/wwj/yrxm/201705/t20170507_4784612.html）
吳文俊對于頒發(fā)給他的諸多榮譽(yù)，說過這樣一句話：“對我個人而言，每次獲獎都是高興的事兒，但對一個國家的科學(xué)發(fā)展而言，稍做出成績，就被大家捧成英雄，像朝圣一樣，這個現(xiàn)象不是好事情，甚至可以說是壞事情，這說明我們的科研還在一個相對落后的階段。要是在這一個領(lǐng)域，發(fā)現(xiàn)有十個八個研究人員的工作都非常好，無法判定誰是英雄，那才說明我們發(fā)展了，進(jìn)步了。”
結(jié)語
許多研究數(shù)學(xué)的人知道，當(dāng)前國際流行的主要符號計算軟件都實(shí)現(xiàn)了中科院院士吳文俊的算法。可以說，吳文俊是我國科研整體水平較為落后的年代里，較少的為人類文明做出過重要貢獻(xiàn)的中國人之一，他在機(jī)器定理證明方面的成就足以讓他的名字寫進(jìn)人工智能發(fā)展的歷史書里。同樣，我們也可以認(rèn)為，中國古代科學(xué)思想蘊(yùn)藏著極大的價值，開發(fā)它對當(dāng)今的科學(xué)技術(shù)發(fā)展仍然有重要的借鑒價值。
參考文獻(xiàn):
[1]尼克.人工智能簡史[M]. 北京：人民郵電出版社，24-54.
[2]紀(jì)志剛.吳文俊與數(shù)學(xué)機(jī)械化[J].上海交通大學(xué)學(xué)報(社會科學(xué)版),2001(03):13-18
[3]傅海倫.定理機(jī)器證明思想的產(chǎn)生與發(fā)展[J].科技導(dǎo)報,2001(06):14-15+30.
[4]陸廣地.吳文俊的貢獻(xiàn)及其對數(shù)學(xué)發(fā)展的推動——深切悼念吳文俊院士[J].廣西民族大學(xué)學(xué)報（自然科學(xué)版）,2017,23(2):20-23.
文章首發(fā)于科學(xué)大院，僅代表作者觀點(diǎn)，不代表科學(xué)大院立場。轉(zhuǎn)載請聯(lián)系cas@cnic.cn?？茖W(xué)大院是中科院官方科普微平臺，由中科院科學(xué)傳播局主辦、中國科普博覽團(tuán)隊運(yùn)營，致力于最新科研成果的深度解讀、社會熱點(diǎn)事件的科學(xué)發(fā)聲。