幾何定理的機(jī)器證明

張景中　彭翕成

幾千年來，人們解幾何題的招數(shù)，層出不窮，爭奇斗艷，概括起來，不外這4類：檢驗(yàn)、搜索、歸約和轉(zhuǎn)換，50多年來，數(shù)學(xué)家和計算機(jī)科學(xué)家費(fèi)盡心思，循循善誘，把個中奧秘向計算機(jī)傳授，使得計算機(jī)解幾何題的能力日新月異，大放光彩，除了靈機(jī)一動加輔助線，或千變?nèi)f化的問題轉(zhuǎn)換之外，前3種方法計算機(jī)都學(xué)得十分出色了，用機(jī)器幫助，以至在某種程度上代替學(xué)者研究幾何，幫助乃至代替老師指導(dǎo)學(xué)生學(xué)習(xí)幾何，已經(jīng)從古老的夢想變?yōu)楝F(xiàn)實(shí)。

在幾何定理機(jī)器證明中，采用代數(shù)方法，引進(jìn)坐標(biāo)，將幾何定理的敘述用代數(shù)方程的形式重新表達(dá)，證明問題就轉(zhuǎn)化成判定是否能從假設(shè)的代數(shù)方程推出結(jié)論的代數(shù)方程的問題，這樣把幾何問題代數(shù)化，自笛卡爾以來已是老生常談，并無實(shí)質(zhì)困難，然而代數(shù)化的過程，坐標(biāo)點(diǎn)的選取和方程引進(jìn)的次序都可能影響到后續(xù)證明的難度，甚至由于技術(shù)條件的限制，影響到證明是否可能完成，也就是說，幾何問題化成純代數(shù)問題之后，也并不見得一定容易，更不能說就能實(shí)現(xiàn)機(jī)械化了，這不僅是因?yàn)榻鉀Q這些代數(shù)問題的計算量往往過大，令人望而卻步，還因代表幾何關(guān)系而出現(xiàn)的那些代數(shù)等式或不等式常常雜亂無章，使人手足無措，從這些雜亂無章的代數(shù)關(guān)系式中要找出一條途徑，以達(dá)到所要證的結(jié)論，往往要用到高度的技巧，換句話說，即使你不怕計算，會用計算機(jī)來算，也不知道從何算起。

解幾何題是思維的體操，是十分有吸引力的智力活動之一，圖形的直觀簡明，推理的曲折嚴(yán)謹(jǐn)，思路的新穎巧妙，常給人以美的享受，許多青少年數(shù)學(xué)愛好者，往往首先是對幾何有了濃厚的興趣，用計算機(jī)證明幾何問題，如果僅限于用平凡而繁瑣的數(shù)值計算代替巧妙而難于入手的綜合推理，則未免大煞風(fēng)景，通過計算機(jī)的大量計算判斷命題為真，確實(shí)是證明了定理，這是有嚴(yán)謹(jǐn)理論基礎(chǔ)的，但這樣的證明寫出來只是一大堆令人眼花繚亂的算式、數(shù)字或符號，既沒有直觀的幾何意義，又難于理解和檢驗(yàn)，這跟幾何教科書上十行八行就說得明明白白的傳統(tǒng)風(fēng)格的證明大相徑庭，如果計算機(jī)給出的這一堆難于理解和檢驗(yàn)的數(shù)據(jù)也算是幾何問題的解答，這種解答只能叫做不可讀的解答。

所幸的是，計算機(jī)不僅能計算，也能推理，只要我們會教，它也能學(xué)會傳統(tǒng)風(fēng)格的幾何解題方法，我們希望的是，既要用計算機(jī)幫助人腦，減輕人的高級腦力勞動，還要在提高效率的同時，尋求保持傳統(tǒng)幾何的魅力。