數學接力：陶哲軒、直覺與 AI 的協作展示
如果數學界有搖滾巨星，那一定是保羅·艾狄胥（Paul Erdős）。
這位匈牙利數學家的一生就像一場永無止境的巡迴演出。他沒有家，沒有固定工作，全部家當都在一個破舊的皮箱裡。他會突然出現在某個數學家的家門口，敲敲門說：「我的大腦敞開了（My brain is open）。」然後住下來，和對方沒日沒夜地解題，直到靈感耗盡，再前往下一站。
艾狄胥是前網際網路時代的「人肉伺服器」。他連結了全世界的數學家，把問題從一個大腦傳遞到另一個大腦。他深知一件事：數學太難了，難到一個人無法獨自面對。
今天的艾狄胥不再需要搭飛機，也不用睡在別人的沙發上。他的大腦已經數位化，變成了一個網站——艾狄胥問題網（Erdos Problem Website）。而最近，這個數位大腦迎來了一位新夥伴，一位不知疲倦、運算速度以光速計的協作者：AI。
菲爾茲獎得主陶哲軒（Terence Tao）最近在該網站上的一場「人機接力賽」，向我們展示數學研究的未來型態。這不再是孤獨天才的獨角戲，而是一場由人類直覺、數位歸檔與 AI 驗證共同編織的「超級大腦」運算。
數位化的 Erdős 大腦
在深入那場精彩的接力賽之前，我們得先談談這個比賽場地：erdosproblems.com。
這個由數學家 Thomas Bloom 維護的網站，不僅僅是一個題庫。它是艾狄胥遺留問題的「數位分身」。艾狄胥一生提出了數千個猜想，許多都懸賞了獎金（從 25 美元到數千美元不等）。過去，這些問題散落在信紙、黑板角落，或是老一輩數學家的記憶裡，隨著時間流逝而模糊。
艾狄胥問題網將這些問題結構化、標籤化，並賦予每個問題一個獨一無二的編號。這看似簡單的整理，實則為 AI 的介入創造了完美的「介面」。AI 也許不懂什麼是「數學之美」，但它非常擅長處理結構化的數據和明確定義的邏輯挑戰。
Bloom 的願景很清晰：他希望將數學變成一個「多人連線遊戲」。而現在，這個遊戲的玩家名單裡，多了矽基生命的名字。
#367 號問題的人機接力賽
讓我們把鏡頭轉到最近發生的 艾狄胥問題 #367。這是一個關於數論的技術性問題，但解決它的過程，比問題本身更具啟發性。這不是某個天才靈光一閃的瞬間，而是一次完美的「分散式運算」。
第一棒：人類的直覺突破
故事始於 11 月 20 日。數學家 Wouter van Doorn 對這個問題的第二部分提出了一個反證（disproof）。但他遇到了一個障礙：他的論證依賴於一個特定的「同餘恆等式」（congruence identity）。
Wouter 擁有數學家最寶貴的資產——直覺（Vibe）。他「感覺」這個恆等式是對的，但他沒有時間或工具去立刻驗證它。於是他把球傳了出來，在論壇上寫道：「我確信這裡有人能驗證這個恆等式確實成立...」
在過去，這句話可能會被淹沒在論壇的深處，等待某個有閒情逸致的研究生幾個月後看到。但這次不同。
第二棒：AI 的光速驗證
陶哲軒接到了球。但他沒有拿起紙筆開始計算。身為當今最頂尖的數學家，他選擇扮演「指揮官」的角色。
他將這個恆等式丟給了 Google 的 AI 模型 Gemini Deepthink。
結果令人震驚。原本可能需要人類數學家耗費數小時甚至數天進行繁瑣運算的過程，AI 在 10 分鐘內就完成了。Gemini Deepthink 不僅確認了恆等式成立，還給出了一個完整的證明。
有趣的是，AI 採取了一種「殺雞用牛刀」的策略。它使用了一種相當高深的 p-adic 代數數論方法來解決這個相對初等的問題。這就像是用核彈來打蚊子，但它有效。
陶哲軒隨後介入，發揮了人類的「審美」與「轉譯」能力。他花了大約半小時，將 AI 那個過於複雜的證明，改寫成一個更優雅、更初等的人類可讀版本，並發布在網站上。
第三棒：形式化的最後一哩路
到這裡，問題似乎解決了。但在數學的最高殿堂，光有證明還不夠，我們需要「絕對的確定性」。
兩天後，另一位數學家 Boris Alexeev 接手了最後一棒。他使用了 Harmonic 公司開發的 AI 工具 Aristotle，將陶哲軒整理好的證明，轉化為 Lean 語言。
Lean 是一種「互動式定理證明工具」，它能將數學證明變成電腦可以驗證的程式碼。這通常是數學研究中最枯燥、最耗時的步驟，被稱為「形式化」（Formalization）。許多數學家因為討厭寫程式碼而對此卻步。
但在 Aristotle 的協助下，Boris 僅用了兩三個小時就完成了形式化工作。為了確保萬無一失，防止 AI 產生幻覺或鑽漏洞（AI exploits），Boris 最後親自手動確認了最終的陳述（Final Statement）。
至此，艾狄胥問題 #367 的這部分（第二部分的否證）被徹底攻克。雖然這不代表整個 #367 號問題被完全解決，但針對這個特定子問題的攻防戰，從直覺猜想，到運算驗證，再到程式碼形式化，整個過程行雲流水。
從「獨行俠」到「指揮官」
這個案例標誌著數學家角色的根本轉變。
過去，數學家是孤獨的登山者，必須獨自背負所有的裝備（計算、文獻、證明細節）爬上頂峰。現在，他們更像是指揮官。他們負責制定戰略（提出猜想、定義問題），然後指派 AI 專員去執行戰術任務：
- 文獻搜索（Literature Search）： 雖然在這個案例中，陶哲軒提到 AI 在文獻搜索上還不夠完美（它搞混了 #366 和 #367），但這只是時間問題。
- 運算驗證（Computation）： 像 Gemini 處理繁瑣的代數運算。
- 形式化（Formalization）： 像 Aristotle 將證明轉化為 Lean 代碼。
陶哲軒將這種新模式稱為 "Vibe Formalizing"（直覺形式化）。這是一個強大的概念。過去，從「直覺」（我覺得這是對的）到「形式化證明」（這是 Lean 代碼）之間，有一道巨大的鴻溝。這道鴻溝阻礙了無數好點子的實現。
現在，AI 架起了這座橋樑。數學家可以專注於產生高品質的「Vibe」，而將繁瑣的「Formalizing」交給 AI。這將極大降低形式化驗證的門檻，讓數學研究進入一個「零信任、全驗證」的新時代。
敬請免費訂閱、贊助本電子報
Mosky 從零開始 AI 寫程式
折扣碼：FOXAI
課程連結和限時優惠網址：https://pse.is/8dqy89
折扣金額：$250
