★置頂zzllrr小樂公眾號，追蹤《小樂數學科普》系列報道，進入數學家們的深度思維空間！

曾參與貢獻研究“移動沙發問題”的數學家丹?羅米克（Dan Romik）近期參加了斯坦福大學的FMS數學未來研討會，本文為其觀后感，與君分享其心得。

圖源： danromik.com

作者：丹?羅米克（Dan Romik）2026-5-8

譯者：zzllrr小樂（數學科普公眾號）2026-6-6

求喜歡

我在上周五（5月1日）參加了斯坦福大學舉辦的數學未來研討會第一天的活動。第二天未能到場，但在YouTube上觀看了全部講座（不幸的是，所有視頻現已全部下架，請移步B站，譯者注）。這是一場星光熠熠、令人興奮的盛會，匯聚了眾多數學家與人工智能行業從業者，大家共同關心基礎數學研究將走向何方。

最近一年，AI 在數學領域的能力突飛猛進，達到了僅僅 1–2 年前（有些方向甚至 8–9 個月前）還遙不可及的水平，現場氣氛熱烈而振奮。與會者是一群極為出色的人：聰明、嚴謹、深思熟慮，熱愛數學，并對AI以（總體上）積極的方式徹底改變數學研究充滿期待。

一、核心印象
1. Lean已成絕對主流

Lean作為數學形式化工具生態里的 “巨無霸” 崛起，其實不算全新現象 ——1–2年前，我身邊不少合作者就已經頻繁討論 Lean。但2026年注定會被銘記：幾乎所有人都開始討論Lean，它正式成為形式化領域的事實標準。

Lean的指數級流行，很大程度上歸功于多家AI公司將其作為關鍵基礎設施，用于開發能進行高水平數學推理的大模型；同時，這些AI公司近期推出了一系列極強的自動形式化工具，如 Aristotle、Gauss、AxiomProver。

這些進展是會議討論的核心話題，多位演講者（萊昂納多?德?莫拉Leonardo de Moura、克拉克?巴雷特Clark Barrett、凱文?巴扎德Kevin Buzzard、瑪麗娜?維亞佐夫斯卡Maryna Viazovska）都詳細介紹了與Lean相關的項目、工具，以及人類與AI輔助形式化最近達成的里程碑。

2. 這更像一場AI大會，而非數學大會

這場會議名義上是 “數學的未來”，但大多數講者并沒有真正聚焦數學本身。他們大量拋出數學術語 —— 領域、定理、猜想等等 —— 卻很少解釋術語背后的數學實質。絕大多數報告的重心都是AI、AI工具，以及這些工具如何真正用于數學研究；數學本身反而有點像事后附帶的東西。

舉個小例子：第二天開場，組織者賈里德?杜格爾?利克曼（Jared Duker Lichtman）在引言里簡短提到了 “所謂的埃爾德什1196問題”，作為AI助力研究突破的例子，但完全沒解釋這個問題是什么。

（我并非批評他，他是非常認真的數學家，對工作充滿熱情；只是在簡短開場里根本沒時間講數學細節，其他演講者也一樣 —— 不是不關心細節，而是議程太滿，必須優先講AI主題。）

不過也有例外：塞巴斯蒂安?布貝克（Sébastien Bubeck）與瑪麗娜?維亞佐夫斯卡（Maryna Viazovska）的報告花了大量篇幅真正講解他們用AI和Lean做出的有趣數學。至少在我看來，這非常受歡迎，也讓報告更有價值。

3. 技術細節遠超預期

我原本以為，絕大多數報告都會比較 “空泛”，只談宏觀、大膽模糊的未來預測，沒多少技術干貨。

確實有少量空話，但整體而言，我喜出望外（而且我最初的預測錯了）：演講者們給出了大量具體、詳實、帶文獻引用的技術細節。他們深耕AI與數學，樂于分享最近工作里的經驗技巧。我說的 “最近” 真的很近：比如桑吉夫?阿羅拉（Sanjeev Arora）就在報告里提到了他幾天前剛完成的亮眼成果。

二、部分報告簡評
1. 萊昂納多?德?莫拉（Leonardo de Moura）

Lean創始人的概述。內容極富技術深度，非常精彩。

2. 亞當?布朗（Adam Brown）

全場最 “好玩” 的報告。風趣、表達流暢，梳理了工業界讓AI攻克困難數學問題的進展。

他的歷史回顧從2019年開始：當時AI做數學大致相當于幼兒園水平；一路講到今天，AI已經在國際數學奧林匹克（IMO）上達到接近超人水平。他對未來趨勢做出了理性且樂觀的推斷。

3. 塞巴斯蒂安?布貝克（Sébastien Bubeck）

我最喜歡的報告之一，很大原因就是數學細節非常豐富。他詳細分享了過去一年里5個真實的、AI輔助完成的數學研究案例。

4. 瑪麗娜?維亞佐夫斯卡（Maryna Viazovska）

我非常喜歡的另一場報告，因為數學含量極高，圍繞她在8維和24維球體堆積問題上的開創性工作，詳見：

這個領域我也很關心（我很高興她甚至引用了我 2023年的一篇小文章）。演講者優秀、內容極具開創性、鼓舞人心，夫復何求？

5. 桑吉夫?阿羅拉（Sanjeev Arora）

內容扎實、信息密度極高，詳細介紹了他與合作者設計的AI解題器高級框架。這些框架讓大模型在國際數學奧林匹克（IMO）和First Proof等研究級挑戰中取得頂尖成績。詳見

6. 陶哲軒（Terry Tao）

報告題目：《新的數學工作流》，詳見。

他聚焦于：在 “證明富足” 時代，數學家的未來會怎樣。強大AI讓證明變得容易，但數學家珍視的另一些目標未必更容易實現。在這樣的世界里，數學研究的整套基礎設施（期刊、審稿、講座傳播）都會失衡。陶哲軒深入討論了數學家需要如何適應這一新現實。

7. 謝爾蓋?古科夫（Sergei Gukov）

我同樣很喜歡。他聚焦一類特定的AI+數學研究：用深度強化學習算法攻克極難的數學問題。

他有趣地回顧了強化學習的歷史：許多基礎算法最初是為了讓電腦高水平玩雅達利電子游戲而開發。如今，幾乎同樣的算法支撐著AlphaFold、自動駕駛，以及古科夫用來攻堅難題的AI流程，非常鼓舞人心。

我也很欣賞他做的研究是硬核機器學習思路，和目前很多人走的大模型路線不太一樣。

三、總結
值得關注的引言

• “我們還沒看到 AI 帶來的重大突破，但它即將到來，很有可能就在今年。”

  —— 塞巴斯蒂安?布貝克

• “數學是一張超圖?！?/strong>

  —— 邁克爾?弗里德曼（全場我最喜歡的一句話）

• 詳見