關(guān)于作者
一個(gè)畢業(yè)于北京大學(xué)數(shù)學(xué)力學(xué)系，在中國(guó)科學(xué)院計(jì)算所、計(jì)算中心和網(wǎng)絡(luò)中心工作過，在澳大利亞科工組織DMS、香港浸會(huì)學(xué)院數(shù)學(xué)系和中國(guó)21世紀(jì)議程管理中心等處工作過，多次獲國(guó)家和中科院科技獎(jiǎng)并享受政府特殊津貼的退休老頭?，F(xiàn)在在【中國(guó)科普博覽】網(wǎng)“科學(xué)新語林”欄目里開設(shè)一個(gè)《數(shù)學(xué)與計(jì)算機(jī)》的個(gè)人專欄，愿和愛好數(shù)學(xué)與計(jì)算機(jī)的各界網(wǎng)友和青少年朋友，談?wù)剬?duì)數(shù)學(xué)與計(jì)算機(jī)的看法、想法。
計(jì)算機(jī)證明（2）
張建中
2013年04月25日
3. 數(shù)學(xué)定理的計(jì)算機(jī)證明
數(shù)學(xué)定理的計(jì)算機(jī)證明，又稱機(jī)器證明，有廣義和狹義之說。
廣義之說是，數(shù)學(xué)定理的機(jī)器證明，顧名思義，就是通過機(jī)器的有限步推斷完成一般數(shù)學(xué)定理的證明，簡(jiǎn)稱為機(jī)器證明，又稱為機(jī)械化證明、自動(dòng)證明，因計(jì)算機(jī)是實(shí)現(xiàn)這類證明的最好機(jī)器，甚至也可以說是現(xiàn)在唯一真正可用的機(jī)器，所以常稱為計(jì)算機(jī)證明；狹義之說是，把數(shù)學(xué)的某一類命題（數(shù)量可很多）從整體上加以考慮，建立統(tǒng)一的、確定的證明程序，經(jīng)計(jì)算機(jī)有限步推斷給出數(shù)學(xué)命題真假的證明,真者就成為定理。
從廣義上講，如四色定理、費(fèi)馬大定理等在計(jì)算機(jī)上進(jìn)行的證明，應(yīng)屬于數(shù)學(xué)定理計(jì)算機(jī)證明的；但這類證明，一事一例，獨(dú)具特點(diǎn)，不是對(duì)一類數(shù)學(xué)定理的證明，因此，從狹義上講，它們并不屬于數(shù)學(xué)定理的計(jì)算機(jī)證明。
數(shù)學(xué)定理的計(jì)算機(jī)證明是現(xiàn)代數(shù)學(xué)中一個(gè)新興的邊緣性學(xué)科，也是現(xiàn)代人工智能發(fā)展的一個(gè)重要方向，以下均簡(jiǎn)稱為機(jī)器證明或計(jì)算機(jī)證明。從傳統(tǒng)的定理手工證明到定理計(jì)算機(jī)證明，是現(xiàn)代數(shù)學(xué)思想方法的一次重大突破，既是計(jì)算機(jī)和人工智能發(fā)展的產(chǎn)物，也是數(shù)學(xué)自身發(fā)展的需要。
4. 計(jì)算機(jī)證明的可行性
西方的幾何學(xué)是由歐幾里德建立的一套公理化系統(tǒng)發(fā)展起來的，是按照定義——公理——定理——證明的演繹系統(tǒng)進(jìn)行的。顯然，這種公理化體系的幾何定理證明現(xiàn)在還很難實(shí)現(xiàn)機(jī)械化。由于幾何在數(shù)學(xué)中的歷史地位及在數(shù)學(xué)教育中的重要作用，對(duì)幾何定理進(jìn)行計(jì)算機(jī)證明成了這一領(lǐng)域中的研究重點(diǎn)。
如何利用機(jī)器進(jìn)行自動(dòng)推理，特別是進(jìn)行幾何定理的自動(dòng)證明，是西方學(xué)術(shù)界長(zhǎng)期以來試圖研究解決的問題。事實(shí)上，17世紀(jì)大數(shù)學(xué)家萊布尼茲就有機(jī)械化證明的設(shè)想；直到19世紀(jì)末，由于希爾伯特（David Hilbert）及其追隨者建立并發(fā)展了數(shù)理邏輯，這一問題才有了明確的數(shù)學(xué)形式；又由于20世紀(jì)40年代計(jì)算機(jī)的出現(xiàn)，才使這一設(shè)想有了實(shí)現(xiàn)的可能和條件。
歷史上一些大師級(jí)的數(shù)學(xué)家，曾在幾何定理計(jì)算機(jī)證明這條路上進(jìn)行過艱苦的探索。
為了用統(tǒng)一的方法處理千變?nèi)f化的幾何問題，笛卡爾（Ren Descartes）發(fā)明了坐標(biāo)方法，創(chuàng)立了解析幾何。跨19世紀(jì)、20世紀(jì)的大數(shù)學(xué)家希爾伯特，在它的名著《幾何基礎(chǔ)》中，曾給出了一類幾何問題的機(jī)械化解題方法。電子計(jì)算機(jī)的出現(xiàn)，大大加快了數(shù)學(xué)定理計(jì)算機(jī)證明研究的進(jìn)程，促進(jìn)了幾何問題求解的計(jì)算機(jī)證明研究。
1948年，塔斯基（Alfred Tarski）發(fā)表了一條引人注目的定理：“一切初等幾何和初等代數(shù)命題構(gòu)成的命題類，是可判定的”。這里，所謂“命題”是一個(gè)具有前提和結(jié)論的判斷句；如果命題的前提和結(jié)論都可以用有限個(gè)整系數(shù)多項(xiàng)式的等式或不等式表達(dá)，就叫做初等幾何和初等代數(shù)命題。如果有一套機(jī)械的方法，對(duì)于某個(gè)命題類的任一個(gè)命題，都能用這套方法經(jīng)有限步的操作確定命題的真假，就說這個(gè)命題類是“可判定的”。
1975年，考林斯（Collins）提出“柱面代數(shù)分解方法”，比塔斯基的方法效率提高了很多，但在計(jì)算機(jī)上仍只能解決個(gè)別稍有難點(diǎn)的幾何問題。
笛卡爾——塔斯基——考林斯，這是用代數(shù)方法尋求幾何問題機(jī)械求解的一條線。
另一條路線，是企圖把解決幾何問題的傳統(tǒng)綜合方法機(jī)械化，通常叫做后推搜索法，又提出了更有效的前推搜索法。這類方法，由于搜索空間過大等問題，未能形成有效的算法。
計(jì)算機(jī)早期只會(huì)進(jìn)行單一的數(shù)值計(jì)算，到了20世紀(jì)60年代中，用它能做符號(hào)計(jì)算，有理式的四則運(yùn)算，多項(xiàng)式的因式分解，求最小公倍式和最大公因式，甚至還能計(jì)算符號(hào)微積分，為幾何問題的計(jì)算機(jī)證明提供了強(qiáng)有力的工具。
1977年，我國(guó)著名數(shù)學(xué)家吳文俊院士在《中國(guó)科學(xué)》雜志上發(fā)表了論文“初等幾何判定問題與機(jī)械化證明”，提出了一個(gè)證明等式型初等幾何定理的新的代數(shù)方法。1984年，中國(guó)留美學(xué)者周咸青在他的博士論文中把這個(gè)方法叫做“吳方法”，并列出了基于吳方法所編寫的程序證明的130個(gè)幾何定理。不久，他又在一本專著中列出了用吳方法證明的512個(gè)幾何定理。吳方法從此在國(guó)際自動(dòng)推理研究領(lǐng)域廣為傳播。
1984年，吳文俊院士的學(xué)術(shù)專著《幾何定理計(jì)算機(jī)證明的基本原理（初等幾何部分）》出版。這本專著遵循機(jī)械化思想引進(jìn)數(shù)系和公理，依照機(jī)械化觀點(diǎn)系統(tǒng)地分析了各類幾何體系，諸如帕斯卡幾何（Pascal's theorem），垂直幾何，度量幾何，歐氏幾何等，證明確立了各類幾何的機(jī)械化定理，系統(tǒng)地闡明了幾何定理機(jī)械化證明代數(shù)方法的基本原理。
1993年，張景中、楊路、高小山和周咸青等人把消點(diǎn)法推廣到了非歐幾何，用計(jì)算機(jī)發(fā)現(xiàn)了幾十條非歐幾何的新定理，并且自動(dòng)生成了它們的可讀證明。
迄今，人們已經(jīng)用計(jì)算機(jī)證明了上百條重要的數(shù)學(xué)定理，甚至還曾經(jīng)用計(jì)算機(jī)發(fā)現(xiàn)過一些猜想。
5. 計(jì)算機(jī)證明的應(yīng)用
目前，計(jì)算機(jī)證明作為數(shù)學(xué)研究的一種方法，還存在著許多理論和技術(shù)上的問題，這些問題的解決將有待于算法理論、計(jì)算機(jī)科學(xué)和人工智能等各個(gè)領(lǐng)域出現(xiàn)新的重大突破。
近30多年來，數(shù)學(xué)定理計(jì)算機(jī)證明的研究從基礎(chǔ)研究領(lǐng)域擴(kuò)展到了應(yīng)用研究和開發(fā)研究領(lǐng)域。這里所說的應(yīng)用既有間接的，也有直接的。
在研究幾何定理計(jì)算機(jī)證明時(shí)，創(chuàng)造或發(fā)展了一些新的方法或代數(shù)工具，它們可以用來解決其他領(lǐng)域的問題，如機(jī)構(gòu)設(shè)計(jì)、曲面造型、計(jì)算機(jī)輔助設(shè)計(jì)、機(jī)器人控制、計(jì)算機(jī)視覺以及其他有關(guān)的數(shù)學(xué)問題，這是間接應(yīng)用。
把幾何定理機(jī)器求解的程序發(fā)展為軟件，或者嵌入計(jì)算機(jī)應(yīng)用軟件，這是直接的應(yīng)用。這類應(yīng)用的實(shí)際需求，主要有兩個(gè)方面：一是為研究者、教師和數(shù)學(xué)愛好者提供智能性幾何解題電子詞典，對(duì)兩千多年的初等幾何作一個(gè)相對(duì)完美的總結(jié)；二是應(yīng)用幾何定理機(jī)器求解研究的成果，可以研制出高智能的教育軟件。
通過計(jì)算機(jī)證明，解決了數(shù)學(xué)中的百年難題，如四色猜想、費(fèi)馬大定理等，開闊了人類的視野，為數(shù)學(xué)發(fā)展開辟了一條新途徑，意義重大，也是計(jì)算機(jī)證明的又一直接應(yīng)用。
計(jì)算機(jī)證明同樣有導(dǎo)致發(fā)現(xiàn)的功能，其中一個(gè)較為典型的例子是分形幾何的創(chuàng)立。早在20世紀(jì)20年代，法國(guó)數(shù)學(xué)家朱利亞（Gaston Julia）就開始著手研究分形幾何，但是由于這種幾何圖形的驚人復(fù)雜性，朱利亞的研究沉寂了幾十年。直到60年代以后，美國(guó)數(shù)學(xué)家曼德勃羅 ( B.Mandelbrot )開始用計(jì)算機(jī)來畫圖，才使分形幾何得到了真正的發(fā)展。
數(shù)學(xué)定理的計(jì)算機(jī)證明，又稱機(jī)器證明，有廣義和狹義之說。
廣義之說是，數(shù)學(xué)定理的機(jī)器證明，顧名思義，就是通過機(jī)器的有限步推斷完成一般數(shù)學(xué)定理的證明，簡(jiǎn)稱為機(jī)器證明，又稱為機(jī)械化證明、自動(dòng)證明，因計(jì)算機(jī)是實(shí)現(xiàn)這類證明的最好機(jī)器，甚至也可以說是現(xiàn)在唯一真正可用的機(jī)器，所以常稱為計(jì)算機(jī)證明；狹義之說是，把數(shù)學(xué)的某一類命題（數(shù)量可很多）從整體上加以考慮，建立統(tǒng)一的、確定的證明程序，經(jīng)計(jì)算機(jī)有限步推斷給出數(shù)學(xué)命題真假的證明,真者就成為定理。
從廣義上講，如四色定理、費(fèi)馬大定理等在計(jì)算機(jī)上進(jìn)行的證明，應(yīng)屬于數(shù)學(xué)定理計(jì)算機(jī)證明的；但這類證明，一事一例，獨(dú)具特點(diǎn)，不是對(duì)一類數(shù)學(xué)定理的證明，因此，從狹義上講，它們并不屬于數(shù)學(xué)定理的計(jì)算機(jī)證明。
數(shù)學(xué)定理的計(jì)算機(jī)證明是現(xiàn)代數(shù)學(xué)中一個(gè)新興的邊緣性學(xué)科，也是現(xiàn)代人工智能發(fā)展的一個(gè)重要方向，以下均簡(jiǎn)稱為機(jī)器證明或計(jì)算機(jī)證明。從傳統(tǒng)的定理手工證明到定理計(jì)算機(jī)證明，是現(xiàn)代數(shù)學(xué)思想方法的一次重大突破，既是計(jì)算機(jī)和人工智能發(fā)展的產(chǎn)物，也是數(shù)學(xué)自身發(fā)展的需要。
4. 計(jì)算機(jī)證明的可行性
西方的幾何學(xué)是由歐幾里德建立的一套公理化系統(tǒng)發(fā)展起來的，是按照定義——公理——定理——證明的演繹系統(tǒng)進(jìn)行的。顯然，這種公理化體系的幾何定理證明現(xiàn)在還很難實(shí)現(xiàn)機(jī)械化。由于幾何在數(shù)學(xué)中的歷史地位及在數(shù)學(xué)教育中的重要作用，對(duì)幾何定理進(jìn)行計(jì)算機(jī)證明成了這一領(lǐng)域中的研究重點(diǎn)。
如何利用機(jī)器進(jìn)行自動(dòng)推理，特別是進(jìn)行幾何定理的自動(dòng)證明，是西方學(xué)術(shù)界長(zhǎng)期以來試圖研究解決的問題。事實(shí)上，17世紀(jì)大數(shù)學(xué)家萊布尼茲就有機(jī)械化證明的設(shè)想；直到19世紀(jì)末，由于希爾伯特（David Hilbert）及其追隨者建立并發(fā)展了數(shù)理邏輯，這一問題才有了明確的數(shù)學(xué)形式；又由于20世紀(jì)40年代計(jì)算機(jī)的出現(xiàn)，才使這一設(shè)想有了實(shí)現(xiàn)的可能和條件。
歷史上一些大師級(jí)的數(shù)學(xué)家，曾在幾何定理計(jì)算機(jī)證明這條路上進(jìn)行過艱苦的探索。
為了用統(tǒng)一的方法處理千變?nèi)f化的幾何問題，笛卡爾（Ren Descartes）發(fā)明了坐標(biāo)方法，創(chuàng)立了解析幾何。跨19世紀(jì)、20世紀(jì)的大數(shù)學(xué)家希爾伯特，在它的名著《幾何基礎(chǔ)》中，曾給出了一類幾何問題的機(jī)械化解題方法。電子計(jì)算機(jī)的出現(xiàn)，大大加快了數(shù)學(xué)定理計(jì)算機(jī)證明研究的進(jìn)程，促進(jìn)了幾何問題求解的計(jì)算機(jī)證明研究。
1948年，塔斯基（Alfred Tarski）發(fā)表了一條引人注目的定理：“一切初等幾何和初等代數(shù)命題構(gòu)成的命題類，是可判定的”。這里，所謂“命題”是一個(gè)具有前提和結(jié)論的判斷句；如果命題的前提和結(jié)論都可以用有限個(gè)整系數(shù)多項(xiàng)式的等式或不等式表達(dá)，就叫做初等幾何和初等代數(shù)命題。如果有一套機(jī)械的方法，對(duì)于某個(gè)命題類的任一個(gè)命題，都能用這套方法經(jīng)有限步的操作確定命題的真假，就說這個(gè)命題類是“可判定的”。
波蘭裔猶太邏輯學(xué)家、數(shù)學(xué)家、語言哲學(xué)家阿 塔斯基 (1901–1983)
1975年，考林斯（Collins）提出“柱面代數(shù)分解方法”，比塔斯基的方法效率提高了很多，但在計(jì)算機(jī)上仍只能解決個(gè)別稍有難點(diǎn)的幾何問題。
笛卡爾——塔斯基——考林斯，這是用代數(shù)方法尋求幾何問題機(jī)械求解的一條線。
另一條路線，是企圖把解決幾何問題的傳統(tǒng)綜合方法機(jī)械化，通常叫做后推搜索法，又提出了更有效的前推搜索法。這類方法，由于搜索空間過大等問題，未能形成有效的算法。
計(jì)算機(jī)早期只會(huì)進(jìn)行單一的數(shù)值計(jì)算，到了20世紀(jì)60年代中，用它能做符號(hào)計(jì)算，有理式的四則運(yùn)算，多項(xiàng)式的因式分解，求最小公倍式和最大公因式，甚至還能計(jì)算符號(hào)微積分，為幾何問題的計(jì)算機(jī)證明提供了強(qiáng)有力的工具。
1977年，我國(guó)著名數(shù)學(xué)家吳文俊院士在《中國(guó)科學(xué)》雜志上發(fā)表了論文“初等幾何判定問題與機(jī)械化證明”，提出了一個(gè)證明等式型初等幾何定理的新的代數(shù)方法。1984年，中國(guó)留美學(xué)者周咸青在他的博士論文中把這個(gè)方法叫做“吳方法”，并列出了基于吳方法所編寫的程序證明的130個(gè)幾何定理。不久，他又在一本專著中列出了用吳方法證明的512個(gè)幾何定理。吳方法從此在國(guó)際自動(dòng)推理研究領(lǐng)域廣為傳播。
1984年，吳文俊院士的學(xué)術(shù)專著《幾何定理計(jì)算機(jī)證明的基本原理（初等幾何部分）》出版。這本專著遵循機(jī)械化思想引進(jìn)數(shù)系和公理，依照機(jī)械化觀點(diǎn)系統(tǒng)地分析了各類幾何體系，諸如帕斯卡幾何（Pascal's theorem），垂直幾何，度量幾何，歐氏幾何等，證明確立了各類幾何的機(jī)械化定理，系統(tǒng)地闡明了幾何定理機(jī)械化證明代數(shù)方法的基本原理。
《幾何定理機(jī)器證明的基本原理》一書
1993年，張景中、楊路、高小山和周咸青等人把消點(diǎn)法推廣到了非歐幾何，用計(jì)算機(jī)發(fā)現(xiàn)了幾十條非歐幾何的新定理，并且自動(dòng)生成了它們的可讀證明。
迄今，人們已經(jīng)用計(jì)算機(jī)證明了上百條重要的數(shù)學(xué)定理，甚至還曾經(jīng)用計(jì)算機(jī)發(fā)現(xiàn)過一些猜想。
5. 計(jì)算機(jī)證明的應(yīng)用
目前，計(jì)算機(jī)證明作為數(shù)學(xué)研究的一種方法，還存在著許多理論和技術(shù)上的問題，這些問題的解決將有待于算法理論、計(jì)算機(jī)科學(xué)和人工智能等各個(gè)領(lǐng)域出現(xiàn)新的重大突破。
近30多年來，數(shù)學(xué)定理計(jì)算機(jī)證明的研究從基礎(chǔ)研究領(lǐng)域擴(kuò)展到了應(yīng)用研究和開發(fā)研究領(lǐng)域。這里所說的應(yīng)用既有間接的，也有直接的。
在研究幾何定理計(jì)算機(jī)證明時(shí)，創(chuàng)造或發(fā)展了一些新的方法或代數(shù)工具，它們可以用來解決其他領(lǐng)域的問題，如機(jī)構(gòu)設(shè)計(jì)、曲面造型、計(jì)算機(jī)輔助設(shè)計(jì)、機(jī)器人控制、計(jì)算機(jī)視覺以及其他有關(guān)的數(shù)學(xué)問題，這是間接應(yīng)用。
把幾何定理機(jī)器求解的程序發(fā)展為軟件，或者嵌入計(jì)算機(jī)應(yīng)用軟件，這是直接的應(yīng)用。這類應(yīng)用的實(shí)際需求，主要有兩個(gè)方面：一是為研究者、教師和數(shù)學(xué)愛好者提供智能性幾何解題電子詞典，對(duì)兩千多年的初等幾何作一個(gè)相對(duì)完美的總結(jié)；二是應(yīng)用幾何定理機(jī)器求解研究的成果，可以研制出高智能的教育軟件。
通過計(jì)算機(jī)證明，解決了數(shù)學(xué)中的百年難題，如四色猜想、費(fèi)馬大定理等，開闊了人類的視野，為數(shù)學(xué)發(fā)展開辟了一條新途徑，意義重大，也是計(jì)算機(jī)證明的又一直接應(yīng)用。
計(jì)算機(jī)證明同樣有導(dǎo)致發(fā)現(xiàn)的功能，其中一個(gè)較為典型的例子是分形幾何的創(chuàng)立。早在20世紀(jì)20年代，法國(guó)數(shù)學(xué)家朱利亞（Gaston Julia）就開始著手研究分形幾何，但是由于這種幾何圖形的驚人復(fù)雜性，朱利亞的研究沉寂了幾十年。直到60年代以后，美國(guó)數(shù)學(xué)家曼德勃羅 ( B.Mandelbrot )開始用計(jì)算機(jī)來畫圖，才使分形幾何得到了真正的發(fā)展。
分形幾何圖形一例