沒有人明白的數學證明能否成立？

近來數學界有兩宗大新聞。一是曾獲數學界最高榮譽菲爾茲獎（Fields Medal）和阿貝爾獎（Abel Prize）、年屆89歲的大數學家阿蒂亞（Michael Atiyah）宣稱已解決世紀難題「黎曼猜想」（Riemann Hypothesis），並在演講中介紹自己的證明。不過數學界並不看好他的證明成立。^[1]

另一則是今年剛獲得菲爾茲獎的舒爾斯（Peter Scholze）與數學家史迪思（Jakob Stix）合撰報告，指京都大學教授望月新一2012年放上網路、以其自創數學理論證明「abc猜想」的數百頁論文中有「無法修補」的漏洞，因此猜想仍然懸而未決。^[2]

不過，數學不是一門明確的學科嗎？一切內容應該寫得清楚明白，為甚麼會有「這到底算不算證明了」的爭議？沒有人能夠明白的數學證明，還算成立嗎？

這得由「甚麼是數學證明」說起。

公理系統

傳統上，數學證明是一組論證，可以使用的前提包括理應是「不證自明」、所有人都接受的公理（axiom），以及其他已被證明的數學定理，再透過邏輯推論、數學運算，最後得出想要證明的數學命題——這時候，該命題便是正式的數學定理了。

這種「公理方法」最早可追溯自古希臘數學家歐幾里德（Euclid）的經典著作《幾何原本》（Elements），他在書中列出公理和定義，然後一步一步推導出不少定理，例如著名的畢氏定理（Pythagorean theorem）。學界普遍相信歐幾里德並非獨自發現書中定理，而是整理當時已知的數學結果。

在公元前約300年寫成的《幾何原本》長時間以來是西歐國家的重要課本，書中所用的公理方法亦被視為數學證明的典範。^[3] 中世紀的伊斯蘭數學家亦發展出重要的算術和代數技巧，使證明不再單靠幾何直覺。

但《幾何原本》的系統亦非完全無誤，除了證明中一些錯處外，歐幾里德有時暗中使用了一些假設而未有明確列出，例如柏齊公理（Pasch axiom）^[4]或連續性公理（continuity axiom）。

既然再嚴謹的人也有可能走眼，以致證明的步驟之間有漏洞——而且這還是相對簡單的歐氏幾何，現代數學要複雜得多——那麼如何能夠確保證明無誤？

形式系統

到了19世紀末，數學界開始出現一場危機。樸素集合論的一些悖論——例如著名的「羅素悖論」（Russell's Paradox）——令數學家擔心數學的基礎隱含矛盾，開始研究如何為數學奠下穩固的根基。數理邏輯及集合論在這段期間發展迅速，逐漸成為數學界的主流語言。

數學家希爾伯特（David Hilbert）提倡以純符號操作的「形式系統」（formal system）重構涉及無限的數學，再用數學方式去研究這個系統的符號變化，企圖證明不會推導出代表矛盾句（例如「0=1」）的公式，從而確保數學根基穩妥。

簡單來說，一個形式系統會規定可以用的符號，這些符號組合起來就稱為「公式」，其中能夠由系統推導出來的公式就稱作「定理」。形式系統包含變換規則，會清楚列出如何把一條定理中的符號改變，從而得出另一條定理。當然，系統亦會首先「免費」提供一些定理，符合特定條件的公式可以成為「公理」（公理也是一種定理）。

形式系統是希望把數學中「由公理出發，推導出結論」的證明方法，以一種抽象方式嚴格定義，讓數學家可以用數學方法去研究數學本身。而形式系統中的證明——簡稱為「形式證明」——就是一串順序排列的公式，每一句要麼是系統中的公理，或者由較早出現的公式應用變換規則得出來。

理想和現實

回到如何確保證明無誤的問題。如果能夠把用文字及數學公式寫成的證明「翻譯」成純粹符號組成的形式證明，那麼，檢查證明是否成立的工作，便可化約為檢查公式之間的符號改變是否合乎規則——後者理應像下棋時，檢查每一步棋有否遵守規則一樣簡單。

在形式證明之中，每一步驟之間的變化減至最小，就只是按規則增加、刪除或轉換公式中的符號，這樣就能夠避免數學家一不留神在證明中犯錯——例如用上未寫清楚的假設、推導過程有誤等。嚴格來說，只要知道形式系統的規則，不懂數學的人都可以檢查證明。

理論上，形式證明可以確保嚴謹，避免推理過程有漏洞。可是在絕大多數的數學書、期刊論文上，你不會見到形式證明，數學界所使用的證明仍然以文字及數學公式為主，原因很簡單︰純粹由符號構成的形式證明並不實用，把所有細節都寫出來會令證明又長又繁瑣，令作者或讀者均不好受。

相比之下，混合文字解說與數學公式的非形式證明，在大部分情況下能夠兼顧「嚴謹」及「易讀」兩項要求（當然是否真正易讀，也得視乎作者寫作功力和讀者知識水平）。當然，那些數學證明應該能夠「翻譯」成形式證明，不過在有人（或機械）把形式證明寫出來檢驗之前，這想法仍只是個信念——雖有大量證據支持，可是兜了一大個圈，似乎還是難以確保證明絕對嚴謹無誤。

另一個定義

現實中無法使用理想的形式證明，可見數學證明應該不只是形式證明，那麼應該如何判斷證明是否成立？

我們不妨考慮數學證明實際上扮演甚麼角色。除了上文提到傳統上「由公理出發、以邏輯推導的論證」外，亦有人把「數學證明」定義為「用來說服數學界（相關領域專家）某數學命題成立的論證」^[5]，而判斷證明是否成立的標準，就取決於能否說服到數學界。