2017-06-27

【關鍵評論】Kayue:「99%確定」還不足夠,所以這數學家再次證明了「克卜勒猜想」 (1222)

16世紀數學家Thomas Hariot是最早以數學研究球體排列的人,天文學家兼數學家克卜勒(Johannes Kepler)在17世紀初期跟Harriot通信,開始對球體排列問題產生興趣。

兩人的通信跟Hariot的原子理論有關,克卜勒最初並不接受,但在1611年的文章中,他探討如果物質都是由極小的球體粒子組成,會有甚麼後果。他的文章描述了「面心立方」裝球法,並指這是最緊密的方式,後來就成為了「克卜勒猜想」(Kepler’s conjecture)。

所謂「面心立方」裝球法,以下圖左邊的排列球體方式,右邊的則稱為「六方最密堆積」法︰

Closepacking
Image Credit: Cdang, derived from Muskid, CC BY-SA 3.0

兩種排列方式的平均密度相同,均為約74.05%(實際比例為π/√18),即球體平均會佔據近74.05%的空間。不過克卜勒未能證明他的說法,成為一項有待證明的數學猜想。如果用淺白的語言來說,克卜勒猜想就是︰「排列球體的最佳方式,就是像小販放橙的那樣」,當然,小販只需要處理有限個橙[1]

一個球同時可親吻多少個球?

跟克卜勒猜想相關的一個問題,就是研究球面的「親吻數」(kissing number)。在平面世界,一個圓形最多可以外接6個圓形,因此二維空間的親吻數是6(圓形是二維的「球面」)。

那麼,三維空間的親吻數是多少呢?參考上圖,若採用「面心立方」或「六方最密堆積」法,每個球都會碰到12個球——上層3個、同一層6個、下層3個,因此三維空間的親吻數最少是12。

kissing
Image Credit: (Left) N.Mori, Public Domain; (Right) Robertwb,CC BY-SA 3.0

牛頓和數學家David Gregory曾經為此爭論,牛頓認為三維空間的親吻數是12,但Gregory認為有其他排列方法可以放得下第13個球。最終牛頓是對的,19世紀有數個不完整的證明支持牛頓,但首個正確證明要到1953年才出現。

1831年,「數學王子」高斯(Carl Friedrich Gauss)證明了如果以規則晶格(lattice)排列,「面心立方」或「六方最密堆積」是最有效率的方法。換言之,如果要證明克卜勒猜想,只需要證明其他排列都不及這兩種排列方法有效率便可以。

實際上沒那麼容易——自高斯的發現後,克卜勒猜想在19世紀內沒有進展。在20世紀開始時,著名數學家希爾伯特(David Hilbert)列出23條有待解決的數學問題,克卜勒猜想亦在其中(為第18條的一部分)。排列方法有無限多種,要證明全部都不及「面心立方」或「六方最密堆積」有效率,絕非易事。

化無限為有限

在1953年,數學家Fejes Tóth László證明了,要判定各種(規則或不規則)排列方式的最高密度這個問題,可以化約成有限的計算,因此理論上能夠以「消除法」證明猜想——只要計算到所有排列方式的最高密度,都不會超過上述近74.05%那個數字,就表示面心立方和六方最密堆積方式最有效率。雖說是「有限的」運算,實際上數量仍然十分龐大,不過Tóth意識到,足夠快的電腦最終令解決這個問題。

Fejes Tóth採用了的數學工具,包括由數學家Georgy Voronoy提出的分割方法,稱為Voronoi圖。這個圖可以用一個簡單故事理解︰設想H市有10個地標,當地政府忽發奇想,要把H市劃分成10區,劃區須滿足以下兩個條件︰

  1. 每區僅有一個地標;
  2. 在每區內任何一處,最接近的地標均在本區。

按照這種劃分方式得出的地圖,就是一個Voronoi圖,而每區均會是個Voronoi多邊形。如果地標的數量、位置改變,所產生的Voronoi圖亦會作出相應改變。Voronoi圖的定義不限於有限的平面,在一個無限大的平面上如果有每限多點,同樣可以劃分出一個Voronoi圖。

Euclidean_Voronoi_diagram_svg
Image Credit: Balu Ertl, CC BY-SA 4.0
Voronoi圖的一個例子。

Fejes Tóth則使用了Voronoi圖的立體版本,把空間以類似方式(按球體中心)劃分成多個的Voronoi立體,並考慮最多13個Voronoi立體體積的加權平均值。他證明了,如果某種方式的加權平均體積大於菱形十二面體(rhombic dodecahedron),就能推論出克卜勒猜想。

原本的克卜勒猜想乃涉及無限多個變數的最佳化問題(optimization problem),而Fejes Tóth的發現能把這問題有可能化約成有限多個變數。不過,Fejes Tóth仍要解釋為何只須考慮13個Voronoi立體——我們已知每個球最多只能同時觸碰12個球,他需要估算第13個球跟中心的距離。1964年,Fejes Tóth提出另一項重要洞見︰他首先提出以電腦解決克卜勒猜想。

與此同時,有其他數學家嘗試從另一途徑攻克猜想。數學家Claude Ambrose Rogers在1958年證明,排列球體的密度上限大約在78%左右,隨後其他數學家把這個數值稍稍拉低,但仍未到達證明克卜勒猜想所需的74.05%。

99%肯定無誤的證明

1992年,數學家Thomas Hales在當時的研究生Samuel Ferguson協助下,結合Fejes Tóth所用的Voronoi立體以及相關的Delaunay三角分割兩種方法,去解決克卜勒猜想。兩人展開一項龐大的研究計劃,以線式規劃方法,對於超過5000種排列球體的方式,尋找一個函數的下限。而要尋找所有下限,需要解決超過10萬條線性規劃問題——每個問題通常有100至200個變數,以及1000到2000個常數。

1996年,Hales在匯報其計劃展進時表示即將見到終點,但需要多一至兩年完成,最終他在1998年宣佈證明了克卜勒猜想,整個證明長達250頁,再加上3GB的數據。證明交到頂尖期刊《數學年鑑》(Annals of Mathematics)的編輯手上,一般審核論文只需要兩三位專家,但審核這篇論文的團隊總共有12人,由Fejes Tóth László的兒子Fejes Tóth Gábor領導。

Halescropped
Photo Credit: Slawekb, CC BY-SA 3.0
Thomas Hales

評審不僅要重新運行Hale的程式碼,還需要檢查5萬行程式碼和數據有沒有錯漏——這並不可能。因此他們僅檢查證明的每一步,以及用作設計程式碼的假設和邏輯,團隊更為此舉辦了一連串研討會來完成。在檢查完後,小Fejes Tóth表示評審團隊有99%肯定證明無誤,他們未有發現錯漏,但由於未能檢查每行程式碼,他們無法絕對肯定證明正確。

最終論文在2005年發表,Hales用上100頁去詳細描述其證明中不涉電腦運算的部份,其後數篇論文則介紹運算內容。

100%形式證明

對Hales來說,99%肯定還不足夠。2003年起,他發起另一項研究計劃,希望移除證明中的不確定性︰構造克卜勒猜想的形式證明,再以電腦驗證。 Hales並非形式證明、電腦驗證等範圍的專家,但開始跟相關領域的專家合作。

所謂的形式證明,是把數學證明從最根本寫起,每一句都是最基本的公理,或者按照推論規則由先前的句子變換得來。形式證明的好處在於每一步均清清楚楚,能夠確保不會犯下大意錯誤,但由於數學研究已經變得非常複雜,正常情況下不會有人使用非常繁複的形式證明。

以電腦協助構造形式證明的話,就可以用電腦自動驗證。不過把由寫給人類看的證明變成形式證明並非易事,過程非常緩慢,而且需要非常細心。在未有電腦的年代,羅素及懷海德合著的數理邏輯經典《數學原理》(Principia Mathematica)就花了數百頁去證明簡單如「1+1=2」的算式(下圖出現於該書第一冊第379頁,留待第二冊才完成證明)。

Principia_Mathematica_54-43
Public Domain

Hales把這項計劃命名為「Flyspeck」,由於當時的軟件無法處理克卜勒猜想般複雜的數學問題,他曾預計整個團隊需要花20年時間才完成。計劃進展得比他想像中快,在2014年8月完成,Hales及21名合作者在2015年1月將論文《克卜勒猜想的形式證明》放上論文預印本存庫arXiv,宣稱證明了猜想。今年5月底,論文正式在期刊《數學論壇Pi》(Forum of Mathematics, Pi)發表。

自1976年數學家Kenneth Appel和Wolfgang Haken透過電腦協助證明四色定理以來,電腦對數學證明的影響越來越大。人類無法處理的運算,交給電腦就可以輕鬆解決,與此同時,人類無法檢視程式碼和大量數據,驗證的工作也開始能交給電腦處理——至於用作驗證的程式、作業系統以至硬件,似乎需要交給其他人處理了。

註︰

  1. 圖片中,面心立方的排列方法為每層「ABCABC…」不斷重複,而六方最密堆積則為「ABABAB…」,兩種堆疊方式可以結合出無限多種排列方法,平均密度相等。

相關文章︰

參考資料︰



原文連結



0 comments:

Post a Comment