數學家一般是怎麼判斷一個定理的證明過程是否正確的?
假如將來某一天,某位數學家證明了哥德巴赫猜想,那那個證明過程肯定極其複雜,說不定會有幾千頁甚至幾萬頁的手稿,那如何對之進行審閱,即使是最頂尖的數學家,在閱讀這麼龐大的資料的時候,我也認為會出現失誤,那如何確定證明過程是正確的?現在一些現存的定理,會不會也有類似的情況發生,它們根本就不是正確的?
【為了降低剛才抖機靈吐槽式回答的罪惡感,我決定認真地回答一個問題。嗯嗯,我其實是一個很高貴冷艷嚴肅的人!┌( ′_&>` )┐】
題主的這個問題涉及的,某種意義上來說是一篇數學論文的審稿機制,因為一般而言證明出來以後都要投稿的。自然對於不同的文章而言,審稿的情況是不一樣的,因為它既取決於文章的本身質量,投稿雜誌的要求,也取決於審稿人的習慣以及對該文章的評價等等。不過大致而言可以分為三種情況:(不過無論是哪種情況,請記住一句話:審稿人就是爹!【whosyourdaddy】)
第一種,文章的結論對於審稿人而言是可信的,甚至於顯然的。這裡的「可信」意思是,當審稿人看完你的簡介(introduction),甚至於只看了摘要(abstract)或者文章的主要結論的時候,他就已經知道你的結論是對的,並且大致知道你的證明思路與技巧。這種情況下有的人會稍微認真看一下證明;有的人就看看你的引理是否印證了自己的想法,並且只讀自己有興趣的引理的證明;有的人會挑出部分引理看看,找找錯誤(畢竟要寫評審報告);有的人甚至於掃一眼就完事,或者把文章扔給學生做。總而言之,對於可信的文章,大家基本上不會花太多的時間在上面的,畢竟評審工作還是很辛苦很耗時間的。(換句不好聽的話來說就是,在他們眼中這篇文章不值得耗費他們太多時間。)同時,這樣的文章可能比較專業(specialized),所以投稿人可能可以推薦審稿人。所以這類文章審稿一般不會太仔細。
第二種,審稿人認為文章結論不是顯然的,並且文章有一定的興趣。這種情況下審稿人會有足夠的動機去讀這篇文章,甚至於對文章本身評價良好。(所以一篇文章的introduction部分很重要。)同理,這類文章也會被投往較好的雜誌。這類雜誌一般都有兩個或兩個以上的(匿名並由編輯選擇的)評審人獨立審稿並分別給出審稿意見,並且往往需要兩人都是「推薦」及其以上的評價,並且至少一人「強烈推薦」才可能給錄用(accepted)。當然對於審稿人而言,由於他們是這個方向的專家,通常也是跳過可信的引理不讀,而去讀自己覺得困難的部分。當然也有人會讀完全文每個細節。不過這種情況較少。如果審稿人發現了問題,會將問題寫在回復郵件中需要作者答覆。因此在這兩種情況中,有可能會在一些小的細節方面證明會有問題(通常是typo),不過它們往往不足以影響到文章的最終結論。
第三種,那就是文章被普遍視為非常重要的結論,並且很多人對此有興趣。一般而言,數學頂級文章的(雜誌編輯安排的官方)審稿人會有四人之多,並且往往要求全部「推薦」以上評價且三人以上「強烈推薦」才給錄用。這是很殘酷的。(據說Annals of Mathematics錄用率為3%. )不過由於審稿人較多,往往是一人為主要審稿人,而其餘人只給出大致的審稿意見和評價即可。對於主審稿人而言,他需要讀完文章並理解幾乎每個細節,以保證證明的正確性。不過往往這是非常困難的,因為這類文章通常涉及到好幾個方向的內容。所以如果文章很重要,主審稿人經常會不斷地要求作者補充必要的細節。所以一般而言這類文章的審稿周期都很長,並且一旦被錄用,就幾乎不會有什麼問題。
另外在文章預印(preprint),比如投在Arxiv上,之後會有很多非審稿人去讀文章。並且在作者投稿之前可能也會於一些同行專家討論,並請求他們閱讀文章草稿。總而言之,被雜誌錄用的文章結論通常是不會有太大問題的。當然也會有特殊的情況,不過這往往是局限於時代的原因(沒有足夠的工具之類的),比如Jordan定理的證明。還有一點,那就是一般沒人喜歡讀長的文章,並且雜誌也一般不會錄太長的文章。因此如果實在是必要,很多文章都會被分割成幾個相對獨立的部分分別審稿和發表。
最後,~( ̄▽ ̄~)(~ ̄▽ ̄)~不是所有難題的證明,都需要複雜的過程和冗繁的篇幅的。一個典型的例子就是懷爾斯的費馬大定理證明,全文只有109頁而已。但這並不代表簡單,事實上,三百年來有無數超一流的數學大腦為此殫精竭慮(包括歐拉、高斯等人在內),已經有了不少的經驗,而這些階段性的成果,在當時就得到了數學界的驗證。後人就可以通過學習,站在這些被確實驗證過的成果上,開始自己的研究。
後來的故事我們都知道了,最後證明它的工具是橢圓曲線和模形式,這兩樣東西本來不是為了證明費馬大定理而被發展出來的,但數學家發現這個領域內的谷山-志村猜想(現已被證明,叫谷山-志村定理了)蘊含了費馬大定理。而懷爾斯發現只需證明此猜想的一個特殊情況成立就可以證明費馬大定理,所以他的證明實際上是從這裡開始工作的,並不需要多少篇幅。
打個比方,如果把數學比作自然界,數學家比作人類,那數學難題就好似珠峰這種人力難及的地界。而對於這種地方,打算征服它們的數學家未必非要從山腳開始往上一步步爬到山頂,也有可能是利用別人為了別的用途所造出來的工具(比如直升機之類),從半路甚至更高的地方切入,達到登頂的目的。而當他們寫自己的攻略(證明)時,只會寫如何利用該工具達到了目的,而不會連工具的製造過程都寫進去的。同樣的,「直升機」製造過程中的原理、工序、實驗等等,都是早已被逐步地驗證過了,這部分的驗證不算在審核難題證明的過程內。
如果歌德巴赫猜想被證明,頂多只有幾百頁。
如果把證明比作尋寶,那麼證明的篇幅就如同一次出征的路程。不可能馬不停蹄一路狂奔就找到,路上一定會有補給站,有休息的地方,有規劃總結。就算寶貝的位置確定了,路程也一定會做合理分段。
數學證明也是這樣。一個猜想的提出,就是尋寶的號令。有時候寶貝在家門口立即就找到了,有時候就要長途跋涉,比如歌德巴赫猜想。這時就是團隊合作了。
其實很少有人理睬號令,大多數人只是到處轉悠。有任何發現,就會和大家互通有無。對寶藏感興趣的,則利用這些前人的成果,選自認為靠譜的方向探索。
有時候數學家們會湊到一起,對某些寶貝規劃路線圖,先找什麼再找什麼,一點點逼近目標。於是就有人沿這種路線攻堅,如果有任何發現,也會通知其他人。
因此,猜想最後的證明,頂多就是珠峰登頂的最後一天。證明者的起點,是無數數學家共同建立起來的營地。但這最後的路程,他仍需要規劃,分出許多小定理。
現在說審閱。上面那位登頂成功,就需要有人沿著他繪製的詳細路線重走一遍,確定不是吹的。路線原本不長,但為節省體力,審閱者也會組隊分段完成驗證。
路程短,所以一般來說大方向不會錯。審閱如果發現路上有陷阱或漏洞,就通知大家一起修補。還有另一任務,就是為之後接踵而來的遊客掃清障礙,把路線簡化。
Abstruse Goose 230
作為一個和數學研究不沾邊,但讀書的時候天天要和數學系的人打交道的人,簡單回答一下現代數學論文大概是怎麼被驗證正確性的。
一篇重大的論文出來,一般沒人看得懂。和這有關的某些大學數學系小team,就會組織3,5個人,開始看論文。一般都是大家事先講好範圍,一般也就10到20頁的樣子吧,回去各自看,一周以後回來討論。某人會說我看懂了,然後給大家講解一下然後再講好下周的範圍,大家回去繼續看。大家都看不懂,就討論一下,然後回去繼續看。由於偉大的牛人們太厲害,看懂別人的論文很費功夫,所以看論文也是個苦差事。
重大證明比如4色原理那個,一般都是等某個小組宣稱自己看完了,證明沒問題,然後大家就都承認了。
過於變態的比如abc猜想,大家都看不懂,又不願意把太多時間放在看別人論文上,就只能存疑了。某義大利哥們曾經給學校請了一年假,真被看完證明。結果1個月就回來了,因為他估計了一下,最後看完大概要10年,呵呵。
另外,一般的數學論文也就幾十到幾百頁,再長真的會死人的啊。
有限單群的分類定理被證明後,我想很少有人能以一己之力來完全了解它的內容,畢竟這個定理的範圍超過10000頁~~~~~~~~~~~
這個定理的正確是數百位數學家最後得到的,對於一般的研究工作,只需知道這個分類是完全清楚的就好了,不需要對所有情況進行驗證了。
現在的數學證明往往是由無數的定義(Definition),引理(Lemma),推論(Corollary),定理(Theorem)組成,結構會相當清楚。而這些東西大多是來源於已有的成果或者成果的推廣,所以一般來說只要不是像有限單群分類那樣的,主體的證明都並不是很長。
但是即使是那種很簡短的成果也需要經過同行們的較長時間審閱。那是因為審閱的困難並不在於論文的長短,而是有時候會需要讀的相關的理論或者新成果較多,另外作者通常在有些技術處理上並不是很仔細,在閱讀的時候需要慢慢補充完善。
因此為了方便同行檢查證明的結果,數學工作者們在有了重大突破時,在發表文章的前後,會以講座或者討論班的形式展示自己的成果。這個過程可能會經歷比較久的時間。
而說現有理論的結果會不會有錯誤,這確實是可能會有的。畢竟有些結果雖然出現了很久,但是由於它過於龐大或者驗證起來過於麻煩所以並沒有徹底完成也是有可能的。這裡不得說一下上面提到的有限單群分類的問題。這個問題從開始到總體完成經歷了一百多年的時間,最終論文有上萬頁(這也是數學界最出名的長篇證明了),它的證明內容目前仍然存在疑問,因為它不像普通的證明一樣僅僅是回答一個是與非的問題,而是將所有有限單群做了分類,因此極有可能在對某一有限單群的分類過程出現錯誤。
總結來說,現在一個偉大的數學結果的出現往往需要很多前人理論的鋪墊,而最終完成這個結果人可能僅僅是靈光一現將很多已有結果綜合起來,這樣一個過程往往需要極強的洞察力和對理論深刻的理解才行,解決問題的困難之處就在於此。結果出現錯誤的可能性雖然有但是在那種已經應用很久的定理上並不容易出現。
有本書《費馬大定理》,裡面詳細的闡述了懷爾斯證明費馬大定理的過程,最後兩章涉及到審閱的內容,一下內容選自該書:
懷爾斯將它的手稿投交到《數學發明》(inventions mathematicae),由它的編輯挑選審稿人,通常是指定2到3個審稿人,但因為該證明的重要性選擇了6個審稿人。證明共200頁,被分成六章,每人負責一章。
實際上懷爾斯最初的證明確實被發現了重大缺陷,後來他用了一年的時間改進方法,最終成功。
現在計算機有Coq跟Agda之類的互動定理證明器可以幫忙驗證
https://coq.inria.fr/
雖然不少定理的證明過程達數百頁, 但其中用到的公設跟推理規則, 都大概只有幾頁就可以描述完, 只需要確認Coq程序本身的推理規則沒錯, 公設沒錯, 其餘過程都可以交由電腦驗證
若是有一大類結構相似的引理, 甚至也可以寫程序自動產生其過程
圖論中的四色定理, 其證明過程長到至今沒有任何活人審核過, 都是計算機驗證的
參閱 A computer-checked proof of the Four Colour Theorem 這篇就是用 Coq 證明的不需要有人通讀稿件,只需要分解成若干個部分(事實上,本來就不太可能有人在不參考任何前人資料的情況下一次性寫一部千頁巨著去證明一個定理,科研通常就是很多人你做一點我做一點步步推進的),每個部分的專家驗證其嚴格性即可。
當然,不能排除出錯的可能。龐加萊猜想中出現一次烏龍,中國數學家完成「臨門一腳」,結果佩雷爾曼和其他數學家證明佩雷爾曼給出的是基本完整證明,現在這兩名中國數學家基本上在數學界已經是沒戲了,現代數學主要是關鍵障礙的解決才是一個數學的基本特徵
實際上一個大的數字證明,內部會包含很多定理,推理等。只需要對他們進行分別證明,然後在此基礎上再推導出新的定理,最後證明出最終結果即可。
別人來驗證的時候也只需要一個個小定理的驗證就行了,因此也就可以多人合作來驗證正確性了。
寫代碼的時候不也是提倡模塊化么,一個道理。
比如下面陳景潤的證明原文(節選且不保證順序)以上說的都對,不過
有時候你真的沒辦法判斷證明過程是對是錯
因為,你沒有能力看懂論文呀,
不信?
證明ABC猜想:意義重大,卻無人能識?
http://zh.wikipedia.org/wiki/Abc%E7%8C%9C%E6%83%B3
對的,現代數學已經發展到不僅僅寫論文的人要熬干心血,讀論文的人也要絞盡腦汁,往往是某天學界突然發表了一個新成果,幾個教授馬上帶著十幾個博士二十幾個研究生開始讀,每個禮拜讀兩三頁,再開個會討論下。幾百頁的證明,很有可能讀完就要一年左右。
然後你告訴他們這證明有錯?
我@¥$《%#{|~$@,你以為數學家平時都很閑是嗎?!
發了有錯論文的數學家如果被人發現,結局就只有一個:
身!敗!名!裂!
日本的一位天才數學家(好像是望月新一?),由於寫的論文又長又讓人看不懂,已經被學界集體無視,他發的東西,大家全都裝做看不見。
唉,其實這樣挺寂寞的。推薦閱讀:
※月球繞著地球轉,地球繞著太陽轉,太陽也繞著銀河系中心轉,這樣的運動循環下去是什麼樣的?
※如果有外星人,他們也會用十進位嗎?
※如何簡明地給文科生解釋曲率(curvature)?
※如何理解《生活大爆炸》第八季第二集里 Howard 和 Sheldon 鬥智里的各種知識點?
※極坐標表示 5000 到 50000 之間的素數為什麼會形成一條斐波那契螺旋線?