數(shù)學(xué)思想方法的重大突破分析

　　一、機(jī)器證明的必要性和可能性

　　定理機(jī)器證明的出現(xiàn)不是偶然的，而是有其客觀必然性，它既是電子計(jì)算機(jī)和人工智能發(fā)展的產(chǎn)物，也是數(shù)學(xué)自身發(fā)展的需要。

　　首先，現(xiàn)代數(shù)學(xué)的發(fā)展迫切需要把數(shù)學(xué)家從繁難的邏輯推演中解放出來(lái)。我們知道，任何數(shù)學(xué)命題的確立都需要嚴(yán)格的邏輯證明，而數(shù)學(xué)命題的證明是一種極其復(fù)雜而又富有創(chuàng)造性的思維活動(dòng)，它不僅需要根據(jù)已有知識(shí)和給定條件進(jìn)行邏輯推理的能力，而且常常需要相當(dāng)高的技巧、靈感和洞察力。有時(shí)為尋找一個(gè)定理的證明，還需要開(kāi)拓一種全新的思路，而這種思路的形成竟要數(shù)學(xué)家們付出幾十年、幾百年乃至上千年的艱苦努力。如果把定理的證明交給計(jì)算機(jī)去完成，那就可以使數(shù)學(xué)家從冗長(zhǎng)繁難的邏輯推演中解放出來(lái)，從而可以把精力和聰明才智更多地用于富有開(kāi)創(chuàng)性的工作，諸如建立新的數(shù)學(xué)概念，提出新的數(shù)學(xué)猜想，構(gòu)造新的數(shù)學(xué)命題，創(chuàng)造新的數(shù)學(xué)方法，開(kāi)辟新的數(shù)學(xué)領(lǐng)域等等，由此提高數(shù)學(xué)創(chuàng)造的效率。

　　其次，機(jī)器證明的必要性，還表現(xiàn)在數(shù)學(xué)中存在著大量傳統(tǒng)的單純?nèi)四X支配手工操作的研究方法難以奏效的證明問(wèn)題。這些問(wèn)題往往因?yàn)樽C明步驟過(guò)于冗長(zhǎng)，工作量十分巨大，使數(shù)學(xué)家在有生之年無(wú)法完成。電子計(jì)算機(jī)具有信息儲(chǔ)存量大，信息加工及變換的速度快等優(yōu)越性，這就突破了人腦生理機(jī)制的局限性與時(shí)空障礙。也就是說(shuō)，如果借助電子計(jì)算機(jī)的優(yōu)勢(shì)就有可能使某些復(fù)雜繁難的證明問(wèn)題得以解決。“四色猜想”的證明就是一個(gè)令人信服的范例。“四色猜想”提出于19世紀(jì)中葉，它的內(nèi)容簡(jiǎn)單說(shuō)來(lái)就是：對(duì)于平面或球面的任何地圖，用四種顏色，就可使相鄰的國(guó)家或地區(qū)區(qū)分開(kāi)。沿著傳統(tǒng)的手工式證明的道路，數(shù)學(xué)家們做了各種嘗試，結(jié)果都未能奏效。直到1976年，由于借助于電子計(jì)算機(jī)才解決了這道百年難題。為證明它，高速電子計(jì)算機(jī)花費(fèi)了120個(gè)機(jī)器小時(shí)，完成了300多億個(gè)邏輯判斷。如果這項(xiàng)工作由一個(gè)人用手工去完成，大約需要30萬(wàn)年。

　　第三，機(jī)器證明的可能性，從認(rèn)識(shí)論上看，是由創(chuàng)造性工作和非創(chuàng)造性工作之間的關(guān)系決定的。我們知道，在定理的證明過(guò)程中，既有創(chuàng)造性思維活動(dòng)，又有非創(chuàng)造性思維活動(dòng)，而思維活動(dòng)中的創(chuàng)造性工作和非創(chuàng)造性工作并不是完全割裂的，而是互為前提、相互制約、相互轉(zhuǎn)化的，非創(chuàng)造性工作是創(chuàng)造性工作的基礎(chǔ)，創(chuàng)造性工作又可以通過(guò)某種途徑部分地轉(zhuǎn)化為非創(chuàng)造性工作。當(dāng)我們通過(guò)算法程序把定理證明中的創(chuàng)造性工作轉(zhuǎn)化為非創(chuàng)造性工作之后，也就有可能把定理的證明交給計(jì)算機(jī)去完成。

　　第四，理論上的研究已經(jīng)表明，的確有不少類(lèi)型的定理證明可以機(jī)械化，可以放心地讓計(jì)算機(jī)去完成。希爾伯特和塔爾斯基的機(jī)械化定理，就是對(duì)定理證明機(jī)械化可能性的一種理論探討。吳文俊教授對(duì)幾何定理證明機(jī)械化的可能性曾作過(guò)深入的研究。他將可施行機(jī)械化證明的實(shí)現(xiàn)劃分為三種不同的類(lèi)型，并給出了實(shí)現(xiàn)機(jī)器證明的一個(gè)行之有效的一般方法。這個(gè)一般化方法的基本思想是：首先借助坐標(biāo)系，把定理的假設(shè)與求證部分用一些代數(shù)關(guān)系式來(lái)表示，然后再把表示代數(shù)關(guān)系的多項(xiàng)式做適當(dāng)處理，即把終結(jié)多項(xiàng)式中的坐標(biāo)逐個(gè)消去，當(dāng)消去的結(jié)果為零時(shí)，定理也就得證。

　　目前，機(jī)器證明作為數(shù)學(xué)研究的一種方法，還存在著許多理論和技術(shù)上的問(wèn)題，這些問(wèn)題的解決將有待于算法理論、計(jì)算機(jī)科學(xué)和人工智能等各個(gè)領(lǐng)域出現(xiàn)新的重大突破。

　　二、機(jī)器證明的興起和進(jìn)展

　　機(jī)器證明的思想淵源可追溯到幾何代數(shù)化思想的出現(xiàn)，然而歷史上最先從理論上明確提出定理證明機(jī)械化思想的是希爾伯特。1899年，他在《幾何基礎(chǔ)》這部經(jīng)典名著中指出，初等幾何中只涉及從屬平行的定理可以實(shí)現(xiàn)證明的機(jī)械化，他還提出了有名的“希爾伯特機(jī)械化定理”。希爾伯特的幾何機(jī)械化思想遵循的就是一條幾何代數(shù)化的道路：從公理系統(tǒng)出發(fā)，建立坐標(biāo)系，引進(jìn)數(shù)系統(tǒng)，把幾何定理的證明轉(zhuǎn)化為代數(shù)式的計(jì)算。這是一條從公理化走向代數(shù)化直至數(shù)值化的道路。1950年，波蘭數(shù)理邏輯學(xué)家塔爾斯基進(jìn)一步從理論上證明，初等代數(shù)和初等幾何的定理可以機(jī)械化。他還提出了以他的名字命名的機(jī)械化定理以及制造證明機(jī)的設(shè)想。

　　機(jī)器證明史上的第一項(xiàng)奠基性的突破，是由美國(guó)的卡內(nèi)基大學(xué)—蘭德公司協(xié)作組做出的。1956年，這個(gè)協(xié)作組的西蒙、紐厄爾和肖烏等人在電子計(jì)算機(jī)上成功地證明了羅素和懷特海所著的《數(shù)學(xué)原理》第二章52條定理中的38條。這一年可作為歷史上計(jì)算機(jī)證明定理的開(kāi)端。1963年，他們又在計(jì)算機(jī)上證明了全部52條定理，西蒙等人使用的是LT（邏輯理論機(jī)）程序。這種程序不是刻板的固定算法程序，而是使用了心理學(xué)方法，將人腦在進(jìn)行演繹推理時(shí)的邏輯過(guò)程、所遵循的一般規(guī)則和所經(jīng)常采用的策略、技巧，以及簡(jiǎn)化步驟的一些方法等編進(jìn)計(jì)算機(jī)程序，讓計(jì)算機(jī)具有自己去探索解題途徑的某種能力。這一程序?yàn)闄C(jī)器證明提供了一個(gè)切實(shí)可行的算法，通常稱它為“啟發(fā)式程序”。

　　在機(jī)器證明的開(kāi)拓者中，還有著名的美籍華人王浩教授。1959年，他只用9分鐘的機(jī)器時(shí)間，就在計(jì)算機(jī)上證明了羅素和懷特海《數(shù)學(xué)原理》一書(shū)中的'一階邏輯部分的全部定理350多條，在當(dāng)時(shí)數(shù)學(xué)界引起了轟動(dòng)。

　　改進(jìn)算法程序是提高機(jī)器證明效率的一個(gè)重要方面。在這方面，美國(guó)數(shù)學(xué)家魯濱遜首先取得了重大突破。1965年，他提出了有名的歸結(jié)原理。這一原理的基本出發(fā)點(diǎn)是，要證明任何一個(gè)命題為真，都可以通過(guò)證明其否定為假來(lái)得到。它要求把問(wèn)題用一階邏輯表示出來(lái)，并且變?yōu)橹痪哂杏勒媸交蛴兰偈叫再|(zhì)的公式。由于許多定理都可以在一階邏輯中得到表示，因而這一程序具有較大的實(shí)用性，對(duì)提高機(jī)器證明的效率有著重要的方法論意義，大大地推動(dòng)了機(jī)器證明的研究。

　　70年代，機(jī)器證明得到新的重大進(jìn)展。1976年，美國(guó)數(shù)學(xué)家阿佩爾和黑肯借助計(jì)算機(jī)成功地解決“四色猜想”的證明問(wèn)題。這是機(jī)器證明首次解決傳統(tǒng)人腦支配手工操作所長(zhǎng)期沒(méi)能解決的重大問(wèn)題。1971-1977年間，萊得索等人給出了分析拓樸學(xué)和集合論方面的一些著名定理的機(jī)器證明。1979年，波依爾和穆?tīng)柕热俗鞒隽诉f歸函數(shù)方面的機(jī)器證明系統(tǒng)。

　　我國(guó)數(shù)學(xué)家在機(jī)器證明研究上取得了顯著的成果，引起了國(guó)內(nèi)外學(xué)術(shù)界的關(guān)注。1977年，吳文俊教授證明了初等幾何主要一類(lèi)定理的證明可以機(jī)械化。1980年，他還用一部微機(jī)在20和60個(gè)機(jī)器小時(shí)左右分別發(fā)現(xiàn)了兩個(gè)幾何學(xué)的新定理。吉林大學(xué)和武漢大學(xué)的研究人員也在定理的機(jī)器證明方面取得了許多可喜的成果。

　　上面我們考察和分析了數(shù)學(xué)史上發(fā)生的6次重大突破。除了這6次重大突破外，還有許多重大事件也都具有一定的突破性，它們都不同程度地帶來(lái)了數(shù)學(xué)思想方法的重大變化。如非歐幾何的發(fā)現(xiàn)，群論的產(chǎn)生，勒貝格積分的建立，突變理論的出現(xiàn)，非標(biāo)準(zhǔn)分析的誕生，就是這樣的事件。現(xiàn)代科學(xué)技術(shù)革命的興起，向數(shù)學(xué)提出了一系列新的重大課題，可以預(yù)想，對(duì)這些課題的探討，必將會(huì)引起數(shù)學(xué)在思想方法上發(fā)生新的重大突破，使數(shù)學(xué)的面貌發(fā)生新的改觀。

【數(shù)學(xué)思想方法的重大突破分析】相關(guān)文章：

重大突破思想方法常量變量學(xué)到數(shù)學(xué)05-12

數(shù)學(xué)思想方法分析05-05

數(shù)學(xué)思想方法06-26

小學(xué)數(shù)學(xué)數(shù)學(xué)思想方法06-27

關(guān)于數(shù)學(xué)的思想方法05-09

數(shù)學(xué)思想方法的突破05-11

數(shù)學(xué)思想方法推薦05-06

數(shù)學(xué)的轉(zhuǎn)化思想方法05-06

中考數(shù)學(xué)思想方法05-06