電腦協助證明是一種部分或全部內容以電腦協助之數學證明。
基本介紹
- 中文名：電腦協助證明
- 外文名：Computer-assisted proof
- 分類：數理科學
哲學爭議,歷史,四色定理,著名的電腦協助證明,
哲學爭議
由於大部分的電腦協助證明計算量龐大，無法以人手驗證，很多數學家不接受電腦協助證明，並表示那只是計算而非證明。他們表示，美麗的數學證明應像首詩，而電腦證明則看似電話簿。
歷史
第一個著名的電腦協助證明，是1976年的四色定理證明。
四色定理
四色定理是一個著名的數學定理：如果在平面上劃出一些鄰接的有限區域，那么可以用四種顏色來給這些區域染色，使得每兩個鄰接區域染的顏色都不一樣；另一個通俗的說法是：每個無外飛地的地圖都可以用不多於四種顏色來染色，而且不會有兩個鄰接的區域顏色相同。被稱為鄰接的兩個區域是指它們有一段公共的邊界，而不僅僅是一個公共的交點。例如右圖左下角的圓形中，紅色部分和綠色部分是鄰接的區域，而黃色部分和紅色部分則不是鄰接區域。
“是否只用四種顏色就能為所有地圖染色”的問題最早是由一位英國製圖員在1852年提出的，被稱為“四色問題”或“四色猜想”。人們發現，要證明寬鬆一點的“五色定理”（即“只用五種顏色就能為所有地圖染色”）很容易，但四色問題卻出人意料地異常困難。曾經有許多人發表四色問題的證明或反例，但都被證實是錯誤的。
1976年，數學家凱尼斯·阿佩爾和沃夫岡·哈肯藉助電子計算機首次得到一個完全的證明，四色問題也終於成為四色定理。這是首個主要藉助計算機證明的定理。這個證明一開始並不為許多數學家接受，因為不少人認為這個證明無法用人手直接驗證。儘管隨著計算機的普及，數學界對計算機輔助證明更能接受，但仍有數學家希望能夠找到更簡潔或不藉助計算機的證明。
