這個話題有點冷門。說它冷門，其實現在卻是最熱話題一一人工智慧。它是人工智慧發展的開端，只不過現在大家都在談人工智慧，很少提機器證明了。對機器證明，本人談不上懂，但也有一些瞭解，早前也曾接觸過這方面的軟體，就以我所知來說說吧。

數學機械化，主要是指幾何定理的機器證明。用機器來進行自動推理，特別是用機器來證明幾何定理，在數學史上有很多牛人都有此夢想，也是長期困擾西方學術界的研究課題。

不得不梳理梳理一下機械證明的發展史，藉此向一個個名字如雷貫耳的數學牛人致敬，瞭解一下他們為機械證明所作的貢獻。

事實上，早在十七世紀數學大伽萊布尼茲（創立微積分的牛人）就有機械化證明的設想，但僅是設想而已進展不大，到了近代十九世紀末，另一個數學大伽希爾伯特及其信徒創立並發展了數理邏輯，使得機器證明有了較大進展一一有明確的數學形式，又過了近半個世紀，二十世紀四十年代馮諾依曼發明電子管計算機，才使萊氏的設想有了實現的可能和條件。機器證明中的機器當然是就專指計算機了。

因而幾何定理的機器證明演變為指用計算機自動證明某一型別幾何定理，甚至某幾何體系全部定理的原理和方法。其背後都要經歷公理化，代數化，座標化，機械化等步驟，主要用來證明初等幾何定理。諸定理分三種類型對應三種不同的機械證明方法。（等會我們還要說到中國的數學大伽為此所作的貢獻）這三種方法分別是希爾伯特方法，效率高，但適用面窄；塔斯基方法，效率低，但適用面寬；重點來了，中國著名數學家，中科院院士吳文俊於1977年給出了初等幾何一類主要定理的機械化證明方法，引起國際學界關注，並稱之為“吳文俊方法”。

1980年在HP9835A型機上用該方法證明一批初等幾何定理，還推廣到微分幾何，仿射微分幾何等領域。由於在機器證明開創性的貢獻，吳院士榮獲首屆（2001年）國家最高科技獎一一自然科學一等獎。在吳院士的帶領和倡導下，中國的數學機械化研究始終與世界同步，處於世界先進陣營。

其後又有張景中，高小山等人在吳文俊院士的基礎上進一步豐富發展了"吳方法”，1992年張景中院士提出了幾何定理機器證明的新方法，即基於幾何不變數的消點法，並與高小山，周鹹青等人合作完善了該方法。張院士後來將此模組整合到專門的數學學習軟體"Z十Z"中，筆者早期接觸到的機器證明就是這個，而“Z十Z“又發展為“超級畫板“再發展為今天的“動態數學“了，也就是皓俊數學實驗室的拳頭產品了。為寫此文筆者專門向他們諮詢了一下，如需要這方面的軟體可以到中科院系統科學研究院網站下載。

您是想知道機械運算的原理吧。最早實現機械運算的是圖靈機。

圖靈機利用了一個紙帶的模型進行計算。這條紙帶被分割成了一個個的方格，方格中只能有空白,0,1這三個值。而紙帶一次運算可向左或向右移動一格，或者不動。利用這個簡單的模型，人們可以用有限步驟的程式控制紙帶移動和讀寫方格的值，完成複雜的計算。在下圖中，紙帶上第一個1代表0,第2個1代表1以此類推。兩個數用0分割。加法計算透過控制紙帶移位和讀寫的程式完成。

所謂機械運算只能實現數學計算，不能直接進行邏輯推理。證明幾何問題的思路一般是，用排列組合的方法將所有可能的結果枚舉出來，然後，一個一個地進行計算，直到計算結果滿足證明條件。