★置頂zzllrr小樂公眾號，追蹤《小樂數學科普》系列報道！

6月2日《AI與數學萊頓宣言》初版正式發布之后，陶哲軒做了積極評價（詳見本文引言），除呼吁同行研讀和酌情簽署（截至北京時間2026.6.4，已有1300+人簽署）之外，同時強調參與公共議題討論的重要性，并推薦大家參閱前期（今年3月份）萊頓宣言初稿。

譯者申明：感謝各位公眾號讀者留言建議，譯文（尤其長篇）僅供參考，一切以原文原意為準（在很可能出現爭議之處，我會盡可能引用原始內容供對比閱讀，原文參考鏈接會始終在底部完整提供，如有個人或平臺轉載，請不要刪除原作者提供的原始文獻鏈接）

2025年9月在荷蘭萊頓大學洛倫茲中心舉辦的研討會

前排中間兩位為參與萊頓宣言撰寫的工作組成員：

Rodrigo Ochigame、Mateja Jamnik

圖源：universiteitleiden.nl

作者：

約翰?科姆蘭（Johan Commelin，荷蘭烏得勒支大學助理教授，Mathlib Initiative項目負責人，Lean定理證明器數學庫Mathlib維護者之一）

馬特亞·亞姆尼克（Mateja Jamnik，劍橋大學計算機科學系教授 *）

Rodrigo Ochigame（萊頓大學助理教授，人類學家和歷史學家 *）

蘭尼·塔爾曼（Lenny Taelman，阿姆斯特丹大學代數幾何教授）

阿克沙伊·文卡泰什 (Akshay Venkatesh，IAS普林斯頓高等研究院教授，菲爾茲獎得主) 2026-5-8

上述標*作者為萊頓宣言工作組成員。

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

求喜歡

引言

作者：陶哲軒 mathstodon.xyz/@tao

日期：2026.6.2

mathstodon.xyz/@tao/116681024360293007

最終文稿經過過去數月的反復打磨完善，成品令我印象深刻，我對此完全贊同、鼎力支持。宣言中的諸多觀點在其他文獻中也曾被提及，比如我本人的寫作與談話就多次探討過其中部分內容，但把所有主張系統凝練在一份文件里，便產生了極高的額外價值。我呼吁業內所有同行研讀這份宣言，并酌情簽署（我本人已簽署完畢 https://leidendeclaration.ai/signatories?q=Terence+Tao ） 。

宣言里各項建議都十分中肯，在此我著重強調參與公共議題討論這一條。現實中一個普遍問題是：一線數學家往往埋頭鉆研解題等技術性工作，疏于向大眾闡釋研究的內在意義。

So long as we had a near-monopoly on the ability to accomplish these tasks, we could have this luxury of only discussing "safe" technical topics in public; but in the new era of "proof abundance", it is increasingly important that we also debate the "soft" aspects of our field, such as our goals and values.

過去，攻克高深數學問題的能力近乎由數學家群體壟斷，我們尚能只在公開場合談論“穩妥”的純技術內容；但在“證明唾手可得”的全新時代，學界必須主動探討學科“軟”性議題，例如科研目標與價值取向，這件事變得愈發關鍵。

另可參閱科姆蘭（Commelin）等人今年3月發布于 arXiv 的萊頓宣言（文獻鏈接：https://arxiv.org/abs/2603.24914 ）及紐約時報文章 https://www.nytimes.com/2026/06/02/science/ai-mathematics-leiden-declaration.html 。

在AI時代塑造數學的未來

作者：約翰?科姆蘭（Johan Commelin）、瑪泰婭?亞姆尼克（Mateja Jamnik）、羅德里戈?奧奇加梅（Rodrigo Ochigame）、倫尼?泰爾曼（Lenny Taelman）、阿克沙伊?文卡特什（Akshay Venkatesh）

日期：2026.5.8（第2版）2026.3.26（第1版）

人工智能正以前所未有的速度與規模重塑數學學科，倒逼學界重新審視這門學科賴以立足的知識根基。依托 20 世紀關于可計算性與數學基礎的理論探索，當代人工智能早已跳出數值運算與窮舉核驗的范疇，發展出成熟的數學推演能力。AI 相關能力的飛速落地，催生了大量亟待整個數學界共同解決的新問題。

這場變革依托多元化、技術路線各不相同的人工智能方案全面鋪開：越來越多數學家開始使用Lean 證明助手 1（基于傳統符號邏輯的形式化驗證系統），在協作式數學形式化項目中完成復雜定理的編碼與證明核驗 [1]。深度神經網絡 + 符號結合的系統（如 AlphaProof）已達到IMO國際數學奧賽獎牌級解題水準；純大語言模型類人工智能，也逐步轉型成為數學科研輔助工具 [7]。盡管上述技術在實現路徑與底層理念上存在顯著差異，但它們共同具備改寫數學知識發現、驗證與體系化方式的潛力。

圖源：荷蘭萊頓大學

本文五位作者于2025年9月在荷蘭萊頓洛倫茨科學中心主辦了一場題為《機械化與數學研究》的專題研討會 2，匯聚數學家、計算機科學家、科學哲學家與科學史家，跳出短期技術細節，從宏觀視角研討 AI 帶來的深層變革。會議研討氛圍熱烈，所有參會學者都意識到這場變革事關數學的長遠走向。本文立足作者參會心得，提煉關鍵結論，旨在推動數學界開展必要討論：既不盲目神化現有科研范式，也不默認技術革新天然具備正向價值。

術語釋義

• 形式化證明（formal proofs）

  可由 Lean、Rocq、Isabelle 等機器系統自動核驗的數學證明；
  

• 形式化證明庫（libraries of formal proofs）

  經過機器核驗的數學命題與證明共享知識庫，典型項目為 Mathlib、AFP（Archive of Formal Proofs） 形式化證明檔案庫 3。

• 人工智能（AI）

  囊括符號派（ symbolic ）與神經網絡（ neural） 兩大技術路線，大語言模型亦在定義范疇內；各類工具實現路徑不同，但均可助力數學推理自動化與新結論發掘。

• 數學共同體（mathematical community）

  定義寬泛，包含高校與產業界科研人員、在讀學生、獨立數學貢獻者。

下文圍繞研討會凝練出五大核心議題：數學的內在價值、科研實操范式、數學教育、前沿技術落地、智能系統衍生的倫理治理，逐一梳理關鍵問題與學界落地建議。AI 時代的數學未來絕非被動降臨，而應由全球數學共同體攜手共同塑造。

一、數學的內在價值

本次研討會上各方觀點分歧鮮明：一部分研究者歡欣鼓舞，期待計算機接管繁瑣的證明撰寫工作；另一部分學者則認為，推導與書寫證明的過程本身就是數學技藝不可或缺的組成部分。有人主張形式化證明全面融入科研與教學，也有學者堅決反對該導向。種種分歧，折射出數學界宣稱的價值理念與現實科研實踐之間持續存在的內在矛盾。

這種廣譜性反映了基礎價值觀的多元性，數學的價值根植于兼具人文屬性與科學屬性的獨特學科傳承，因此切勿用單一標簽概括全體數學家的價值取向。

但當下的時代要求我們全面、審慎地審視數學價值的復雜內涵。手段會反過來重塑目的（Means reshape ends）：新技術的強大能力，有可能主導何為重要的數學研究，而非服務于數學本身的核心訴求。數學證明片段的自動化，會改變研究者的選題方向與受推崇的證明范式；依托形式化與機器驗證提升嚴謹度，也將改寫論文發表的評判標準。

And while some parts of the community may benefit from the increased commercial interest in mathematical AI, we must remain conscious of how such interest can reorient the field’s internal compass. Otherwise, our discipline risks losing its intellectual autonomy.

盡管部分學者能從資本對數學人工智能的追捧中獲益，但我們必須警惕商業導向扭曲學科內在發展方向，否則數學或將喪失學術自主性。

上述問題由來已久，只因近年技術迭代的規模與速度，使其迫在眉睫。解決方案并無捷徑，但研討會達成一條廣泛共識：

Ensure that the development and adoption of new technologies in mathematics remain firmly rooted in our own epistemic and aesthetic values—diverse as they are—rather than driven by the internal logic of those technologies or the commercial interests of their developers.

數學新技術的研發與落地，必須牢牢立足數學多元的認知與審美價值，不能受制于技術自身邏輯或研發方的商業利益。

各國數學學會、高校數學系與科研工作者，都應積極參與相關研討，攜手規劃學科的發展道路。

二、數學科研范式的未來走向

現階段我們尚無法預判：AI 系統能否、何時、在何種程度上超越人類完成標準化數學任務（例如生成完整形式化證明）。但洛倫茨中心的研討結論明確：學界必須即刻直面該假設落地后的連鎖影響。

整個共同體需要共同思考：一旦 AI 可批量生成形式證明，何謂數學新發現？是產出一份機器可驗證的形式證明、提出關鍵性猜想、構建具備解釋力的論證，還是其他成果？人類數學直覺的定位將如何變化？在科研模式劇變的環境下，我們該如何培養新一代數學家？據此提煉行動方向：

研究者應攜手學生共同探討：當機器承接當前數學研究大量日常工作后，人類與數學之間的關系將如何重塑。

三、數學教學與人才培養

如同手持計算器和舊時代技術普及帶來的變革，人工智能將顛覆數學基礎能力的定義，進而改寫數學教育的本質目標。當計算機可以規模化完成標準化數學演算，人類數學素養的核心不再是手動演算，而是判斷任務類型、厘清運算目的、串聯具體問題與宏觀研究方向，以及形成賦予數學意義的判斷力與洞察力。

該變革同步帶來考核難題：在 AI 可輕松完成常規計算與證明的環境下，如何通過考試測評學生真實的理解與能力？為提升數學共同體應對未來變局的韌性，學界建議：

修訂本碩階段數學培養方案，擴充教學能力邊界，重點培養學生提出問題、學術交流、辨析邏輯論證優劣的綜合素養.

四、面向數學的人工智能技術建設

如何讓數學家深度參與數學專用 AI 工具研發，掌握技術發展話語權？

形式化證明開源庫已率先走出一條可行路徑：成功吸納海量職業與業余數學家共建。為保障這類知識庫長期健康發展、貼合學術價值觀，必須借鑒開源項目成敗經驗完善治理規則。

In particular, we must establish clear licensing frameworks and contributor norms that protect these libraries from unrestricted commercial use without attribution or respect for the rights of authors.

我們尤其必須制定清晰開源框架協議與貢獻者規范，防范項目成果被商業主體無償盜用、無視原作者著作權。

Another proposal being pursued by multiple groups is the creation of community-owned benchmarks. Good benchmarks can signal community values to those developing AI systems, while also helping mathematicians understand realistic use cases for, and limitations of, the technology. For example, benchmarks that focus on open-ended problems can counter overstated claims based on narrow task suites.

另一項學界共識方案：共建屬于數學共同體的評測基準數據集。優質基準既能向 AI 研發方傳遞數學界價值導向，也幫助數學家認清 AI 真實能力邊界與落地局限；聚焦開放性數學問題的基準庫，還能遏制廠商基于窄域測試夸大 AI 性能的宣傳亂象。

當前頂尖數學推理 AI 多由商業科技企業閉源研發，但開源、權重開放的同類模型正不斷涌現（如 Goedel-Prover、Kimina-Prover）[5, 8]。閉源與開源路線既存在良性競爭，也可在學界內部、產學研之間協同互補：交叉驗證、技術互補、經驗互通，助力整個行業理性推進數學 AI 研發。

據此確立建設目標：

搭建學術導向的數學 AI 基礎設施：代碼開源、決策透明、由學界共同監督，降低數學領域對單一商業企業的技術依賴。

這套公共基建除守護數學學術獨立外，還能實現算力成本、訓練數據、能耗環保等關鍵信息公開透明，讓技術研發始終對齊數學共同體的發展優先級。

五、行業規范、科研倫理與治理框架

人工智能融入數學研究，衍生出諸多突出的倫理與治理難題。

The training of such systems uses the work of the mathematical community in an opaque way that threatens established norms of attribution and credit. AI-generated papers are starting to put still more pressure on a publication system already strained to the breaking point; and how should formal proofs be integrated into this?

1. 這類人工智能系統在訓練過程中，以不透明的方式取用數學界前人的研究成果，動搖了現行的成果署名與學術確權規范。由人工智能生成的論文，進一步加重本就瀕臨承壓極限的學術出版體系負擔；而形式化證明又該如何納入現有出版規則，目前尚無定論。

3. Mechanization may also create new forms of inequality, in which disparities in access to computational resources distort the competitive dynamics of mathematical research. Moreover, the substantial energy demands of AI systems raise important environmental concerns.

   機械化工具還可能催生新的科研不公：算力資源獲取條件的差距，會打破數學科研公平競爭的格局。除此之外，人工智能模型龐大的能耗需求，也帶來不容忽視的環保問題。

為此學界提出落地建議：

Develop and maintain a living statement of ethical principles to guide academic mathematicians and mathematical institutions in their interactions with AI systems and developers.

編制并動態更新數學 AI 倫理準則規范，指導數學研究者與科研機構規范和 AI 技術方的合作。

該倫理文件不具備強制法律效力，也無法窮盡全部細則，經由廣泛學界磋商形成，凝練全行業共識與行為規范（對標 1975 年重組 DNA 阿西洛馬倫理會議模式[6]），內容涵蓋：成果署名與引用規范、算力與訓練數據披露要求、預印本與形式證明庫開源授權細則、AI 使用行為守則。文件需由各國數學學會牽頭常態化修訂，持續適配新興技術挑戰；本次研討會已有參會學者啟動準則起草工作。

結語：主動參與 AI 與數學的議題共建

層出不窮的 AI 新聞，容易讓一部分研究者心生質疑，也會讓另一部分人被動躺平、消極認命。本文呼吁所有讀者主動投身相關討論：學習 AI 技術原理與能力邊界，和同事、學生、行業學會深入交流，立足自身科研體悟梳理個人數學價值觀，并落地集體行動。

當下正處在數學發展的關鍵十字路口，學科的未來定義權正在重新博弈。積極參與相關研討，就是讓數學的未來扎根全人類數學家共同的理想與價值。

原文參考文獻

[1] J. Commelin and A. Topaz (2024)：純數學中的抽象邊界與規范驅動開發，《美國數學會通報》第 61 卷第 2 期，241–255 頁

https://dx.doi.org/10.1090/bull/1831

[2] Lean 社區 (2020)：Lean 數學庫，《ACM 第 9 屆認證程序與證明國際會議論文集》，367–381 頁

https://dx.doi.org/10.1145/3372885.3373824

[3] L. de Moura 等人 (2015)：Lean 定理證明器（系統綜述），CADE 第 25 屆自動推理會議，《計算機講義》9195 卷，378–388 頁

https://dx.doi.org/10.1007/978-3-319-21401-6%5F26

[4] T. Hubert 等人 (2025)：《基于強化學習實現奧賽級形式數學推理》，《自然》651 卷 (8106)，607–613 頁

https://dx.doi.org/10.1038/s41586-025-09833-y

[5] Y. Lin 等人 (2025)：Goedel-Prover：前沿開源自動定理證明模型（預印本 2502.07640）

https://arxiv.org/abs/2502.07640

[6] 1975 阿西洛馬重組 DNA 會議組委會：重組 DNA 阿西洛馬會議，《自然》255 卷，442 頁

https://dx.doi.org/10.1038/255442a0

[7] A. Salim (2025)：借助大模型加速數學研究：凸分析問題 GPT-5-Pro 協作案例（預印本 2510.26647）

https://arxiv.org/abs/2510.26647

[8] H. Wang 等人 (2025)：Kimina-Prover 預覽：面向強化學習的大規模形式推理模型（預印本 2504.11354）

https://arxiv.org/abs/2504.11354

腳注對應鏈接

1 Lean 社區官網：

https://leanprover-community.github.io

2 洛倫茨中心會議主頁：

https://www.lorentzcenter.nl/mechanization-and-mathematical-research.html

講座回放：

https://www.youtube.com/@mechanicalmath

3 AFP 形式證明檔案庫官網：

https://www.isa-afp.org

參考資料

https://arxiv.org/html/2603.24914v2

https://mathstodon.xyz/@tao/116681024360293007

https://leidendeclaration.ai

https://www.universiteitleiden.nl/en/news/2026/06/leiden-declaration-warns-ai-is-challenging-the-core-values-of-mathematics

https://www.lorentzcenter.nl/mechanization-and-mathematical-research.html

小樂數學科普近期文章

小樂數學科普歷年合集

版權聲明：本文首發于微信公眾號“zzllrr小樂”的專欄《小樂數學科普》。歡迎個人轉發。如需轉載，請在“zzllrr小樂”公眾號后臺回復“轉載”，還可通過公眾號菜單、發送郵件到zzllrr@gmail.com與我們取得聯系。相關圖文音視頻內容默認遵守CC BY-NC 4.0知識共享協議，未獲作者和譯者授權，禁止用于營銷宣傳和商業目的。

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊底部一起捐

助力騰訊公益

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！