關于作者
一個畢業(yè)于北京大學數(shù)學力學系，在中國科學院計算所、計算中心和網絡中心工作過，在澳大利亞科工組織DMS、香港浸會學院數(shù)學系和中國21世紀議程管理中心等處工作過，多次獲國家和中科院科技獎并享受政府特殊津貼的退休老頭。現(xiàn)在在【中國科普博覽】網“科學新語林”欄目里開設一個《數(shù)學與計算機》的個人專欄，愿和愛好數(shù)學與計算機的各界網友和青少年朋友，談談對數(shù)學與計算機的看法、想法。
計算機證明（1）
張建中
2013年04月08日
1. 必須經過證明的數(shù)學定理
數(shù)學含眾多分支，除數(shù)學共有的公理系統(tǒng)外，各分支還各有自己的公理、研究和發(fā)展領域，但都包括若干經過嚴格證明的定理。
在數(shù)學中，判斷一件事情的語句叫做“命題”，正確的語句叫做“真命題”，錯誤的語句叫做“假命題”。說明名詞含義，使各個名詞互不相混的語句叫做“定義”。有些真命題，它們的正確性是人們在長期的實踐過程中總結出來的，并作為判斷其他命題真假的依據(jù)，這樣的真命題稱為“公理”，也叫“公設”。有些命題，它們的正確性是用推理證實的，這樣的真命題叫做“定理”，推理的過程叫做“證明”。一般來說，在數(shù)學中，只有重要或有趣的經過證明的命題才叫定理。
如果因為其某些特例已在某種程度上證實某一語句為真，但該語句尚未被證明為真或為假，則稱該語句為猜想，而非定理。一個定理包含條件和結論兩部分，必須經過證明；證明是連接條件和結論的橋梁；證明定理是數(shù)學里一項最重要的任務與活動。
在學校學習過程中，數(shù)學一直是許多學生比較頭痛的一門課程，尤其是課本中形形色色的定理及其證明都極其抽象，千變萬化，難懂難做，令人發(fā)憷，如幾何題的證法，各具巧思，爭奇斗艷，無定法可循，只有依賴個人的經驗、技巧和靈感，這些成了許多學生選學文不選學理的一個重要原因。人們經常會問，數(shù)學定理為什么都要經過證明呢？數(shù)學定理能不能象其他學科那樣，從幾個實驗結果或者事實來宣布其正確而成為定理呢？如在物理學中，當年意大利科學家伽利略在比薩斜塔上做自由落體實驗，經過多次重復實驗，發(fā)現(xiàn)從塔頂落下的石子落地的時間總是相等，且其規(guī)律為：h = g*t2/2，其中h是塔高，g為地球重力加速度，t是時間，單位是米和秒，于是就有了自由落體的物理定律。作為實驗科學的物理等自然科學，都承認可以重復作出的結果為其科學結論。對數(shù)學定理,這樣能行嗎？
數(shù)學當然也可以重復實驗，如對偶數(shù)有6 = 3+3，8 = 3+5，10 = 5+5，12 = 5+7，14 = 7+7，16 = 5+11，18 = 7+11，……，這種把偶數(shù)拆分成兩個素數(shù)之和的實驗可以成功地做上千萬次，利用計算機不難成功進行上億次試驗；如果按物理學家們的規(guī)矩，早就可以宣布哥德巴赫猜想“任何一個大于6的偶數(shù)，都可以表示成兩個素數(shù)之和”為定理了，但數(shù)學不是物理，數(shù)學有自己這一學科的規(guī)矩，那就是一切數(shù)學定理都必須經過嚴格的證明才算數(shù)。所謂數(shù)學定理證明，就是從一組原始概念和公理出發(fā)，經過嚴格的推理證明才能給出一系列的定理，這是幾千年來數(shù)學學科所遵循的學習和研究模式。當然，數(shù)學定理證明的真正含義并不完全在于檢驗核實命題，而在于理解命題，啟迪思維，交流思想，培養(yǎng)、提高邏輯思維能力和推理能力，導致數(shù)學的新發(fā)現(xiàn)。這種模式是保護和促進數(shù)學健康成長的法規(guī)，不遵守它，數(shù)學科學就會出問題，就要遭殃！
事實上，作為嚴密科學的數(shù)學，它的定理不允許有一個反例。自然科學則不然，例如觀察了大量的鳥類都會飛之后，可以得出“鳥類會飛”的結論，不怕鴕鳥不會飛這一反例的存在，自然科學追求的往往是絕大多數(shù)情況下成立的結論。
美國數(shù)學家波利亞（George Polya，1887-1985）說：“數(shù)學家與自然科學家在研究方法上是截然不同的；觀察對自然科學家來說是可信的方法，但對數(shù)學家來說卻并非如此。選擇恰當?shù)膶嵗M行檢驗，這是生物學家肯定猜想規(guī)律的唯一方法，但是對于數(shù)學家來說，選擇恰當?shù)膶嵗M行驗證，從鼓勵信心的角度來看是有用的，但這樣還不能算是數(shù)學科學里證明了一個猜想。經驗的歸納只能說明所得結果可能可靠，但并不能證明它一定可靠?！?
2. 數(shù)學定理的證明
這里所說“數(shù)學定理證明”，就是對一個給定的命題，從一組原始概念和公理出發(fā)，經過有限步的嚴格推理，給出該命題正確性的論證，從而成為數(shù)學中的的定理。但我們不要忘記，這里所說的證明不只在不同的文化里有不同的含義，就連在不同的時代中也有不同的含義。顯然，我們不會擁有而且極可能永遠不會有一個這樣的證明標準，它獨立于時代、獨立于所要證明的東西，獨立于使用它的某個人或某個學派。
數(shù)學領域中的定理證明，一直被認為是一項需要智能才能完成的任務。證明定理時，不僅需要有根據(jù)假設進行演繹的能力，而且需要有某些特別的智慧和技巧。例如數(shù)學家在求證一個定理時，會熟練地運用他掌握的豐富專業(yè)知識，猜測應當先證明哪一個引理，精確判斷出已有的哪些定理可用，并把主問題分解為若干問題，分別獨立進行求證。
對一個數(shù)學定理給出證明，還可以幫助我們理解定理，看哪些條件的作用大、重要，哪些條件作用小、次要，是否可以把條件放寬一些；結論是不等式時，是否可以把上界變小一些，把下界放大一些，等等，進而發(fā)現(xiàn)改進和推廣該定理的思路，或發(fā)現(xiàn)原證明方法夠不夠美、過長，能否設計出更簡潔漂亮的證明等。
在數(shù)學教學中，定理證明有著極其重要的教育價值：通過證明，加深受教育者對相關數(shù)學知識的理解；通過證明，訓練和培養(yǎng)受教育者邏輯的和非邏輯的思維能力及數(shù)學交流能力；通過證明，使受教育者尋找新舊知識之間的內在聯(lián)系，使數(shù)學知識更加系統(tǒng)化；通過證明，使受教育者更牢固地掌握已學到的知識，并盡可能去發(fā)現(xiàn)新知識；通過證明，培養(yǎng)受教育者的理性精神，促進思想解放，提高與豐富受教育者的科學素質。
數(shù)學證明中的挫折和失敗往往引出有價值的數(shù)學成果。在數(shù)學史上一個極重大的事件是對歐幾里得第五公設（歐氏平行公理）的證明，到19世紀，幾乎很多大數(shù)學家都曾嘗試過，無奈大家都失敗了，引起了大家對第五公設是否是真理的考慮。鑒于上述證明的受阻，數(shù)學家們（如高斯、羅巴切夫斯基等大數(shù)學家）萌生了否定歐氏第五公設建立新幾何的念頭，終于誕生了非歐幾何。它的產生對20世紀相對論建立起了重要的作用。
由此可見，盡管對數(shù)學證明存在一些不同的認識和看法，但數(shù)學定理的嚴格證明是非常必要的，決非可有可無的。既然數(shù)學定理證明很困難、很重要，能否用機器替人進行這一工作呢？事實上，在計算機出現(xiàn)之前，就有一些很出色數(shù)學家提出了這一問題，并在20世紀后半期利用計算機取得了成功。
下面，我們給出部分學者對數(shù)學證明的一些不同看法，供參考。
美國數(shù)學家懷特（R.Wilder）說：“我們不要忘記，所謂證明不只在不同的文化有不同的含義，就連在不同的時代也有不同的含義。”“很明顯，我們不會擁有而且極可能永遠不會有一個這樣的證明標準：它獨立于時代，獨立于所要證明的東西，并且獨立于使用它的個人或某個思想學派?！?
C.Hanna說：“證明是一種透明的辯論，其中用到的論據(jù)、推理過程……都清楚地展示給讀者，任由人們公開批評，不必向權威低頭?！?
法國布爾巴基（Bourbaki）數(shù)學學派認為：“單是驗證了一個數(shù)學證明的逐步邏輯推導，而沒有試圖洞察獲得這一連串推導的背后的意念，并不算理解了那個數(shù)學證明?！?
更有甚者，英國數(shù)學家哈代(G.H.Hardy)說：“嚴格說起來根本沒有所謂數(shù)學證明……，歸根到底我們只是指出一些要點，……把證明稱之為廢話，它是為打動某些人而編造的一堆華麗辭藻，是講演時用來演示的圖片，是激發(fā)小學生想像力的工具?！?
隨著數(shù)學定理計算機證明的出現(xiàn)，對數(shù)學定理證明有了更多的不同的看法和認知。
國際數(shù)學教育委員會(ICMI)在《計算機對數(shù)學和數(shù)學教學的影響》報告中指出：“借助于計算機的證明不應該比人工證明有更多的懷疑……，我們不能認為計算機將增加錯誤證明的數(shù)目，恰恰相反，對計算機證明的批評，例如四色問題的證明，主要集中在它僅依靠蠻力和缺乏思考的洞察力。……計算機證明會給人們帶來一些新啟示，會激勵人們去尋找更好的、更短的、更富有說服力的證明，會鼓勵數(shù)學家去更準確地把握形式化的想法?！?
由于計算機的介入，新一代的數(shù)學家已經開始在計算機上實驗自己的各種思想，甚至他們宣布自己是實驗數(shù)學家，著手建立數(shù)學實驗室，創(chuàng)辦《實驗數(shù)學》雜志。同時他們對數(shù)學提出了一些新的看法：
1.對數(shù)學追求的是理解，而不是證明；
2.重視發(fā)現(xiàn)與創(chuàng)造，數(shù)學的本質在于思想的充分自由與發(fā)揮人的創(chuàng)造能力；
3.追求對解決問題的數(shù)學精神，利用數(shù)學更好地解決、處理復雜的自然現(xiàn)象。
數(shù)學含眾多分支，除數(shù)學共有的公理系統(tǒng)外，各分支還各有自己的公理、研究和發(fā)展領域，但都包括若干經過嚴格證明的定理。
在數(shù)學中，判斷一件事情的語句叫做“命題”，正確的語句叫做“真命題”，錯誤的語句叫做“假命題”。說明名詞含義，使各個名詞互不相混的語句叫做“定義”。有些真命題，它們的正確性是人們在長期的實踐過程中總結出來的，并作為判斷其他命題真假的依據(jù)，這樣的真命題稱為“公理”，也叫“公設”。有些命題，它們的正確性是用推理證實的，這樣的真命題叫做“定理”，推理的過程叫做“證明”。一般來說，在數(shù)學中，只有重要或有趣的經過證明的命題才叫定理。
如果因為其某些特例已在某種程度上證實某一語句為真，但該語句尚未被證明為真或為假，則稱該語句為猜想，而非定理。一個定理包含條件和結論兩部分，必須經過證明；證明是連接條件和結論的橋梁；證明定理是數(shù)學里一項最重要的任務與活動。
在學校學習過程中，數(shù)學一直是許多學生比較頭痛的一門課程，尤其是課本中形形色色的定理及其證明都極其抽象，千變萬化，難懂難做，令人發(fā)憷，如幾何題的證法，各具巧思，爭奇斗艷，無定法可循，只有依賴個人的經驗、技巧和靈感，這些成了許多學生選學文不選學理的一個重要原因。人們經常會問，數(shù)學定理為什么都要經過證明呢？數(shù)學定理能不能象其他學科那樣，從幾個實驗結果或者事實來宣布其正確而成為定理呢？如在物理學中，當年意大利科學家伽利略在比薩斜塔上做自由落體實驗，經過多次重復實驗，發(fā)現(xiàn)從塔頂落下的石子落地的時間總是相等，且其規(guī)律為：h = g*t2/2，其中h是塔高，g為地球重力加速度，t是時間，單位是米和秒，于是就有了自由落體的物理定律。作為實驗科學的物理等自然科學，都承認可以重復作出的結果為其科學結論。對數(shù)學定理,這樣能行嗎？
數(shù)學當然也可以重復實驗，如對偶數(shù)有6 = 3+3，8 = 3+5，10 = 5+5，12 = 5+7，14 = 7+7，16 = 5+11，18 = 7+11，……，這種把偶數(shù)拆分成兩個素數(shù)之和的實驗可以成功地做上千萬次，利用計算機不難成功進行上億次試驗；如果按物理學家們的規(guī)矩，早就可以宣布哥德巴赫猜想“任何一個大于6的偶數(shù)，都可以表示成兩個素數(shù)之和”為定理了，但數(shù)學不是物理，數(shù)學有自己這一學科的規(guī)矩，那就是一切數(shù)學定理都必須經過嚴格的證明才算數(shù)。所謂數(shù)學定理證明，就是從一組原始概念和公理出發(fā)，經過嚴格的推理證明才能給出一系列的定理，這是幾千年來數(shù)學學科所遵循的學習和研究模式。當然，數(shù)學定理證明的真正含義并不完全在于檢驗核實命題，而在于理解命題，啟迪思維，交流思想，培養(yǎng)、提高邏輯思維能力和推理能力，導致數(shù)學的新發(fā)現(xiàn)。這種模式是保護和促進數(shù)學健康成長的法規(guī)，不遵守它，數(shù)學科學就會出問題，就要遭殃！
事實上，作為嚴密科學的數(shù)學，它的定理不允許有一個反例。自然科學則不然，例如觀察了大量的鳥類都會飛之后，可以得出“鳥類會飛”的結論，不怕鴕鳥不會飛這一反例的存在，自然科學追求的往往是絕大多數(shù)情況下成立的結論。
美國數(shù)學家波利亞（George Polya，1887-1985）說：“數(shù)學家與自然科學家在研究方法上是截然不同的；觀察對自然科學家來說是可信的方法，但對數(shù)學家來說卻并非如此。選擇恰當?shù)膶嵗M行檢驗，這是生物學家肯定猜想規(guī)律的唯一方法，但是對于數(shù)學家來說，選擇恰當?shù)膶嵗M行驗證，從鼓勵信心的角度來看是有用的，但這樣還不能算是數(shù)學科學里證明了一個猜想。經驗的歸納只能說明所得結果可能可靠，但并不能證明它一定可靠?！?
2. 數(shù)學定理的證明
這里所說“數(shù)學定理證明”，就是對一個給定的命題，從一組原始概念和公理出發(fā)，經過有限步的嚴格推理，給出該命題正確性的論證，從而成為數(shù)學中的的定理。但我們不要忘記，這里所說的證明不只在不同的文化里有不同的含義，就連在不同的時代中也有不同的含義。顯然，我們不會擁有而且極可能永遠不會有一個這樣的證明標準，它獨立于時代、獨立于所要證明的東西，獨立于使用它的某個人或某個學派。
數(shù)學領域中的定理證明，一直被認為是一項需要智能才能完成的任務。證明定理時，不僅需要有根據(jù)假設進行演繹的能力，而且需要有某些特別的智慧和技巧。例如數(shù)學家在求證一個定理時，會熟練地運用他掌握的豐富專業(yè)知識，猜測應當先證明哪一個引理，精確判斷出已有的哪些定理可用，并把主問題分解為若干問題，分別獨立進行求證。
對一個數(shù)學定理給出證明，還可以幫助我們理解定理，看哪些條件的作用大、重要，哪些條件作用小、次要，是否可以把條件放寬一些；結論是不等式時，是否可以把上界變小一些，把下界放大一些，等等，進而發(fā)現(xiàn)改進和推廣該定理的思路，或發(fā)現(xiàn)原證明方法夠不夠美、過長，能否設計出更簡潔漂亮的證明等。
在數(shù)學教學中，定理證明有著極其重要的教育價值：通過證明，加深受教育者對相關數(shù)學知識的理解；通過證明，訓練和培養(yǎng)受教育者邏輯的和非邏輯的思維能力及數(shù)學交流能力；通過證明，使受教育者尋找新舊知識之間的內在聯(lián)系，使數(shù)學知識更加系統(tǒng)化；通過證明，使受教育者更牢固地掌握已學到的知識，并盡可能去發(fā)現(xiàn)新知識；通過證明，培養(yǎng)受教育者的理性精神，促進思想解放，提高與豐富受教育者的科學素質。
數(shù)學證明中的挫折和失敗往往引出有價值的數(shù)學成果。在數(shù)學史上一個極重大的事件是對歐幾里得第五公設（歐氏平行公理）的證明，到19世紀，幾乎很多大數(shù)學家都曾嘗試過，無奈大家都失敗了，引起了大家對第五公設是否是真理的考慮。鑒于上述證明的受阻，數(shù)學家們（如高斯、羅巴切夫斯基等大數(shù)學家）萌生了否定歐氏第五公設建立新幾何的念頭，終于誕生了非歐幾何。它的產生對20世紀相對論建立起了重要的作用。
由此可見，盡管對數(shù)學證明存在一些不同的認識和看法，但數(shù)學定理的嚴格證明是非常必要的，決非可有可無的。既然數(shù)學定理證明很困難、很重要，能否用機器替人進行這一工作呢？事實上，在計算機出現(xiàn)之前，就有一些很出色數(shù)學家提出了這一問題，并在20世紀后半期利用計算機取得了成功。
下面，我們給出部分學者對數(shù)學證明的一些不同看法，供參考。
美國數(shù)學家懷特（R.Wilder）說：“我們不要忘記，所謂證明不只在不同的文化有不同的含義，就連在不同的時代也有不同的含義。”“很明顯，我們不會擁有而且極可能永遠不會有一個這樣的證明標準：它獨立于時代，獨立于所要證明的東西，并且獨立于使用它的個人或某個思想學派?！?
C.Hanna說：“證明是一種透明的辯論，其中用到的論據(jù)、推理過程……都清楚地展示給讀者，任由人們公開批評，不必向權威低頭?！?
法國布爾巴基（Bourbaki）數(shù)學學派認為：“單是驗證了一個數(shù)學證明的逐步邏輯推導，而沒有試圖洞察獲得這一連串推導的背后的意念，并不算理解了那個數(shù)學證明?！?
更有甚者，英國數(shù)學家哈代(G.H.Hardy)說：“嚴格說起來根本沒有所謂數(shù)學證明……，歸根到底我們只是指出一些要點，……把證明稱之為廢話，它是為打動某些人而編造的一堆華麗辭藻，是講演時用來演示的圖片，是激發(fā)小學生想像力的工具?！?
隨著數(shù)學定理計算機證明的出現(xiàn)，對數(shù)學定理證明有了更多的不同的看法和認知。
國際數(shù)學教育委員會(ICMI)在《計算機對數(shù)學和數(shù)學教學的影響》報告中指出：“借助于計算機的證明不應該比人工證明有更多的懷疑……，我們不能認為計算機將增加錯誤證明的數(shù)目，恰恰相反，對計算機證明的批評，例如四色問題的證明，主要集中在它僅依靠蠻力和缺乏思考的洞察力。……計算機證明會給人們帶來一些新啟示，會激勵人們去尋找更好的、更短的、更富有說服力的證明，會鼓勵數(shù)學家去更準確地把握形式化的想法?！?
由于計算機的介入，新一代的數(shù)學家已經開始在計算機上實驗自己的各種思想，甚至他們宣布自己是實驗數(shù)學家，著手建立數(shù)學實驗室，創(chuàng)辦《實驗數(shù)學》雜志。同時他們對數(shù)學提出了一些新的看法：
1.對數(shù)學追求的是理解，而不是證明；
2.重視發(fā)現(xiàn)與創(chuàng)造，數(shù)學的本質在于思想的充分自由與發(fā)揮人的創(chuàng)造能力；
3.追求對解決問題的數(shù)學精神，利用數(shù)學更好地解決、處理復雜的自然現(xiàn)象。