計算機科學家馬倫・豪勒（Marijn Heule）始終在數學領域內尋求挑戰。豪勒是卡內基梅隆大學的一名副教授，他因善於使用計算工具解決數學難題而聲名卓著。他 2016 年對 “布林畢氏三元組問題” 的解答因其巨大的證明量而成為了頭條新聞：“200TB 的數學證明前所未有。” 如今，
他正在運用自動化的方式向及其簡明的考拉茲猜想發起攻堅戰
。
（根據某些說法）考拉茲猜想於二十世紀 30 年代由德國數學家羅特哈爾・考拉茲（Lothar Collatz）首次提出，這一數論問題提出了一個生成數列的方法，或者叫演算法：數列的首項是任一正整數；如果該數為偶數，則將其除以 2；如果該數為奇數，則將其乘以 3 再加 1；然後不斷重複這一規則。該猜想稱，這一數列最終一定會得到 1（之後繼續以 4，2，1 的順序迴圈）。
例如，以 5 作為數列首項，會產生 6 個數：
5， 16， 8， 4， 2， 1
以 27 為首項會生成一個 111 項的數列，在到達 1 之前上下波動，最大值達到 9232。
把首項增大到 40，得到的數列就又短了回去：
40， 20， 10， 5， 16， 8， 4， 2， 1
如今，
從 1 到接近 300000000000000000000 為止的正整數都已被計算機驗證符合考拉茲猜想
。
大多數研究者都相信考拉茲猜想是正確的。它吸引了許多數學圈子內外的人士為之前赴後繼，但尚未有人能為它提供證明。二十世紀 80 年代初，匈牙利數學家保羅・厄德斯（Paul Erdős）曾稱：“數學還沒準備好解決這樣的問題。”
“我們想知道究竟是人類還是電腦更善於解決這類問題。”—— 馬倫・豪勒
“他可能是正確的，” 豪勒說。對於豪勒而言，考拉茲猜想的誘惑力與其說是實現突破的可能性，不如說是它能促進自動推理技術的進步。最近，與考拉茲猜想纏鬥了 5 年之久的豪勒和他的合作伙伴 —— 斯科特・阿隆森（Scott Aaronson）和埃姆雷・約爾庫（Emre Yolcu）—— 在預付印平臺 arXiv 上釋出了一篇論文。他們在論文中寫道：“儘管我們沒能成功證明考拉茲猜想，但我們認為，本文的觀點提供了一種十分有趣的新方法。”
“這是次寶貴的失敗，” 阿隆森如此評價到。他是一名計算機科學家，任職於德克薩斯大學奧斯汀分校。說它失敗，是因為他們沒能成功證明考拉茲猜想。說它寶貴，是因為他們在另一種意義上實現了進步：豪勒認為，
從此開始，我們將能夠確認究竟是人類還是計算機更善於證明此類問題
。
把數學譯為計算
對於許多數學問題而言，計算機是指望不上的，因為後者接觸不到歷史上積累的大量數學作品。但電腦也有行的時候。把問題答案可能長什麼樣告訴電腦 —— 給它定個目標並規定好搜尋域 —— 電腦可能就會靠強力找到答案，儘管電腦計算的結果能否算得上對數學經典的有意義的補充尚且存在爭議。傳統觀點認為，只有人類透過概念和觀念發揮的創造力和直覺才能擴充套件數學的範圍，相比之下，透過計算實現的進步往往被鄙稱為工程學。
在某種程度上，
計算機和考拉茲猜想可謂天作之合
。一方面，正如卡內基梅隆大學的邏輯學家和哲學教授傑瑞米・阿維加德（Jeremy Avigad）所言，迭代演算法的概念是計算機科學的基礎，而透過特定規則一步步演算出來的考拉茲數列正是迭代演算法的絕佳示例。同時，程序終止的表達也是計算機科學中的一個常見問題。阿維加德說：“計算機科學家都想知道他們的演算法於何處終止，所謂終止就是說它會重複得到同一個答案。” 豪勒和他的同僚在處理考拉茲猜想（其實就是個終止問題）時就運用了這一技術。
豪勒的專長是使用一種叫做 “SAT 求解器”（或 “可滿足性” 求解器）的計算工具，這一程式可用於確定某一公式或問題在給定約束條件的情況下是否存在解決方案。然而關鍵在於，
在用 SAT 求解器解決數學問題時，需要先把問題轉譯或表示為計算機能夠理解的形式
。並且，就像豪勒的博士生約爾庫所說的：“這一步很重要，非常非常重要。”
目標太遠，但值得打一槍試試
當豪勒最初提出要用 SAT 求解器對付考拉茲猜想時，阿隆森心想：“這打死都行不通。” 但他很快就被勸服了，認為這值得一試，因為豪勒發現了一種很巧妙的方式，能把這個古老的問題轉化為可以用計算工具處理的形式。豪勒注意到，有一群計算機科學家成功地運用 SAT 求解器為一種稱為 “重寫系統” 的抽象計算表達找到了終止性證明。雖然目標距離有點遠，但他還是向阿隆森提議道，如果把考拉茲猜想轉化為一種重寫系統，或許就能得到它的終止性證明（阿隆森曾用小型圖靈機對黎曼假說進行編碼，幫助將其轉化為計算系統）。當晚，阿隆森就把系統設計出來了。對此，他表示 “就像做作業、解趣味題似的”。
阿隆森的系統把考拉茲問題還原為 11 條規則。如果研究人員能為一個以任意順序應用這 11 條規則的模擬系統找到終止性證明的話，也就能夠證實考拉茲猜想了。
豪勒用最頂尖的重寫系統終止性證明工具進行了嘗試，但沒能成功 —— 雖然這是意料之中的事情，但也令人失望。豪勒表示：“這些工具是為了那些能在分秒之內解決的問題而最佳化的，但解決考拉茲問題需要數日以至於數年的連續計算。” 這次失敗激勵豪勒他們隊進一步打磨計算方法，並運用他們自己的工具來把考拉茲猜想轉換為 SAT 問題。
考拉茲猜想的 11 條規則重寫系統示例。來自馬倫・豪勒。
阿隆森發現，如果放棄 11 條規則中的一條，問題解決起來會容易得多 —— 這樣的結果是一個 “類考拉茲系統”，是達成更大目標的試金石。他發起了一項人類對抗電腦的挑戰：
最先運用 10 條規則解決所有子系統者勝
。阿隆森徒手上陣，豪勒則腰佩 SAT 求解器之利劍：他不僅把系統編碼成一個可滿足性問題 —— 他還巧妙地運用了另一個表示層，把系統轉化為以 0 和 1 表達的計算機語言 —— 然後讓他的 SAT 求解器在核心上執行，尋找終止性的證據。
此處的系統遵循以 27 位首項的考拉茲數列 ——27 在對角陣的左上角，1 在右下角。中間有 71 而非 111 步，因為研究者用了一種稍有不同但本質上等同的考拉茲演算法：如果數字是偶數就除以 2，否則就乘以 3 再加 1，再把結果除以 2。來自馬倫・豪勒。
他倆都成功證明該系統按照 10 條規則的可變集具有終止性。有時，對於人類和程式而言，這都是一項微不足道的任務。豪勒的自動化方法最多隻用了 24 小時。阿隆森的純人工方式需要大量腦力勞動，耗時在數小時到一整日之間 —— 他沒能證明這 10 條規則的其中一種組合方式，但他堅信只要再努力努力也就能解出來了。
阿隆森說：“在
最嚴格的字面意義上，我的對手是終結者 —— 或者至少是個終止性定理的證明者。”
與此同時，約爾庫對 SAT 求解器進行了調校，將其校準以更好地適應考拉茲問題。這些手段讓情況大大改觀，10 規則子系統的求解速度大大加快了，執行時間縮短到了秒級。
阿隆森表示：“剩下的最主要的問題是，11 條規則的完整集怎麼處理？如果試著用這個系統跑 11 條規則，那它會無休止地跑下去。我們或許不該對此表示震驚，畢竟這是考拉茲問題。”
在豪勒看來，自動推理領域內的大部分研究都回避了需要大量計算的問題。但基於他此前的突破，他相信這些問題並非無解。有些研究者已經把考拉茲問題轉化成了重寫系統，但是，
只有配合極強的算力大規模運用經過微調的 SAT 求解器才有可能求得證明。
到目前為止，豪勒都是用 5000 個核心（為電腦提供算力的處理單元；消費級電腦通常是 4 核心或 8 核心）來處理考拉茲問題的。作為亞馬遜學者，亞馬遜網路服務對他發出了公開邀請，允許他使用 “實際上毫無限制” 的資源，也就是多大一百萬個核心。但豪勒不太願意用過多的核心。
他說：“我想或多或少地表現出這是個很實際的嘗試。” 不這樣做的話，豪勒覺得他就會浪費資源，辜負信任。“我不需要百分百的信心，但我真的想證明這事有成功的可能。”
促成轉變
“這一自動技術的優美之處在於，你只需要開啟電腦，然後等著就行了
，” 密歇根大學的數學家傑弗裡・拉加利亞斯如是說。他已經和考拉茲猜想纏鬥了差不多 50 年，儼然是其相關知識的守門人，著作等身，還編輯了一本關於考拉茲猜想的題為《終極挑戰》的書。對於拉加利亞斯而言，這個自動化方法讓他想起了普林斯頓的數學家約翰・霍爾頓・康威（John Horton Conway）於 2013 年發表的一篇論文，後者在文中稱，考拉茲問題可能屬於一類難以捉摸的問題，它們是真實的，且具有 “不可判定性”—— 但又不能證明其不可判定。正如康威所言：“…… 甚至對於它不可證明的斷言都是不可證明的，然後，對於其不可證明的斷言是不可證明的這一斷言，亦無法證明，以此迴圈往復。”
拉加利亞斯表示：“如果康威是對的，那不管用自動化的方法還是靠手解，考拉茲猜想都是無法證明的，並且我們永遠不會知道確切的答案。”
目前，可以說是最接近證明考拉茲猜想的人類是 UCLA 的數學家泰倫斯・陶（Terence Tao）。陶在 2019 年證明考拉茲猜想對於 “幾乎” 所有數都 “幾乎” 正確（他的 “幾乎” 基於兩條技術性定義，但也符合英語的日常語義）。
陶相信，
對該猜想的人工證明 —— 瞭解其箇中緣由 —— 比計算機證明在數學的層面上更有意義
。他同時表示：“但是，自動化證明工具如果能解決重大的未解難題的話，就會極大地推動數學家在工作中運用計算機的方式發生革命性的轉變。對於考拉茲猜想這個級別的難題，我們會接納任何洞見。”
然而，透過在考拉茲問題上運用自動化方法，豪勒及其同僚真正追尋的是這樣一種場景：電腦在特定問題上戰勝了人類，或者人類反過來戰勝電腦。“在當前的時間節點上，我們無從知曉究竟是這些技術比人類靠雙手所能做到的事情更強大，還是人類能做到電腦無法完成之事，” 豪勒說，“我們想知道，究竟是人類還是計算機更善於解決此類問題。”
為了得到答案，咱們就拭目以待，看看誰能先證明考拉茲猜想吧。
-End-
