|
證明 是數(shù)學(xué)的精髓 在數(shù)學(xué)上，證明是指在一個特定的公理系統(tǒng)中，根據(jù)一定的規(guī)則或標(biāo)準(zhǔn)，由公理和定理推導(dǎo)出某些命題的過程。 任何數(shù)學(xué)結(jié)果都應(yīng)按照嚴格的邏輯從第一原理推導(dǎo)得出。 證明也可謂是數(shù)學(xué)的精髓，是將數(shù)學(xué)與其他智力活動區(qū)分開來的東西。 但近日，帝國理工學(xué)院的純數(shù)學(xué)教授Kevin Buzzard在劍橋舉辦的一次研討會上表示：
（他的被觀點整理在plus.maths上） Buzzard說：“事情有些失控。” 作為一名專業(yè)的數(shù)學(xué)研究人員，Buzzard在博士期間就研究與費馬大定理的證明有關(guān)的一些數(shù)學(xué)。 不過最近幾年，他開始對學(xué)術(shù)界中的數(shù)學(xué)證明標(biāo)準(zhǔn)的擔(dān)憂。 Kevin Buzzard 他認為有些證明是存在漏洞的，有些證明是有錯誤的，還有些證明在全世界只有一兩個人能理解。即使是發(fā)表在學(xué)術(shù)期刊上的東西，也不一定都正確。 想要確切地知道哪些結(jié)果是可信賴的，你得成為一個能接近那些達成了共識的專家的圈內(nèi)人。 他表示，這種擔(dān)憂或許部分源于他的數(shù)學(xué)中年危機，這讓他重新審視在自己選擇的職業(yè)生涯內(nèi)，事物是如何運作的。
Buzzard認為數(shù)學(xué)研究中的問題通常不在于有意地欺騙，而是源于一些其他的狀況。 比如說，一些數(shù)學(xué)家有時會在自己的工作中引用尚未發(fā)表的論文，因為他們非常確信這些未被發(fā)表的結(jié)果是正確的，并認定它們會很快地通過同行評審然后得以發(fā)表在學(xué)術(shù)期刊上，這種情況并不少見。 然而，有時這些未發(fā)表的結(jié)果確實永遠不會出現(xiàn)在期刊上。 那么當(dāng)越來越多的工作建立在這些未經(jīng)檢驗的結(jié)果之上時，未經(jīng)檢驗這一事實就可能被遺忘和掩蓋。 這樣的事情就曾發(fā)生在數(shù)學(xué)家James Arthur的一篇著名的專著之上，這本專著是根據(jù)他的四篇未發(fā)表的論文寫成。 雖然人們能意識到了這些證明中可能存在某些漏洞，但他們?nèi)匀灰恢抡J為它們可能大概率沒問題。 加上Authur對數(shù)學(xué)作出的諸多貢獻，還被授予了幾個重要的獎項，這更加深了人們認為Authur的結(jié)果就100%正確的印象。 除此之外，還有一個問題，那就是犯錯。 每個人都會犯錯，而有的時候，這些錯誤甚至?xí)舆^決定論文是否發(fā)表的專家評審的法眼。 因為評審們并不總是會逐行檢驗結(jié)果，他們的目標(biāo)是說服自己，論文中使用的方法足以證明主要的結(jié)果。 即使發(fā)表后發(fā)現(xiàn)明顯的錯誤，數(shù)學(xué)家都會承認錯誤。但錯誤的更正或論文的撤回都只是作為一個“更正”或者“編輯說明”出現(xiàn)在下一期的期刊上。 有多少人會讀到這些呢？專業(yè)領(lǐng)域內(nèi)的同行當(dāng)然會知道，但其他人并不會。 有些證明又長又復(fù)雜，只有全世界的少數(shù)人能理解，這或許是錯誤或漏洞最主要的來源。 一個著名的例子是所謂的有限單群分類（classification of finite simple groups），這也是二十世紀(jì)數(shù)學(xué)領(lǐng)域的一大成就。 1983年，證明這個分類正確且完備的第一版證明被發(fā)布，證明長度超過了10000頁，分布在500個期刊論文中，由100多個作者完成。 結(jié)果人們發(fā)現(xiàn)，這個證明之中存在一個問題，修正這個問題就又花了9年的時間外加一篇超過1000頁的論文。 基于第一版證明的巨大復(fù)雜性，論文的主要作者承諾會給出一個“更簡單”的第二個版證明，他們計劃分12卷出版。 然而截至2019年，只有其中7卷已問世。最終能夠完全理解整個證明的很可能只有極少數(shù)人，而那時候他們也已經(jīng)不再年輕。 雖然數(shù)學(xué)家一致認為，有限單群分類確實是完備的，并且認為只要有人愿意在大量的文獻中搜尋線索，最終就應(yīng)該能夠拼湊出完整的證明——但是多少人有這樣的時間和這樣的頭腦去這樣做呢？ Buzzard認為，這類問題嚴重破壞了純數(shù)學(xué)，以至于它陷入了危機。 如何化解這場危機呢？ 作為一門創(chuàng)造性的學(xué)科，而不是程序性的學(xué)科，數(shù)學(xué)家也是人。他們喜歡分組工作，不喜歡被細節(jié)所困擾。 因此要求他們始終堅持正當(dāng)程序就是要求他們像機器一樣工作。 但Buzzard認為，這正是解決方案所在：我們不需要讓數(shù)學(xué)家像機器一樣工作，而可以讓他們使用機器。 計算機科學(xué)家和數(shù)學(xué)家是兩個相關(guān)聯(lián)的群體，但他們有著本質(zhì)的區(qū)別：計算機科學(xué)家修復(fù)錯誤，而數(shù)學(xué)家則忽略錯誤。 一些計算機科學(xué)家經(jīng)常游走于數(shù)學(xué)家之間，他們開發(fā)出了一些定理證明軟件，例如LEAN和Isabelle。 這雖然些軟件并不能神奇般地為那些困擾了人們數(shù)個世紀(jì)的難題找到一個證明，這類問題仍需要人類數(shù)學(xué)家來解決題，但它們可以幫助我們檢驗數(shù)學(xué)家的證明是否正確。
Buzzard說，計算機科學(xué)家可能會認為，一個結(jié)果只有經(jīng)過定理證明軟件的正式檢驗才能被證明。 這意味著，對計算機科學(xué)家來說，數(shù)學(xué)領(lǐng)域的許多重大成果，包括費馬最后定理或有限簡單群的分類，仍然可以得到更仔細的檢驗。 Buzzard深知，要把數(shù)學(xué)證明轉(zhuǎn)化成軟件可以理解的代碼需要付出巨大的努力，以費馬大定理為例，它的花費估計需要1億英鎊。 盡管如此，Buzzard認為，我們至少可以培養(yǎng)初露頭角的數(shù)學(xué)家去接受這種方式。 他在帝國理工學(xué)院的本科生們就在學(xué)習(xí)如何使用定理證明軟件，他還會鼓勵學(xué)生將機器證明應(yīng)用到結(jié)果當(dāng)中。 如果數(shù)學(xué)家養(yǎng)成了這樣做的習(xí)慣，同時還有其他人開始正式檢驗?zāi)切┮延械淖C明結(jié)果，那么數(shù)學(xué)就可以被帶回到正確的軌道上。 不過也有人擔(dān)心，在數(shù)學(xué)中使用計算機是否會導(dǎo)致人們丟失對證明的真正理解。 假設(shè)計算機為我們做了工作，而且它們以一種我們?nèi)祟愝^低級的數(shù)據(jù)處理能力，且我們無法跟進的方式來證明，那么我們就不能聲稱自己理解最終的結(jié)果了。 其實Buzzard并不是在提倡使用機器學(xué)習(xí)中的那種黑箱算法。 他是想將證明轉(zhuǎn)換成計算機程序可理解的代碼，以便證明過程可以得到非?？煽康臋z驗，而不是要讓證明變得無法理解。 雖然我們當(dāng)然無法保證這些程序絕不會出錯，但它們的錯誤比人類少多了。 |
|
|
