數學家談研究選題

關於《幾何定理機器可讀證明》選題的思考

張景中

尋求標誌性的進展

我的工作方向本來是「距離幾何」和「動力系統」。1978年底讀了吳文俊院士關於幾何定理機器證明的突破性論文（簡稱「吳法」），深受吳老數學機械化思想的吸引，我清楚地看到這是一個大有前途的方向。但是搞基礎數學的，改大方向談何容易，從熟悉的領域進入一個新的天地，要下大的決心。經過8年的思考和準備，1986年我開始進入機器證明的研究領域。

當時，「吳法」已經在計算機上成功實現，開始在國際上傳播。大家想到的研究題目有3類：第一類是用「吳法」解決各種具體問題；第二類是對「吳法」進行完善和改進；第三類是找尋其他類似「吳法」的幾何定理機器判定的方法。

1986~1991年，我和合作者所作的是上述第二類和第三類的研究。這5年間先是提出並實現了「幾何定理機器判定的數值並行法(多點例證法）」，後來又做出「弱非退化條件」、「正常升列」、「非線性代數方程組相容判定」、「相對分解的整序方法」等結果。這些工作雖然有一定意義，但尚無全局影響，不能算是標誌性的進展。

在機器證明領域中，「吳法」是一個標誌性的進展。「吳法」提出十幾年了，大家都是跟著「吳法」做這三類工作，當然難有大的突破。要有突破，要有標誌性的進展，必須尋求新的道路，研究「吳法」所不能解決的問題。

對權威的觀點要冷靜思考

這時，吳老和許多同行專家都斷言：初等幾何機器證明領域的工作已經結束。除非有挑戰性的問題，不再進行這方面的研究了。

我卻有不同的看法：這個領域的研究並未結束，因為有兩個挑戰性的問題尚未解決。一個是機器證明的可讀性問題；另一個是幾何不等式的機器證明問題。這兩個問題的重要性是眾所周知的，但大家都認為太難了，不去做它。

用「吳法」證明幾何定理，靠的是大量的代數計算，算到最後結果是零，就宣布命題一般成立。至於計算是否有誤，定理成立的幾何理由，人是難以理解，難以檢驗的。這和解方程不同。計算機解方程，雖然計算過程不能檢驗，但結果可以代入驗算。宣布一條定理成立，則是無法驗箅的，要儘可能講明道理。傳統的幾何證明是講得明白的，用機器就講不明白。無論是從哲學上看，從數學文化角度看，還是從數學教育的需求看，可讀證明都是有重要意義的。所以，我就想研究這個問題。

有一次，吳老談起初等幾何的機器證明已經無事可做時，我就請教道：「可不可以讓機器生成容易看懂的證明過程呢?」吳老說：「那不可能」。我是非常敬重吳老的，但始終沒有死了做可讀證明研究的心。

吳老說「不可能」並非隨便說說的。仔細讀他的著作，看到他不止一次地強調機器證明是用冗繁但有章可循的計算來代替簡捷巧妙但法無定法的推演。這和該領域的國際著名專家王浩的看法是一致的。王認為，機器證明就是用量的複雜來代替質的困難。吳老還具體指出，人作幾何題，一題一法，可根據不同情形找尋不同的巧法，機器證明要用統一的演算法解決不同的問題，解題過程不可能簡捷。

權威科學家不認可的研究方向，是不是可以作為選題目標？經過反覆思考，我認為不能一概而論。因為權威的看法並不是嚴密的論證，只來自他們的學術經歷。用大量計算代替巧妙的思考，是「吳法」的成功經驗，但不能否定其他的路。創新的思維可以來自權威的指引，也可能來自權威的光芒照不到的地方。從巧妙的思考中尋求一般的規律，也未必不能成功。計算機能做冗繁的計算，也能做多方面的試探和搜索，這和人們在大量實踐中發現巧妙方法有類似之處。

出於這樣的思考，我傾向於做可讀證明機械化的研究。

對自己的經驗和能力有適當的估計

前面提到，「吳法」出現之後，幾何定理機器證明領域有兩個重要問題。除了可讀機器證明，另一個是不等式的機器證明。吳老指出，不等式的機器證明是「一大難題」。兩者中我選擇了前者，是因為覺得更有可能成功。

選題不能只看重要性，還要估計自己能不能把它吃下來。我1974年就開始研究面積方法，用面積方法解過大量的幾何題。面積方法本來被認為是一種特殊技巧，我在十幾年間把它發展成了系統的一般性方法。從一般性的方法到機械性的演算法，好像只有一步之遙，但有時候這一步就是很難跨過去。坐標法也是一種系統性的一般方法，從坐標法到機械化的「吳法」經過了幾百年的發展。能不能把系統的面積方法發展為機械的演算法？我想有可能，因為我對面積方法、對幾何問題已經十分熟悉了。出於對自己研究經歷和能力的了解，我相信能夠有所突破。

後來的事實表明，認定這個題目是正確的，因為不久果然有了突破。事先下決心做這個題目，倒是用了更久。並且，當我向別人提到這個選題的想法時，沒有誰認真支持這個想法。

選好大題目里的小題目

從機器證明領域裡選擇做可讀證明，是從大題目里選小題目。在選定了做可讀證明之後，仍然不可能把整個問題一口吃下，還有一個再選小題目的問題。

做題目要從易到難，分割解決。這個道理看來粗淺，但是往往當局者迷，胃口過大，或看不準如何分割。

「吳法」在戰略上的高明之處，在於把等式和不等式分開，先做容易突破的等式證明，即無序幾何的證明。而在吳之前的塔斯基、考林斯，沒有做這種分割，想一下子解決，結果效率都上不去。順便提到，在「吳法"突破了等式型幾何命題的機器證明20年後，楊路教授突破了幾何不等式的機器證明的難題。這表明了分割解決戰略的成功。

提出消點方法，在可讀機器證明方面取得關鍵的突破後，我們接著對課題進行了分割。先解決不涉及角度和長度的希爾伯特類命題類，進一步做歐氏幾何的構造性命題類，然後作非歐幾何。這樣下來，一步一步都取得了好的效果。

張景中，計算機科學家、數學家，中國科學院院士。1936年12月生於河南省汝南縣，1959年畢業於北京大學數學力學系。曾任中國科學院成都計算機應用研究所名譽所長，兼任廣州大學計算機教育軟體研究所所長、中國科普作家協會理事長，現任中國科學院成都信息技術有限公司研究員。主要從事機器證明、教育數學、距離幾何及動力系統等領域的研究。其主要研究成果獲國家自然科學獎二等獎1項、國家科技進步獎二等獎1項、國家發明獎二等獎1項、中國科學院自然科學獎一等獎1項、香港國際發明展覽會金獎。1980年以來發表學術論著共150多篇（冊），撰寫了大量科普文章和通俗讀物，被評為新中國成立以來貢獻突出的科普作家。

點評:

不僅要用計算機快速有效地證明幾何定理，而且要由機器自動產生—個個定理的「可讀證明」：即人能夠理解、驗證和接受的證明。這件事初聽起來有點匪夷所思。因為無論是早些年「四色定理」的機器驗證，還是最近熱炒的「開普勒猜想」的機器驗證，都由於其推理過程無法檢驗而難以取信於人，這樣的問題將會長期存在而且越積越多。張景中這一選題因而具有特別重大的意義。科研選題在一定程度上將決定科學家的學術生涯和學術命運。文中提到做題目不要貪大求全，採取分塊解決的戰略，是十分寶貴的經驗。

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！