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