關(guān)于作者
計(jì)算機(jī)證明（7）
張建中
2013年07月23日迄今為止，人們已經(jīng)用計(jì)算機(jī)證明了上百條數(shù)學(xué)定理，甚至還曾經(jīng)用計(jì)算機(jī)發(fā)現(xiàn)過(guò)一些猜想。這一切當(dāng)然令人驚喜和受到鼓舞，但這也只能算作是開(kāi)始，人們還不曾讓計(jì)算機(jī)做出過(guò)任何真正意義上的數(shù)學(xué)貢獻(xiàn)，幾乎所有計(jì)算機(jī)證明的都是人類已經(jīng)知道的事情，而且多數(shù)都是比較初等的結(jié)論。指望計(jì)算機(jī)幫我們?nèi)プC明歌德巴赫猜想，那一天還遠(yuǎn)遠(yuǎn)沒(méi)有到來(lái)。
就數(shù)學(xué)定理計(jì)算機(jī)證明發(fā)展的前途而言，任何人估計(jì)都可以看出來(lái)這條道路的遠(yuǎn)大前景。和人類相比，計(jì)算機(jī)不知疲倦和邏輯嚴(yán)密的優(yōu)點(diǎn)使得其前途不可限量。計(jì)算機(jī)當(dāng)然也會(huì)犯錯(cuò)誤，但是這種錯(cuò)誤歸根結(jié)底是容易檢驗(yàn)的——其正確性歸結(jié)為這些軟件內(nèi)核的正確性，而內(nèi)核一共也就幾百行、上千行代碼而已，經(jīng)反復(fù)、多次檢驗(yàn)，正確性會(huì)有足夠的保證。一代代數(shù)學(xué)家永遠(yuǎn)都要從零開(kāi)始學(xué)習(xí)、逐步成長(zhǎng)和長(zhǎng)期積累，而計(jì)算機(jī)則總是建立在已有成果的肩膀上，假以時(shí)日，計(jì)算機(jī)會(huì)不會(huì)成為有史以來(lái)最偉大的數(shù)學(xué)家呢？
國(guó)外已出現(xiàn)一些人機(jī)交互的計(jì)算機(jī)推理系統(tǒng)。借助這些系統(tǒng)，能夠用來(lái)進(jìn)行不同的數(shù)學(xué)領(lǐng)域的推理，所生成的證明和數(shù)學(xué)家的工作很類似。
對(duì)于人類面臨的很多難題，既然單個(gè)群體無(wú)法解決，那我們齊心協(xié)力一起解決不是很好么！數(shù)學(xué)家提供理論基礎(chǔ)，計(jì)算機(jī)科學(xué)家設(shè)計(jì)算法并編程實(shí)現(xiàn)，而物理學(xué)家和工程師保證計(jì)算機(jī)的穩(wěn)定性。
我們堅(jiān)信，機(jī)器證明不但不會(huì)像有些數(shù)學(xué)家擔(dān)心的那樣“使數(shù)學(xué)走向衰敗”，還將使數(shù)學(xué)家擺脫大量的繁瑣的機(jī)械計(jì)算和推理，使他們把節(jié)省下來(lái)的時(shí)間和精力用于更加富有創(chuàng)造性的工作中去。
對(duì)于數(shù)學(xué)定理計(jì)算機(jī)證明來(lái)說(shuō)，真正的挑戰(zhàn)仍然體現(xiàn)在對(duì)未知證明的尋找上。如何讓計(jì)算機(jī)學(xué)會(huì)迅速發(fā)現(xiàn)合適的證明路徑，是這一領(lǐng)域里最困難也最迷人的問(wèn)題之一。畢竟即使數(shù)學(xué)家自己往往也說(shuō)不清楚數(shù)學(xué)證明的靈感是怎樣產(chǎn)生又怎樣被自己捕捉到的，更不用說(shuō)讓計(jì)算機(jī)來(lái)模擬這一過(guò)程了。對(duì)于計(jì)算機(jī)“思考方式”的設(shè)計(jì)和研究，本身當(dāng)然就是很深刻的數(shù)學(xué)問(wèn)題。從某種意義上說(shuō)來(lái)，這一自我纏繞的局面不但沒(méi)有構(gòu)成對(duì)傳統(tǒng)意義上的數(shù)學(xué)之美的消解，反而是它的延續(xù)。歸根結(jié)底，這一領(lǐng)域的任何進(jìn)展，都標(biāo)志著人們對(duì)于“智慧思考”這一問(wèn)題更深刻的理解，這已經(jīng)足以令人驕傲了。
但我們?nèi)匀徊坏貌豢吹?，?shù)學(xué)定理計(jì)算機(jī)證明這條道路從開(kāi)始的第一天起就伴隨著巨大的爭(zhēng)議和疑慮。
人們對(duì)計(jì)算機(jī)證明的批評(píng)多半集中于它極端的繁瑣和不直觀。然而，既然人們已經(jīng)知道如何把一個(gè)傳統(tǒng)證明翻譯為計(jì)算機(jī)證明，那么把一個(gè)計(jì)算機(jī)生成的計(jì)算機(jī)證明翻譯成人們可以直接閱讀和理解的直觀證明，從理論上說(shuō)來(lái)也并非全然不可能。就這一點(diǎn)來(lái)說(shuō)，計(jì)算機(jī)證明和傳統(tǒng)證明之間的鴻溝并非是不可逾越的，盡管還有很長(zhǎng)的路要走。現(xiàn)在已經(jīng)實(shí)現(xiàn)的幾何定理可讀機(jī)器求解，所生成的解答其推理過(guò)程的簡(jiǎn)潔優(yōu)美可以與人工解答媲美。雖然解決的只是一小類數(shù)學(xué)問(wèn)題，遠(yuǎn)沒(méi)有達(dá)到解決四色定理、費(fèi)馬大定理一類難題的水平，但至少說(shuō)明了計(jì)算機(jī)證明和人工證明之間并沒(méi)有不可逾越的鴻溝，人類的創(chuàng)造力再一次得到展現(xiàn)。我們可以設(shè)想，在未來(lái)的某一天，這兩種證明之間的界面變得極其友好，于是任何一個(gè)數(shù)學(xué)家都會(huì)把計(jì)算機(jī)證明作為日常數(shù)學(xué)工具加以掌握，任何一本數(shù)學(xué)雜志都會(huì)要求提交的證明必須是經(jīng)過(guò)計(jì)算機(jī)驗(yàn)證的。
數(shù)學(xué)證明，是人類理性最光輝的成果之一，蘊(yùn)藏在深刻美麗的數(shù)學(xué)定理背后的那些那種苦心孤詣的勞動(dòng)和成功之后宛若天成的光輝，吸引了一代又一代偉大的頭腦投身于其中。如果這些定理最終都只不過(guò)是被一些代碼算出來(lái)的，這種美還有什么意義嗎？
計(jì)算機(jī)一直被認(rèn)為是數(shù)學(xué)家最引以為自豪的發(fā)明之一，然而當(dāng)它轉(zhuǎn)過(guò)頭來(lái)開(kāi)始侵蝕數(shù)學(xué)家的傳統(tǒng)領(lǐng)地“定理證明”時(shí)，數(shù)學(xué)家的首要反應(yīng)是捍衛(wèi)自己的尊嚴(yán)。一個(gè)由計(jì)算機(jī)生成的證明，從廣義上說(shuō)來(lái)，當(dāng)然也是人類智慧的產(chǎn)物，可是如果有朝一日，困擾人類數(shù)百年的某個(gè)著名猜想被計(jì)算機(jī)所證明，數(shù)學(xué)家會(huì)怎樣考慮和看待這一問(wèn)題呢？
當(dāng)然，計(jì)算機(jī)證明之路已經(jīng)打開(kāi)，你可以像很多數(shù)學(xué)家一樣投去懷疑甚至不屑一顧的目光，但是你不能無(wú)視它的存在，因?yàn)榈缆芬呀?jīng)打開(kāi)，縱然迷霧重重，但是沒(méi)有理由不繼續(xù)走下去。前途光明，奮斗仍需繼續(xù)，讓我們共同努力吧！