電腦能從事數學工作嗎？ 聽到這個問題的時候，你的第一個反應必定是「可以」 吧，畢竟我們只需在 Google 搜尋「1 + 1」，它就會自動顯 示答案「2」。事實上最初發明電腦的目的真的是為了計算； 英文名稱「computer」（計算機）來自字根「compute」（計 算），在沒有電腦的年代指從事計算工作的計算員。透過微 軟 Excel 或 Python 及 C++ 等程式語言，電腦的確可以迅 速地進行複雜的計算工作，所需時間遠比人類短，可是數學 家感興趣的卻是另一種「數學」：寫數學證明。 考慮以下的問題：任意選一個數字作起點，如果這個 數字是雙數，把它除以二；如果是單數，先將數字乘以三， 再加上一。重覆以上步驟，到底數列最終是不是永遠都會 得出 1？這個看似簡單的問題就是考拉茲猜想 （Collatz Conjecture），但現在還沒有人能夠解答。電腦可以檢查一 個任意大的數字最後會得出甚麼（假設有足夠的時間和計 算能力給電腦去計算），但這與要證明任何一個數字最後都 會得出 1 還有一段距離，要解決這個問題肯定需要一些新 方法，但擁有電腦的我們卻一籌莫展。 那有甚麼問題是我們可以用電腦解決的呢？例如這道： 試找出圖一四邊形中所示的角度。我們都懂得用「圓內接四 邊形外角」這條定理去證明兩者相等。那麼，電腦又懂得這 樣做嗎？如果我們教曉電腦用這條定理的話，那沒問題；然 而，電腦又能不能解開人類還沒解開的數學問題呢？ 嗯，也許可以吧。但我們要先給電腦上一課數學課。 第一個任務是把我們現在知道的數學知識形式化 （formalize）。近年這方面有一個在 2013 年由微軟工程 師 Leonardo de Moura 開發，叫 Lean 的軟件 [1]。自 Lean 問世而來很多大學程度的基本數學知識都已經被形 式化（以電腦能理解的形式改寫），現時多方仍在努力豐富 Lean 的數學知識庫，令其可以引用更多數學知識和定理。 網上有一個叫《The Natural Number》的遊戲讓玩家 可以體驗把數學知識形式化的過程 [2]。在遊戲中你可以嘗 試教電腦數算、基本加法和乘法，但在這之前你需要告訴電 腦例如「x的下一個自然數是x + 1」等最基本的知識。 當然，現時數學家研究的課題遠比數算難，但我們可以 對 Lean 輸入更多更複雜的定理讓其發揮更多。2020 年 末，數學家 Peter Scholze 對自己寫的一部分證明有所懷 疑；他是菲爾茲獎得主（註一），主要研究以極其專門和抽 象見稱的算術幾何。事源他和 Dustin Clausen 幾年前證 明了一條對該範疇非常重要的定理，但他對當中一些細節 並不確定。如果要檢查這份證明，還有比電腦更適合的「人 選」嗎？於是他們展開了液體張量實驗（Liquid Tensor Experiment），嘗試用 Lean 來驗證證明 [3]。 六個月後，Scholze 和 Clausen 得到了正面的結果： 儘管他們的證明有幾個小漏洞，但大致正確。實驗中，以 Johan Commelin 貢獻最多的一組數學家在理解 Scholze 和 Clausen 寫的證明後，以電腦明白的語言「教」電腦讀懂 證明，使其能驗證證明 [4]。 因此電腦的確有能力參與數學研究並作出貢獻，但有一 個細節必須注意：上文提到的 Lean 只能輔助我們檢查證 明，但它並不能憑空寫出證明。由於電腦不能讀懂用我們文 字寫的證明，因此即使要驗證也要靠我們把證明形式化。電 腦亦肯定不能自行創造出這類極為複雜的證明，儘管 Lean 能洞察到證明中可以作出簡化的地方，並在這些對我們來 說未必太明顯的位置精簡證明，但總的來說它還是僅僅順 著 Scholze 和 Clausen 所寫的論證來檢查證明是否邏輯 上正確。 這延伸出另一方面的問題：雖然數學研究大多都是關於 證明敘述，但當中亦涉及如何找「正確」的敘述來證明。當 數學家不能證明某個敘述時，他們往往會將敘述簡化，先證 明比較簡單但仍然「有用」的版本。然而判別何謂「正確」和 「有用」並不像分辨對錯那樣非黑即白，這需要用到更高階 的思維，譬如我們現在並不能證明孿生質數猜想（其敘述為 「前後兩者相差為 2 的質數對有無限多對」），但是我們卻 能退而求其次，證明前後兩者相差少於或等於 246 的質數 對有無限多對 [5]，這個安慰獎對我們來說還是有用的。 把猜想簡化成仍然有用的敘述對人類來說並不難，但 對電腦來說可能一點也不容易。數學家正嘗試用機器學習 （machine learning）研究一個問題到底何謂「簡單」和「困 難」，例如 Timothy Gowers 最近就正著手處理這個問題 [6]。一旦有所突破，也許我們就能讓電腦自行找出一些「不 太困難」但仍對數學家有用的敘述來證明。 對於要用上一些「捷徑」或「提示」，或是要建構特別例 子才能解決的數學問題，電腦還是鞭長莫及。這些問題通常 很難透過蠻力搜尋（brute force searching）以窮舉的方 式解決，但當你知道所需的方法後一切卻會迎刃而解。如果 沒有人對電腦輸入這個「提示」，現今的電腦是不能自己洞 察到的；儘管是數學家，這種直覺也是讀書和實戰多年後的 成果。 圖一 圓內接四邊形外角
RkJQdWJsaXNoZXIy NDk5Njg=