數(shù)學(xué)問(wèn)題的機(jī)械化，就是要求在運(yùn)算或證明過(guò)程中，每前進(jìn)一步之后，都有一個(gè)確定的、必須選擇的下一步，這樣沿著一條有規(guī)律的、刻板的道路，一直達(dá)到結(jié)論。即所謂的機(jī)械化就是刻板化和規(guī)格化。這一導(dǎo)源于中國(guó)古代傳統(tǒng)數(shù)學(xué)，由于計(jì)算機(jī)的出現(xiàn)而呈現(xiàn)旺盛生命力的數(shù)學(xué)機(jī)械化思想在數(shù)學(xué)研究上已經(jīng)發(fā)揮出它的巨大威力，并且對(duì)當(dāng)今數(shù)學(xué)及數(shù)學(xué)教學(xué)產(chǎn)生了具大的影響。

簡(jiǎn)介

數(shù)學(xué)機(jī)械化是我國(guó)數(shù)學(xué)家開創(chuàng)的基礎(chǔ)研究領(lǐng)域。20多年來(lái)，吳文俊先生身體力行、滿腔熱情地倡導(dǎo)數(shù)學(xué)機(jī)械化研究，其內(nèi)容、方法和意義日益獲得科學(xué)界的理解和贊同。

研究人員

計(jì)算機(jī)證明數(shù)學(xué)問(wèn)題是由吳文俊提出，華人美籍?dāng)?shù)學(xué)家王浩也是最初的研究人員之一，它是極為神奇的超級(jí)工程數(shù)學(xué)，有可能引發(fā)工程技術(shù)的革命和某些基礎(chǔ)數(shù)學(xué)的革命。

數(shù)學(xué)

是研究數(shù)量關(guān)系和形體性質(zhì)的科學(xué)?！皵?shù)”與“形”在現(xiàn)實(shí)世界中無(wú)處不在，因此，數(shù)學(xué)科學(xué)是自然科學(xué)的基礎(chǔ)，也是高新技術(shù)的基礎(chǔ)，甚至是工程建設(shè)的基礎(chǔ)，這已是人們的共識(shí)。數(shù)學(xué)科學(xué)的好處是，可以化難為易，把奧妙變?yōu)槌ＷR(shí)，為各類問(wèn)題的解決提供框架。

在產(chǎn)業(yè)革命的進(jìn)程中，各類機(jī)器不斷問(wèn)世，逐步實(shí)現(xiàn)著體力勞動(dòng)的機(jī)械化。這已延續(xù)了數(shù)百年。伴隨著這一過(guò)程，自然科學(xué)獲得了巨大進(jìn)步，數(shù)學(xué)科學(xué)取得了現(xiàn)代數(shù)學(xué)的偉大發(fā)現(xiàn)。如今，人類社會(huì)正步入信息革命時(shí)代。計(jì)算機(jī)的功能不斷增強(qiáng)，人類社會(huì)開始逐步實(shí)現(xiàn)腦力勞動(dòng)的機(jī)械化。數(shù)學(xué)研究是典型的腦力勞動(dòng)，具有論證嚴(yán)謹(jǐn)、表述明確等優(yōu)點(diǎn)，理應(yīng)率先實(shí)現(xiàn)機(jī)械化。

20世紀(jì)70年代，吳文俊先生研讀中國(guó)數(shù)學(xué)史。中國(guó)古代數(shù)學(xué)，既有系統(tǒng)的理論，又有豐碩的成果，這些成果經(jīng)常以算法（術(shù)）的方式表述，其理論依據(jù)則總結(jié)為一些原理。直到16世紀(jì)，中國(guó)數(shù)學(xué)在很多分支都在國(guó)際上遙遙領(lǐng)先，是名副其實(shí)的數(shù)學(xué)強(qiáng)國(guó)。吳文俊先生提出，數(shù)學(xué)機(jī)械化思想貫穿于中國(guó)傳統(tǒng)數(shù)學(xué)，數(shù)學(xué)機(jī)械化思想是我國(guó)古代數(shù)學(xué)的精髓。他分析了中國(guó)傳統(tǒng)數(shù)學(xué)的光輝成就在數(shù)學(xué)科學(xué)進(jìn)步歷程中的地位和作用，明確指出，源于西方的公理化思想和源于中國(guó)的機(jī)械化思想，對(duì)于數(shù)學(xué)的發(fā)展都發(fā)揮了巨大作用，理應(yīng)兼收并蓄。如今，計(jì)算機(jī)科學(xué)被認(rèn)為是算法的科學(xué)。以算法為核心的機(jī)械化思想，既傳統(tǒng)又前瞻，將為信息時(shí)代數(shù)學(xué)科學(xué)的創(chuàng)新發(fā)揮重大作用。

理論基礎(chǔ)

數(shù)學(xué)機(jī)械化研究，是在初等幾何定理的機(jī)器證明研究方面取得突破的。公理化體系的幾何定理證明非常不機(jī)械化。以中學(xué)課程中的幾何為例，－個(gè)定理的證明，往往要經(jīng)過(guò)冥思苦想，奇巧構(gòu)思，無(wú)章可循地填加輔助線，迂回曲拆地給出證明。如何利用計(jì)算機(jī)進(jìn)行自動(dòng)推理，特別是進(jìn)行幾何定理的自動(dòng)證明，是學(xué)術(shù)界長(zhǎng)期研究的課題。所謂定理的機(jī)械化證明，就是對(duì)一類定理（這類定理可能成千上萬(wàn)）提供一種統(tǒng)一的方法，使得該類定理中每個(gè)定理，都可依此方法給出證明。在證明過(guò)程中，每前進(jìn)一步，都有章可循地確定下一步該做什么和如何做。從“一理一證”到“－類一證”，是數(shù)學(xué)的認(rèn)識(shí)和實(shí)踐的飛躍。吳先生創(chuàng)立了初等幾何（泛指不具有微分運(yùn)算的幾何，如歐氏幾何、非歐幾何、仿射幾何、投影幾何、代數(shù)幾何等等）定理證明的機(jī)械化方法，國(guó)際上稱“吳方法”，首次實(shí)現(xiàn)了高效的幾何定理的機(jī)器證明?！皡欠椒ā币部捎糜趲缀味ɡ淼淖詣?dòng)發(fā)現(xiàn)和未知關(guān)系的自動(dòng)推導(dǎo)。吳文俊先生的開創(chuàng)性成果，打破了國(guó)際自動(dòng)推理界在幾何定理自動(dòng)證明研究中長(zhǎng)期徘徊不前的局面，也使我國(guó)在這一領(lǐng)域處于領(lǐng)先地位。吳先生的杰出貢獻(xiàn)，使他獲得1998年度國(guó)際自動(dòng)推理界的最高獎(jiǎng)“Herbrand獎(jiǎng)”。（此獎(jiǎng)每?jī)赡觐C發(fā)一次，每屆最多授予一人，迄今為止，獲獎(jiǎng)?wù)呔鶠樽詣?dòng)推理界的領(lǐng)袖人物。）

幾何學(xué)

幾何學(xué)包括定理證明、幾何作圖和幾何不等式證明。在吳先生開創(chuàng)性成果的影響和啟迪下，在幾何學(xué)的機(jī)械化方面，如定理機(jī)器證明、幾何自動(dòng)作圖和幾何不等式機(jī)器證明，我國(guó)學(xué)者都取得了很大成績(jī)。這個(gè)領(lǐng)域也開始吸引外國(guó)學(xué)者向我們學(xué)習(xí)。

眾所周知，直線和平面等幾何概念可由一次代數(shù)方程描述，多項(xiàng)式方程則用于描述曲線和曲面等。數(shù)學(xué)科學(xué)中，從線性到非線性的第一步跨躍，是由多項(xiàng)式實(shí)觀的。因此，多項(xiàng)式方程組求解是非線性數(shù)學(xué)最基本的課題，這個(gè)問(wèn)題的研究已經(jīng)持續(xù)幾百年。數(shù)學(xué)不同分支中許多的問(wèn)題、自然科學(xué)不同領(lǐng)域中很多的問(wèn)題、高新技術(shù)中大量的問(wèn)題，都可轉(zhuǎn)化為多項(xiàng)式方程組求解。在幾何定理機(jī)器證明的過(guò)程中，必須理清多項(xiàng)式方程組的零點(diǎn)結(jié)構(gòu)。這一需求，促使吳先生創(chuàng)立了多項(xiàng)式方程組求解的理論和方法，國(guó)際上稱“特征列法”或“吳消元法”。吳先生還把這些方法拓展到微分情形，建立了微分幾何定理機(jī)器證明和微分代數(shù)方程組求解的機(jī)械化理論和方法。自然，較之代數(shù)情形，微分代數(shù)的應(yīng)用范圍更為廣闊，同時(shí)，問(wèn)題的研究更為復(fù)雜和困難。

證定理和解方程

證定理和解方程，大體上涵蓋了數(shù)學(xué)活動(dòng)的主要內(nèi)容。在機(jī)證定理和機(jī)解方程兩個(gè)方面，吳文俊先生在理論和方法上都做出了原創(chuàng)性的貢獻(xiàn)。

相關(guān)言論

吳文俊先生強(qiáng)調(diào)：“數(shù)學(xué)機(jī)械化方法的應(yīng)用，是數(shù)學(xué)機(jī)械化研究的生命線”。他本人的研究工作己涉及許多應(yīng)用領(lǐng)域，如線性控制系統(tǒng)、機(jī)構(gòu)綜合設(shè)計(jì)、平面星體運(yùn)行的中心構(gòu)形、化學(xué)反應(yīng)方程的平衡、代數(shù)曲面的光滑拼接、從開普勒定律自動(dòng)惟出牛頓定律、全局優(yōu)化求解等等。在他的指導(dǎo)和帶動(dòng)下，數(shù)學(xué)機(jī)械化方法己在一些交叉研究領(lǐng)域獲得初步應(yīng)用，如理論物理、計(jì)算機(jī)科學(xué)、信息科學(xué)、自動(dòng)推理、工程幾何、機(jī)械機(jī)構(gòu)學(xué)等等。數(shù)學(xué)機(jī)械化研究不斷開拓更多的應(yīng)用方面。

吳文俊先生說(shuō)過(guò)，從事數(shù)學(xué)研究，要有良好的思維方式，在思想觀念上要有所突破。許多事例表明，－些數(shù)學(xué)分支正是由于踏上了機(jī)械化的道路而獲得了蓬勃的發(fā)展，使之成為重要的研究方向，甚至成為數(shù)學(xué)的主流。這是因?yàn)?，抽象的?shù)學(xué)概念和結(jié)論，往往是難于掌握和運(yùn)用的。當(dāng)把抽象的概念變成具體可算的（算法經(jīng)常用公式表達(dá)），既有定性的結(jié)論又有定量的計(jì)算，數(shù)學(xué)理論才臻于完善，易于接受和適宜應(yīng)用。運(yùn)用機(jī)械化思想考察數(shù)學(xué)，將會(huì)發(fā)現(xiàn)數(shù)學(xué)的不同側(cè)面，建立新的模式，活躍和啟迪數(shù)學(xué)家的思維，從而產(chǎn)生大量的原始創(chuàng)新。

發(fā)展

在信息革命時(shí)代，數(shù)學(xué)將出現(xiàn)什么樣的變化？尤其是，中國(guó)的數(shù)學(xué)將如何進(jìn)步？這是數(shù)學(xué)家們經(jīng)常思考的問(wèn)題。倡導(dǎo)和開展數(shù)學(xué)機(jī)械化研究，則為中國(guó)數(shù)學(xué)的發(fā)展提出了一種戰(zhàn)略導(dǎo)向。如今數(shù)學(xué)機(jī)械化研究剛剛處于起步階段。吳文俊先生制定的目標(biāo)十分明確：讓數(shù)學(xué)機(jī)械化思想普照數(shù)學(xué)的各個(gè)角落。這是將要綿延幾代人的事業(yè)，需要各個(gè)方面專家的參與和共同努力。