- 專欄
文章專區
2018-01-01談電腦輔助證明
577 期
Author 作者
游森棚／任教於臺灣師範大學數學系及空軍官校。
這個月的專欄來談談電腦輔助證明，我們來看看幾個例子。
五邊形拼平面
先回憶一下前（2016）年 4 月份的本專欄文章〈拼滿平面的五邊形〉，數學家對用全等的凸多邊形能否週期性地拼滿整個平面非常感興趣。因為用任意三角形一定可以鋪滿平面，要判斷四邊形是否能鋪滿平面也不難，六邊形以上因為內角和的關係不可能，所以，只剩下五邊形。
那篇專欄中，說明了這100年間，一路下來只找到15種 五邊形可以鋪滿平面，而且第15 種還是在2015年才找到的（圖一）。因為長度和角度都是「漂亮的」，這個形狀也成為2016年大學學測的題目。
而其實，第15種是用電腦搜尋出來的，是否只有15種？還是一個有名的未解問題，至少在去年我寫專欄的時候還是一個未解問題。
今年7月，法國國家科學研究中心（Centre national de la recherche scientifique, CNRS）的研究員拉奧（Michaël Rao）宣稱終結了這個問題。他的結果是拼滿平面的五邊形就只有這15種。拉奧的證明用到了電腦輔助證明。 他先透過數學方式把整個問題分成371類，然後再用電腦進行大量的計算處理。目前論文已經投稿，還在接受同儕的審查中，所以此證明是否能證明真的只有這15種可能還要再等一陣子才知道。但，目前數學界類似這種 「證明中的一大部分是電腦完成」的證明，真的是愈來愈多了。
四色定理
往前回溯，來看看著名的四色定理。這是第一個用電腦輔助證明出來的大定理。四色定理是說任何一個地圖只要用四個顏色，就可以讓相鄰區域不同色。這並不顯然，如圖二，讀者可以試試看能不能用4個顏色就讓相鄰區域不同色。（相當不容易！）
四色定理的第一個證明在1976年由數學家阿佩爾（Kenneth Appel）與哈肯（Wolfgang Haken）發表。經過數百頁的紙筆證明，他們把問題化為只要考慮1936 個特殊的圖形。經過電腦連續計算 1200個小時（50 天）後，得到這1936個圖形都是不可約的（irreducible）構形，從而證明了四色定理。……【更多內容請閱讀科學月刊第577期】