幾何定理的機器證明

張景中　彭翕成

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

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

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

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