用計算機軟件驗證和證明數學問題應謹慎

文/寧玉川

摘 要：計算機圖形軟件的算法也是基于數學理論建立起來的，由于程序員編寫的程序所運用的數學原理是看不到的，因此一不小心，就會犯下循環論證的錯誤。

關鍵詞：計算機證明；循環論證；過程目標

在初中數學教材（人教版）上，設置了幾個可用計算機軟件去驗證的數學問題，如，探索旋轉的性質、探索二次函數性質、探索位似性質等。這些內容的設置，豐富了教材的內容，增強了教材的趣味性，具有一定的時代特色。

但是，用計算機驗證或證明數學問題真的具有合理性嗎？

比如，在初中數學教材（人教版）九年級下冊，第27章中的“平行線等分線段對應成比例”一節，課本上是通過讓學生畫圖并測量得出結論的。然而，學生畫圖和測量不可能十分精確，都會出現誤差，有的只能得出近似成比例的結果，這時，我們應該用歸納法得出猜想，再通過大量實驗驗證其合理性、真實性、可靠性。

如果某人試圖用相似三角形的性質去證明上述定理，顯然是十分荒謬的，顯然這是犯了循環論證的錯誤。

也有的教師為了能完美地得出精確的實驗結果，提出了用計算機軟件測量驗證的方法，甚至在一些公開課活動中，也動用了此方法。評課時，很多教師對此大加贊賞，說什么既減少了實驗誤差，又使用了現代教學手段。豈不知，不知不覺中，我們就有可能犯了一個嚴重的邏輯錯誤——循環論證。

為什么這樣說呢？

因為計算機圖形軟件的算法也是基于數學理論建立起來的，各種應用軟件都是用一些計算機高級語言程序開發的，這些高級語言為開發者提供了大量的函數（又稱為類）模型，用于軟件開發者綜合使用這些函數處理各種信息，包括圖形。而應用程序的使用者之所以移動鼠標就可以畫出各種圖形，是因為計算機通過應用軟件把鼠標的坐標信息傳遞給了這些函數模型，從而畫出（顯示）了相應的圖象。在高級語言提供的類函數中，包含了類似于平線線分線段成比例的類函數，這個類函數就是基于平行線分線段成比例建立起來的。我們應用計算機軟件畫出的三條平行線分兩條直線一定是符合函數模型的，也就是說計算機是運用平行線分線段成比例計算出顯示坐標，從而了畫出的平行直線。如果我們又反過來用計算機建立的平行直線去驗證所截線段是否成比

例，那恰好等同于用平行線分線段成比例本身去驗證自己。所以說，用計算機軟件證明上述定理是荒謬的，犯了循環論證的嚴重錯誤。

也許某些圖形軟件在處理有關平行線的繪圖時沒有使用類似于平線線分線段成比例的類函數，而使用的是與之不相關聯的算法編寫的應用程序。如果是這樣的話，我們使用它去證明上述的平行線分線段成比例是沒有問題的。可是我們不是應用程序的編寫者，當然并不知道某個軟件運行時，使用的是何種算法，因此盲目用計算機軟件證明一個數學問題是不可靠的。

我們不要誤認為計算是萬能的，計算機是人類用已有的智慧建造出來的，在計算速度和記憶檢索能力方面超過了自然人，但是這些能力畢竟是程序編制者賦予的，在計算方法方面永遠按照編程者給出的指令去運行。編程者所提供給計算機的計算方法，無不來自已有的數學定理定律。到目前為止，還沒聽說過哪臺計算機能自己編寫真正意義的新的計算方法。一些原初的基本的定理，是不可能用計算機證明的。所謂計算機證明、驗證，充其量只是一種旁證而已。也就是說，計算機只可以證明一些推論，驗證一些推廣，驗證解答的正確性。所以說計算機證明只是一種輔助的驗證，具有很大的局限性。

所謂的計算機計算證明，至少到現在為止，還處于初級的研究階段。就拿最為著名的“用計算機證明四色定理”為例：20世紀初，肯普提出了一個證明的思路，不過過程十分繁雜。富蘭克林于1939年證明了22國以下的地圖都可以用四色著色。1950年以后，人們把定理的證明推廣到35國地圖。1960年又證明了39國以下的地圖也可以，隨后又推進到了50國。但是由于運算十分復雜，推進十分緩慢。直到1976年，美國數學家阿佩爾與哈肯把證明方法過程編寫成程序輸入了計算機，讓這些復雜演算用計算機去完成，結果計算機用了1千多小時，做了100億多個判斷，終于完成了四色定理的證明，轟動了全世界。兩位數學家謙虛地說是計算機完成了四色定理的證明。不過多數科學家并不贊同這是計算機取得的成就，因為這個證明的辦法是數學家找到的，只是因計算量特別大，短時間內用紙筆很難完成，所以編寫成程序輸入計算機，計算機發揮了其計算速度快的特點，在一個相對較短的時間內，按照人所設定的流程，完成了繁雜的演算過程而已。至今人們還在尋找四色定理簡潔明快的書面證明方法。

綜上所述，計算機證明數學問題，至今仍處于探索研究階段。我們在教學中不要輕言所謂用計算機去證明數學定理，不要誤導學生，不要讓他們誤認為可以不用學習，什么事情都可以交給計算機，要讓學生知道計算機也是聽人的指揮的。

雖然用計算機去證明數學定理是不一定都是可行的，但是我們用它驗證和解題倒是可以的，讓它協助我們做一些復雜的演算也是可以的。初中教材中所提供的都是用計算機驗證的方法，這種驗證只是在一些局部的范圍內具有合理性，所以不能亂用。由于程序員編寫的程序所運用的數學原理你是看不到的，因此一不小心，我們在不知道的情況下就會犯下循環論證的錯誤。

參考文獻：

孫熙椿.幾何定理計算機證明［M］.科學出版社，2007-06-01.

編輯 韓 曉

endprint