2017年12月27日

談電腦輔助證明

游森棚/任教於臺灣師範大學數學系及空軍官校。


這個月的專欄來談談電腦輔助證明,我們來看看幾個例子。

五邊形拼平面
先回憶一下前(2016)年4 月份的本專欄文章〈拼滿平面的五邊形〉,數學家對用全等的凸多邊形能否週期性地拼滿整個平面非常感興趣。因為用任意三角形一定可以鋪滿平面,要判斷四邊形是否能鋪滿平面也不難,六邊形以上因為內角和的關係不可能,所以,只剩下五邊形。那篇專欄中,說明了這100 年間,一路下來只找到15 種五邊形可以鋪滿平面,而且第15 種還是在2015 年才找到的(圖一)。因為長度和角度都是「漂亮的」,這個形狀也成為2016 年大學學測的題目。

圖一

而其實,第15 種是用電腦搜尋出來的,是否只有15 種?還是一個有名的未解問題,至少在去年我寫專欄的時候還是一個未解問題。

今年7 月,法國國家科學研究中心(Centre national de la recherche scienti que, CNRS)的研究員拉奧(Michaël Rao)宣稱終結了這個問題。他的結果是拼滿平面的五邊形就只有這15 種。拉奧的證明用到了電腦輔助證明。他先透過數學方式把整個問題分成371 類,然後再用電腦進行大量的計算處理。目前論文已經投稿,還在接受同儕的審查中,所以此證明是否能證明真的只有這15種可能還要再等一陣子才知道。然現今數學界類似這種「證明中的一大部分是電腦完成」的證明,真的是愈來愈多了。

四色定理
往前回溯,來看看著名的四色定理。這是第一個用電腦輔助證明出來的大定理。四色定理是說任何一個地圖只要用四個顏色,就可以讓相鄰區域不同色。這並不顯然,如圖二,讀者可以試試看能不能用4 個顏色就讓相鄰區域不同色。(相當不容易!)

圖二

四色定理的第一個證明在1976年由數學家阿佩爾(Kenneth Appel)與哈肯(Wolfgang Haken)發表。經過數百頁的紙筆證明,他們把問題化為只要考慮1936 個特殊的圖形。經過電腦連續計算1200 個小時(50 天)後,得到這1936 個圖形都是不可約的(irreducible)構形,從而證明了四色定理。

50 年前就用電腦來輔助證明,真是一個劃時代的想法。但因為這個證明的手法太過先進, 因此四色定理的證明是否「合法」,一直受到數學家的質疑。這些數學家堅持所有的「證明」必須是能夠一行一行用人腦檢驗的,畢竟電腦計算量這麼大,都在中央處理器(CPU)中黑箱作業,連續算了50 天,到底中間發生什麼事,有沒有出錯,誰能知道?

因此,從此證明發表以來,有幾個團隊改良了證明。雖然現在還是需要電腦的幫忙,但質疑的聲音力道已少了許多。

克卜勒的最密堆積
時代和觀念總是會變化的,電腦輔助證明的一大肯定是克卜勒最密堆積問題的證明。假設你有許多個一元銅板要放在桌上,怎麼放會最密?......【更多內容請閱讀科學月刊第577期】

沒有留言: