福建
數學，是人類文明中最古老的獨奏藝術。一個人、一張紙、一根筆，再加幾年心血，這幾乎是數學家工作方式的終極標準像。
陶哲軒想把這張底牌翻過來。
這位2006年菲爾茲獎得主、UCLA教授，被公認為當代最全能的數學家之一，他的研究橫跨素數分布、流體動力學、核磁共振成像算法等十余個領域。但如今，讓陶哲軒花費最多精力的，不是某個具體的數學定理，而是一個更根本的問題：怎樣讓數學這件事本身，變得更快、更可靠、更開放？
Lean：讓計算機當數學的裁判
2023年10月，陶哲軒在社交媒體上宣布，他決定認真學習Lean，這是一款允許用戶以代碼形式書寫數學證明、并由計算機自動驗證正確性的形式化工具。他的選擇在數學界引發了不小的轟動，因為Lean一向以入門門檻極高著稱，許多職業數學家對其望而卻步。
當時 72 歲的保羅·埃爾德什和 10 歲的陶哲軒。 比利·格雷斯·陶
學習的過程充滿了意外。陶哲軒先挑選了一道關于麥克勞林不等式的問題，按慣例寫出了一份10頁的手寫證明，然后開始嘗試把它翻譯成Lean代碼。他以為一周能完成，結果花了將近一個月。
麻煩出在"顯然"二字上。手寫證明中，他信手寫下"三個數若均大于1，其和自然至少為3"，但Lean不接受"自然"這個詞。他必須在Mathlib數學庫里找到對應的引理，一步步補全邏輯鏈條。更繁瑣的是，數字"3"在人類數學語言里可以同時是整數、自然數和實數，無需說明；但Lean要求每次都明確指定類型，否則代碼直接報錯。
這種"編譯錯誤"的體驗，恰好印證了陶哲軒十年前的一個預言。2014年，他曾在一次對話中預測：未來數學家或許不再用LaTeX寫論文，而是用某種可被計算機理解的形式語言，"偶爾會有編譯錯誤——計算機無法理解你是怎么從這一步推出下一步的"。當時，臺下的人覺得這個想法比"我們生活在模擬宇宙里"還要荒誕。
如今，那個"編譯錯誤"真的出現在了他自己的屏幕上。
2200萬個問題，一個月解決了99%
塞繆爾·貝拉斯科/廣達雜志
完成麥克勞林不等式的Lean形式化后，陶哲軒在網絡社區發了一條評論，語氣幾乎是道歉式的："順便說一下，我已經成功實現了這個結果，代碼寫得相當糟糕。"但就是這條評論，讓他正式成為Lean社區的貢獻者。
真正的大動作發生在2024年9月25日。陶哲軒在個人博客宣布啟動"方程理論"項目。他的想法是：把所有運算次數恰好為四次的代數定律放在一起，梳理它們之間的邏輯蘊含關系，畫出一張完整的地圖。
這意味著4694條定律，以及兩兩之間約2200萬個需要驗證的邏輯關系。
項目啟動僅48小時，陶哲軒就在博客上寫道："進展速度遠遠超出了我的預期，我原以為會像PFR項目那樣花三周，但這次的速度簡直瘋狂。"
來自全球各地的數學家、程序員、博士生和業余愛好者涌入項目頻道。志愿者們用Python腳本批量測試，用自動化定理證明器掃蕩簡單情形，再由人類處理最頑固的邊緣案例。每個貢獻都以Lean代碼的形式提交，系統自動驗證正確性，無需陶哲軒逐一審閱。
這正是他苦苦尋找的結構：大問題分解成模塊，機器負責驗證，人類負責洞察，分工清晰，無需中央審核員。
一個月內，2200萬個問題縮減至238個。項目最終還衍生出了"巖漿上同調"這一此前從未被描述過的數學構造，讓專攻上同調理論的數學家約翰·貝茲也坦言從未見過。貝茲原本對這個項目評價不高，稱其"在我看來純屬浪費時間"，但這個意外發現讓他無話可說。
陶哲軒的結論很清晰：這不是一次對已知答案的整理歸檔，而是真正發現了新東西。
他的更大野心，是讓數學走上物理學曾經走過的路，從一門依賴少數孤獨天才的手藝，演變為一個擁有實驗分支的體系，人工智能處理大量細碎子問題，形式化工具提供絕對可靠的驗證，人類數學家專注于那些機器還無法觸及的深處。
在陶哲軒看來，Lean不是數學家的威脅，而是數學得以擴張邊界的新工具。數學的未來，可能不再是一個天才，一張紙，和幾年孤獨。
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
