純數學陷入了危機？

證明是數學的精髓。任何數學結果都應按照嚴格的邏輯從第一原理推導得出。證明是將數學與其他智力活動區分開來的東西，他也是數學之所以優美並純粹的原因。

最近，帝國理工學院的純數學教授Kevin Buzzard在劍橋舉辦的一次研討會上表示，證明是一種很高的標準，它被矜矜業業地應用到了本科的數學課程中，卻沒有應用到更高層次的數學研究中。

有些證明是存在漏洞的，有些證明是有錯誤的，還有些證明在全世界只有一兩個人能理解。即使是發表在學術期刊上的東西，也不一定都正確。想要確切地知道哪些結果是可信賴的，你得成為一個能接近那些達成了共識的專家的圈內人。Buzzard說：「事情有些失控。」

Buzzard自己就是這樣一位專家，從1998年以來，他就是一名專業的數學研究人員。在博士期間，他研究與費馬大定理的證明有關的一些數學。不過最近幾年，對學術界中的數學證明標準的擔憂，悄然襲上了他的心頭。他說，這種擔憂或許部分源於他的數學中年危機，這讓他重新審視在自己選擇的職業生涯內，事物是如何運作的。

問題是什麼？

數學研究中的問題通常不在於有意地欺騙，而是源於一些其他的狀況。比如說，一些數學家有時會在自己的工作中引用尚未發表的論文，因為他們非常確信這些未被發表的結果是正確的，並認定它們會很快地通過同行評審然後得以發表在學術期刊上，這種情況並不少見。然而，有時這些未發表的結果確實永遠不會出現在期刊上。那麼當越來越多的工作建立在這些未經檢驗的結果之上時，未經檢驗這一事實就可能被遺忘和掩蓋。

這樣的事情就曾發生在數學家James Arthur的一篇著名的專著之上，它依賴於他的四篇還未經發表的論文。人們能意識到了這些證明中可能存在某些漏洞，卻又會一致認為它們可能大概率沒問題。最近，由於對數學作出的諸多貢獻，Authur被授予了幾個重要的獎項，雖然這些獎項實至名歸，卻也加深了人們認為Authur的結果就100%正確的印象。

另一個問題是錯誤。每個人都會犯錯，而有的時候，這些錯誤甚至會逃過決定論文是否發表的專家評審的法眼。因為評審們並不總是會逐行檢驗結果，他們的目標是說服自己，論文中使用的方法足以證明主要的結果。

如果在論文發表後發現了明顯的錯誤，沒有哪個自重的數學家會拒絕承認自己的錯誤。但錯誤的更正或論文的撤回都只是作為一個「更正」或者「編輯說明」出現在下一期的期刊上。有多少人會讀到這些呢？專業領域內的同行當然會知道，但其他人並不會。

有些證明又長又複雜，只有全世界的少數人能理解，這或許是錯誤或漏洞最主要的來源。一個著名的例子是所謂的有限單群分類，也就是對無限多個數學對象中的每一個進行分類，這是二十世紀數學領域的一大成就。證明這個分類正確且完備的第一版證明發佈於1983年，證明長度超過了10000頁，分布在500個期刊論文中，由100多個作者完成。結果人們發現，這個證明之中存在一個問題，修正這個問題就又花了9年的時間外加一篇超過1000頁的論文。

基於第一版證明的巨大複雜性，論文的主要作者承諾會給出一個「更簡單」的第二個版證明，他們計劃分12卷出版。然而截至2019年，只有其中7卷已問世。最終能夠完全理解整個證明的很可能只有極少數人，而那時候他們也已經不再年輕。

雖然數學家一致認為，有限單群分類確實是完備的，並且認為只要有人願意在大量的文獻中搜尋線索，最終就應該能夠拼湊出完整的證明——但是多少人有這樣的時間和這樣的頭腦去這樣做呢？

解決方案是什麼？

Buzzard認為，這類問題已經嚴重破壞了純數學，甚至讓純數學陷入危機。但要如何才能化解這場危機？數學是一門創造性的學科，而不是程序性的；而且數學家是人，他們喜歡分組工作，而不希望深陷在細節的泥潭裡。因此，要求他們始終堅持預設的程序就是要求他們像機器一樣工作。

但是Buzzard認為，這正是問題的癥結所在：我們不需要數學家像機器一樣工作，而是可以要他們去使用機器。計算機科學家和數學家是兩個相關聯的群體，但他們有著本質的區別：計算機科學家修復錯誤，而數學家則忽略錯誤。

一些計算機科學家經常遊走於數學家之間，他們開發出了一些定理證明軟體，例如LEAN和Isabelle。這些軟體並不能神奇般地為那些困擾了人們數個世紀的難題找到一個證明，這類問題仍需要人類數學家來解決題，但它們可以幫助我們檢驗數學家的證明是否正確。

如果給出一個用代碼表達的證明，軟體會根據之前的結果和數學公理檢驗所有的邏輯步驟是否正確。如果出現錯誤，機器就會發出信號告訴我們；如果之前在證明中留有漏洞，機器也不會放任我們忘記。

Buzzard說，計算機科學家可能因此會認為，一個結果只有經過了定理證明軟體的正式檢驗之後，才能算是被證明了。這就意味著，對計算機科學家來說，數學領域的許多重大成果，包括費馬大定理或有限單群分類，仍然可以被檢驗得更加仔細。

Buzzard深知，要把數學證明轉化成軟體可以理解的代碼需要付出巨大的努力，以費馬大定理為例，它的花費估計需要1億英鎊。儘管如此，但Buzzard認為，我們至少可以培養初露頭角的數學家去接受這種方式。他在帝國理工學院的本科生們就在學習如何使用定理證明軟體，他還會鼓勵學生將機器證明應用到結果當中。如果數學家養成了這樣做的習慣，同時還有其他人開始正式檢驗那些已有的證明結果，那麼數學就可以被帶回到正確的軌道上。

不過有些人擔憂，在數學證明中使用計算機會導致人們喪失對證明的真正理解：如果計算機做了我們的工作，如果它們以一種我們人類較低級的數據處理能力無法跟進的方式來證明，那麼我們就不能聲稱自己理解最終的結果了。

但Buzzard並不是在提倡使用機器學習中的那種黑箱演算法。他是想將證明轉換成計算機程序可理解的代碼，以便證明過程可以得到非常可靠的檢驗，而不是要讓證明變得無法理解。我們當然無法保證這些程序絕不會出錯，但它們的錯誤比人類少多了。

在Buzzard看來，這麼做不會讓數學失去任何東西，只會獲得。

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