證明

是數(shù)學(xué)的精髓

在數(shù)學(xué)上,，證明是指在一個(gè)特定的公理系統(tǒng)中,，根據(jù)一定的規(guī)則或標(biāo)準(zhǔn)，由公理和定理推導(dǎo)出某些命題的過(guò)程,。

任何數(shù)學(xué)結(jié)果都應(yīng)按照嚴(yán)格的邏輯從第一原理推導(dǎo)得出,。

證明也可謂是數(shù)學(xué)的精髓，是將數(shù)學(xué)與其他智力活動(dòng)區(qū)分開(kāi)來(lái)的東西,。

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

證明是一種很高的標(biāo)準(zhǔn)。它被兢兢業(yè)業(yè)地應(yīng)用到了本科的數(shù)學(xué)課程中,，卻沒(méi)有應(yīng)用到更高層次的數(shù)學(xué)研究中,。

（他的被觀點(diǎn)整理在plus.maths上）

    Buzzard說(shuō)：“事情有些失控。”    

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

不過(guò)最近幾年，他開(kāi)始對(duì)學(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)作的,。

    問(wèn)題是什么    

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

比如說(shuō),，一些數(shù)學(xué)家有時(shí)會(huì)在自己的工作中引用尚未發(fā)表的論文，因?yàn)樗麄兎浅４_信這些未被發(fā)表的結(jié)果是正確的,，并認(rèn)定它們會(huì)很快地通過(guò)同行評(píng)審然后得以發(fā)表在學(xué)術(shù)期刊上，這種情況并不少見(jiàn),。

然而,，有時(shí)這些未發(fā)表的結(jié)果確實(shí)永遠(yuǎn)不會(huì)出現(xiàn)在期刊上。

那么當(dāng)越來(lái)越多的工作建立在這些未經(jīng)檢驗(yàn)的結(jié)果之上時(shí),，未經(jīng)檢驗(yàn)這一事實(shí)就可能被遺忘和掩蓋,。

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

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

加上Authur對(duì)數(shù)學(xué)作出的諸多貢獻(xiàn),，還被授予了幾個(gè)重要的獎(jiǎng)項(xiàng),，這更加深了人們認(rèn)為Authur的結(jié)果就100%正確的印象。

除此之外,，還有一個(gè)問(wèn)題,，那就是犯錯(cuò)。

每個(gè)人都會(huì)犯錯(cuò),，而有的時(shí)候,，這些錯(cuò)誤甚至?xí)舆^(guò)決定論文是否發(fā)表的專家評(píng)審的法眼。

因?yàn)樵u(píng)審們并不總是會(huì)逐行檢驗(yàn)結(jié)果,，他們的目標(biāo)是說(shuō)服自己,，論文中使用的方法足以證明主要的結(jié)果。

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

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

有些證明又長(zhǎng)又復(fù)雜，只有全世界的少數(shù)人能理解,，這或許是錯(cuò)誤或漏洞最主要的來(lái)源,。

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

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

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

基于第一版證明的巨大復(fù)雜性,，論文的主要作者承諾會(huì)給出一個(gè)“更簡(jiǎn)單”的第二個(gè)版證明,，他們計(jì)劃分12卷出版。

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

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

Buzzard認(rèn)為，這類問(wèn)題嚴(yán)重破壞了純數(shù)學(xué),，以至于它陷入了危機(jī),。

   如何化解這場(chǎng)危機(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é)家之間，他們開(kāi)發(fā)出了一些定理證明軟件,，例如LEAN和Isabelle,。

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

當(dāng)給出一個(gè)用代碼表達(dá)的證明，軟件會(huì)根據(jù)之前的結(jié)果和數(shù)學(xué)公理檢驗(yàn)所有的邏輯步驟是否正確,。

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

Buzzard說(shuō)，計(jì)算機(jī)科學(xué)家可能會(huì)認(rèn)為,，一個(gè)結(jié)果只有經(jīng)過(guò)定理證明軟件的正式檢驗(yàn)才能被證明,。

這意味著，對(duì)計(jì)算機(jī)科學(xué)家來(lái)說(shuō),，數(shù)學(xué)領(lǐng)域的許多重大成果，包括費(fèi)馬最后定理或有限簡(jiǎn)單群的分類,，仍然可以得到更仔細(xì)的檢驗(yàn),。

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

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

他在帝國(guó)理工學(xué)院的本科生們就在學(xué)習(xí)如何使用定理證明軟件,，他還會(huì)鼓勵(lì)學(xué)生將機(jī)器證明應(yīng)用到結(jié)果當(dāng)中,。

如果數(shù)學(xué)家養(yǎng)成了這樣做的習(xí)慣，同時(shí)還有其他人開(kāi)始正式檢驗(yàn)?zāi)切┮延械淖C明結(jié)果,，那么數(shù)學(xué)就可以被帶回到正確的軌道上,。

不過(guò)也有人擔(dān)心，在數(shù)學(xué)中使用計(jì)算機(jī)是否會(huì)導(dǎo)致人們丟失對(duì)證明的真正理解,。

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

其實(shí)Buzzard并不是在提倡使用機(jī)器學(xué)習(xí)中的那種黑箱算法,。

他是想將證明轉(zhuǎn)換成計(jì)算機(jī)程序可理解的代碼，以便證明過(guò)程可以得到非?？煽康臋z驗(yàn),，而不是要讓證明變得無(wú)法理解。

雖然我們當(dāng)然無(wú)法保證這些程序絕不會(huì)出錯(cuò),，但它們的錯(cuò)誤比人類少多了,。