證明

是數(shù)學的精髓

在數(shù)學上，證明是指在一個特定的公理系統(tǒng)中，根據(jù)一定的規(guī)則或標準，由公理和定理推導出某些命題的過程。

任何數(shù)學結果都應按照嚴格的邏輯從第一原理推導得出。

證明也可謂是數(shù)學的精髓，是將數(shù)學與其他智力活動區(qū)分開來的東西。

但近日，帝國理工學院的純數(shù)學教授Kevin Buzzard在劍橋舉辦的一次研討會上表示：

證明是一種很高的標準。它被兢兢業(yè)業(yè)地應用到了本科的數(shù)學課程中，卻沒有應用到更高層次的數(shù)學研究中。

（他的被觀點整理在plus.maths上）

    Buzzard說：“事情有些失控。”    

作為一名專業(yè)的數(shù)學研究人員，Buzzard在博士期間就研究與費馬大定理的證明有關的一些數(shù)學。

不過最近幾年，他開始對學術界中的數(shù)學證明標準的擔憂。

Kevin Buzzard

他認為有些證明是存在漏洞的，有些證明是有錯誤的，還有些證明在全世界只有一兩個人能理解。即使是發(fā)表在學術期刊上的東西，也不一定都正確。

想要確切地知道哪些結果是可信賴的，你得成為一個能接近那些達成了共識的專家的圈內(nèi)人。

他表示，這種擔憂或許部分源于他的數(shù)學中年危機，這讓他重新審視在自己選擇的職業(yè)生涯內(nèi)，事物是如何運作的。

    問題是什么    

Buzzard認為數(shù)學研究中的問題通常不在于有意地欺騙，而是源于一些其他的狀況。

比如說，一些數(shù)學家有時會在自己的工作中引用尚未發(fā)表的論文，因為他們非常確信這些未被發(fā)表的結果是正確的，并認定它們會很快地通過同行評審然后得以發(fā)表在學術期刊上，這種情況并不少見。

然而，有時這些未發(fā)表的結果確實永遠不會出現(xiàn)在期刊上。

那么當越來越多的工作建立在這些未經(jīng)檢驗的結果之上時，未經(jīng)檢驗這一事實就可能被遺忘和掩蓋。

這樣的事情就曾發(fā)生在數(shù)學家James Arthur的一篇著名的專著之上，這本專著是根據(jù)他的四篇未發(fā)表的論文寫成。

雖然人們能意識到了這些證明中可能存在某些漏洞，但他們?nèi)匀灰恢抡J為它們可能大概率沒問題。

加上Authur對數(shù)學作出的諸多貢獻，還被授予了幾個重要的獎項，這更加深了人們認為Authur的結果就100%正確的印象。

除此之外，還有一個問題，那就是犯錯。

每個人都會犯錯，而有的時候，這些錯誤甚至會逃過決定論文是否發(fā)表的專家評審的法眼。

因為評審們并不總是會逐行檢驗結果，他們的目標是說服自己，論文中使用的方法足以證明主要的結果。

即使發(fā)表后發(fā)現(xiàn)明顯的錯誤，數(shù)學家都會承認錯誤。但錯誤的更正或論文的撤回都只是作為一個“更正”或者“編輯說明”出現(xiàn)在下一期的期刊上。

有多少人會讀到這些呢？專業(yè)領域內(nèi)的同行當然會知道，但其他人并不會。

有些證明又長又復雜，只有全世界的少數(shù)人能理解，這或許是錯誤或漏洞最主要的來源。

一個著名的例子是所謂的有限單群分類（classification of finite simple groups），這也是二十世紀數(shù)學領域的一大成就。

1983年，證明這個分類正確且完備的第一版證明被發(fā)布，證明長度超過了10000頁，分布在500個期刊論文中，由100多個作者完成。

結果人們發(fā)現(xiàn)，這個證明之中存在一個問題，修正這個問題就又花了9年的時間外加一篇超過1000頁的論文。

基于第一版證明的巨大復雜性，論文的主要作者承諾會給出一個“更簡單”的第二個版證明，他們計劃分12卷出版。

然而截至2019年，只有其中7卷已問世。最終能夠完全理解整個證明的很可能只有極少數(shù)人，而那時候他們也已經(jīng)不再年輕。

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

Buzzard認為，這類問題嚴重破壞了純數(shù)學，以至于它陷入了危機。

   如何化解這場危機呢？    

作為一門創(chuàng)造性的學科，而不是程序性的學科，數(shù)學家也是人。他們喜歡分組工作，不喜歡被細節(jié)所困擾。

因此要求他們始終堅持正當程序就是要求他們像機器一樣工作。

但Buzzard認為，這正是解決方案所在：我們不需要讓數(shù)學家像機器一樣工作，而可以讓他們使用機器。

計算機科學家和數(shù)學家是兩個相關聯(lián)的群體，但他們有著本質的區(qū)別：計算機科學家修復錯誤，而數(shù)學家則忽略錯誤。

一些計算機科學家經(jīng)常游走于數(shù)學家之間，他們開發(fā)出了一些定理證明軟件，例如LEAN和Isabelle。

這雖然些軟件并不能神奇般地為那些困擾了人們數(shù)個世紀的難題找到一個證明，這類問題仍需要人類數(shù)學家來解決題，但它們可以幫助我們檢驗數(shù)學家的證明是否正確。

當給出一個用代碼表達的證明，軟件會根據(jù)之前的結果和數(shù)學公理檢驗所有的邏輯步驟是否正確。

如果出現(xiàn)錯誤，機器就會發(fā)出信號告訴我們；如果之前在證明中留有漏洞，機器也不會放任我們忘記。

Buzzard說，計算機科學家可能會認為，一個結果只有經(jīng)過定理證明軟件的正式檢驗才能被證明。

這意味著，對計算機科學家來說，數(shù)學領域的許多重大成果，包括費馬最后定理或有限簡單群的分類，仍然可以得到更仔細的檢驗。

Buzzard深知，要把數(shù)學證明轉化成軟件可以理解的代碼需要付出巨大的努力，以費馬大定理為例，它的花費估計需要1億英鎊。

盡管如此，Buzzard認為，我們至少可以培養(yǎng)初露頭角的數(shù)學家去接受這種方式。

他在帝國理工學院的本科生們就在學習如何使用定理證明軟件，他還會鼓勵學生將機器證明應用到結果當中。

如果數(shù)學家養(yǎng)成了這樣做的習慣，同時還有其他人開始正式檢驗那些已有的證明結果，那么數(shù)學就可以被帶回到正確的軌道上。

不過也有人擔心，在數(shù)學中使用計算機是否會導致人們丟失對證明的真正理解。

假設計算機為我們做了工作，而且它們以一種我們?nèi)祟愝^低級的數(shù)據(jù)處理能力，且我們無法跟進的方式來證明，那么我們就不能聲稱自己理解最終的結果了。

其實Buzzard并不是在提倡使用機器學習中的那種黑箱算法。

他是想將證明轉換成計算機程序可理解的代碼，以便證明過程可以得到非?？煽康臋z驗，而不是要讓證明變得無法理解。

雖然我們當然無法保證這些程序絕不會出錯，但它們的錯誤比人類少多了。