一群數學家終於完成了凱勒的猜想，但不是自己計算，而是教了一批計算機來幫他們解題。
奧特·海因裡希·凱勒（Ott-Heinrich Keller）於90年前提出了凱勒猜想。這個猜想是關於用相同瓷磚覆蓋空間的問題，猜測如果用二維正方形瓷磚覆蓋二維空間，則至少兩個瓷磚必須共享一條邊，以此類推，在使用12維「正方形」瓷磚覆蓋12維空間時，也至少有兩個彼此鄰接的瓷磚。
多年來，數學家不斷進行證明，發現凱勒猜想在某些維度空間是正確的，但在另一些維度空間是錯誤的，截至去年10月，僅有七維空間是否正確仍是個謎。
但現在，數學家終於利用計算機解決了這個問題，並發布了證明過程。這是人類獨創性結合計算機計算能力解決數學難題的最新示例。
解決這個問題的數學家使用了40臺電腦進行計算，30分鐘後，機器就給出了一個單詞的答案：是的。
答案附有很長的證明，解釋了為什麼在凱勒猜想在七維空間是正確的。
神秘的第七維度
不難發現，凱勒的猜想在二維空間中是正確的。拿一張紙，並嘗試用相等大小的正方形覆蓋它，正方形之間沒有間隙且沒有重疊。同樣，該猜想在三維空間中也很容易被證明是正確的。
自1930年凱勒猜想發表以來，1940年，奧斯卡·佩隆（Oskar Perron）證明了猜想對於尺寸為1到6的空間是正確的。但是50多年後，新一代數學家找到了該猜想的第一個反例：Jeffrey Lagarias和Peter Shor在1992年證明了該猜想在10維上是錯誤的。
一個簡單的論證表明，一旦猜想在一個維度上為假，那麼在所有更高維度上就必然為假。因此，唯一未解決的維度是7、8和9。
2002年，麥基證明了凱勒的猜想在第8維也是錯誤的，所以，九維空間也是錯誤的。
剩下的只有七維空間了，它是猜想所在的最高維度，或者是失敗的最低維度。
看的習慣
數十年來，隨著數學家逐漸解決這一問題，他們的方法發生了變化。佩隆用鉛筆和紙算出了前六個維度，但是到1990年代，研究人員已經學會了如何將凱勒猜想轉換成完全不同的形式——一種使他們可以將計算機應用於問題的形式。
凱勒猜想的最初表述是光滑、連續的空間。在該空間內，有無數種方法來放置無限多的瓷磚。但是計算機並不擅長解決涉及無限選擇的問題，要發揮其魔力，需要某種離散的、有限的對象來思考。
1990年，KeresztélyCorrádi和SándorSzabó提出了一個離散的對象。他們證明了可以提出與凱勒猜想等效的關於該對象的問題，因此，如果對這些對象進行證明，則也必須證明凱勒的猜想。這有效地將無窮大的問題簡化為幾個數的算術的簡單問題。
運作方式如下。
假設您想解決二維的凱勒猜想。Corrádi和Szabó提出了一種建立所謂的凱勒圖的方法。
首先，假設桌上有16個骰子，每個骰子的位置都使兩個點的面朝上。（它是兩個點的事實反映了您正在解決二維空間的猜想，而且我們馬上就會知道為什麼它是16個骰子。）
現在使用四種顏色（紅色，綠色，白色或紅色）中的任何一個為每個點著色。
單個骰子上點的位置不可互換：將一個位置表示為x坐標，將另一個位置表示為y坐標。將骰子著色後，如果滿足以下兩個條件，我們將開始在骰子對之間繪製線條或邊緣：骰子在一個位置具有不同顏色的點，在另一個位置具有可以配對的點，比如紅色和綠色形成一對，黑色和白色形成一對。
因此，例如，如果一個骰子有兩個紅點，而另一個骰子有兩個黑點，則它們沒有連接：雖然它們滿足一個位置的標準（不同的顏色），但不滿足另一個位置的標準（配對的顏色）。但是，如果一個邊緣被染成紅黑色，而另一個邊緣被染成綠綠色，則它們是相連的，因為它們在一個位置具有成對的顏色（紅綠色），而在另一位置具有不同的顏色（黑綠色）。
有16種可能的方法來使用四種顏色為兩個點著色（這就是我們使用16個骰子的原因）。將所有16種可能性排列在您面前。連接所有符合規則的骰子。現在來解決關鍵問題：您能否找到四個相互連接的骰子？
這樣完全相連的骰子子集稱為集團。如果找到一個，就證明凱勒的猜想在第二維上是錯誤的。但是您不能，因為它不存在。沒有四個骰子集團的事實意味著凱勒的猜想在第二維度上是正確的。
骰子從字面上看並不是凱勒猜想中要討論的瓷磚，但是您可以將每個骰子視為代表一個瓷磚。將分配給點的顏色視為位於骰子在空間中的坐標。並將邊緣的存在視為兩個骰子如何相對放置的描述。
如果兩個骰子具有完全相同的顏色，則它們表示在空間中處於完全相同位置的圖塊。如果它們沒有共同的顏色，也沒有成對的顏色（一個骰子是黑白，另一個是綠紅色），則它們表示部分重疊的圖塊-記住，不允許在圖塊中使用。如果兩個骰子具有一組成對的顏色，而一組具有相同的顏色（一組是紅黑色，另一組是綠黑色），則它們表示共享一個面的圖塊。
最後，最重要的是，如果它們具有一組成對的顏色，而另一組顏色僅是不同的，即，如果它們通過一條邊連接，則表示骰子表示彼此觸摸但發生了位移的小塊彼此稍微分開，以便他們的臉不完全對齊。這是您真正要調查的條件。通過邊連接的骰子表示未共享面就連接的圖塊-恰好是證明凱勒猜想所需的一種排列方式。
擴大
30年前，Corrádi和Szabó證明了數學家可以通過調整實驗參數，使用此過程來解決凱勒在任何維度上的猜想。為了在三個維度上證明凱勒的猜想，您可以使用216個骰子，在臉上帶有三個點，並可能使用三對顏色（儘管這一點很靈活）。然後，您將尋找八個骰子（2 ），它們之間使用我們之前使用的相同兩個條件相互完全連接。
作為一般規則，要證明維度為n的凱勒猜想，請使用帶有n個點的骰子，並嘗試找到大小為2 n的集團。您可以認為這個集團代表了一種「超級圖塊」（由2n個較小的圖塊組成），可以覆蓋整個n維空間。
因此，如果您可以找到此超級圖塊（其本身不包含任何面部共享圖塊），則可以使用其平移或移位副本使用不共享面孔的圖塊覆蓋整個空間，從而反駁了Keller的猜想。
「如果成功，您可以通過翻譯覆蓋整個領域。沒有共同面孔的街區將延伸到整個瓷磚，」現在在密西根大學工作的拉加裡亞斯說。
那天我辦公室裡工作的是真正的智力天才。就像看韋恩·格雷茨基，就像看NBA總決賽中的勒布朗·詹姆斯一樣。
麥基通過找到256個骰子（2 8）的派系來反駁凱勒在第八維的猜想，因此要回答第七維的凱勒的猜想就需要尋找一個128個骰子（2 7）的派系。找到那個集團，您就證明了凱勒的猜想在第七維度上是錯誤的。另一方面，證明這樣的集團是不存在的，並且您已經證明了這種猜想是正確的。
不幸的是，找到128個骰子團是一個特別棘手的問題。在以前的工作中，研究人員可以利用以下事實：從某種意義上說，維度8和10可以「分解」為易於使用的較低維度的空間。但七維空間不可以。
Lagarias說：「七維不好，因為它是質數，這意味著您無法將其分解為低維事物。因此，別無選擇，只能處理這些圖的全部組合。」
對於無助的人腦來說，尋找大小為128的小集團可能是一項艱巨的任務，但這恰恰是一臺計算機擅長回答的問題，尤其是在您需要一點幫助的情況下。
邏輯語言
要將對派系的搜索變成計算機可以解決的問題，您需要使用命題邏輯來表示問題。這是一種邏輯推理，其中包含一組約束。
假設您和兩個朋友正在計劃一個聚會。你們三個人試圖將來賓列表放在一起，但是您有一些競爭的利益。也許您想邀請Avery或排除Kemba。您的一位共同計劃者想邀請Kemba或Brad或他們兩者都邀請。您的另一位共同計劃者要用斧頭打磨，想要離開Avery或Brad或他們倆。鑑於這些限制，您可能會問：是否有一個滿足所有三方計劃者的客人名單？
用計算機科學的術語來說，這類問題稱為可滿足性問題。您可以通過在這種情況下看起來像這樣的命題公式中描述它來解決它，其中字母A，K和B代表潛在客人：（A OR NOT K）AND（K OR B）AND（NO A是否B）。
計算機通過為每個變量插入0或1來評估此公式。0表示變量為false或已關閉，而1表示變量為true或已打開。因此，如果您為「A」輸入0，則表示不邀請Avery，而為1則表示邀請她。有很多方法可以為這個簡單的公式分配1和0（或建立來賓列表），並且在運行它們之後，計算機可能會得出結論，即無法滿足所有競爭需求。但是，在這種情況下，有兩種分配給所有人的1和0的方法：A = 1，K = 1，B = 0（意味著邀請Avery和Kemba），A = 0，K = 0，B = 1 （意味著邀請Brad）。
像這樣解決命題邏輯語句的電腦程式稱為SAT求解器，其中「 SAT」代表「可滿足性」。它探索變量的每種組合併產生一個單詞的答案：是的，有一種方法可以滿足公式，否則的話，沒有。
隱藏的效率
Mackey回憶起在他眼中該項目真正成立的那一天。他站在卡內基梅隆大學辦公室的黑板前，與兩位合著者Heule和Brakensiek討論了這個問題，當時Heule提出了一種結構化搜索的方法，以便可以合理地完成搜索。
您可以通過多種方式來增強對特定凱勒圖的搜索。想像一下，您桌上有很多骰子，而您正試圖以符合凱勒圖規則的方式排列其中的128個。也許您正確地排列了其中的12個模具，但是找不到增加下一個模具的方法。到那時，您可以排除128個骰子的所有配置，這些配置涉及12個瓷磚的不可行的初始配置。
效率的另一種形式涉及對稱性。當對象是對稱的時，我們認為它們在某種意義上是相同的。這種相同性使您可以通過研究對象的一部分來了解整個對象：瞥一下一半的人臉，然後可以重建整個外觀。