AI人工智能時代的數學家們——杰里米·阿維加德（Jeremy Avigad）

★置頂zzllrr小樂公眾號（主頁右上角）數學科普不迷路！

AI人工智能能夠以形式化和非形式化的方式證明數學領域的研究級定理。當前全球交互式定理證明（Lean）與形式化數學領域的核心領軍人物之一、卡內基梅隆大學教授杰里米·阿維加德（Jeremy Avigad）呼吁數學家們緊跟該技術的發展步伐，思考其對數學研究實踐的顛覆性影響，并以恰當的方式應對當下面臨的挑戰與機遇。

杰里米·阿維加德（Jeremy Avigad）卡內基梅隆大學教授

作者：杰里米·阿維加德（Jeremy Avigad，卡內基梅隆大學教授）2026-3-7

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

致謝

感謝約翰·科梅林（Johan Commelin）、西德哈斯·哈里哈蘭（Sidharth Hariharan）、布萊娜·克拉（Bryna Kra）、埃米莉·里爾（Emily Riehl）與阿克沙伊·文卡特什（Akshay Venkatesh）提供的意見、修正建議與研究思路。

1 研究背景

過去一年，美國國家科學基金會（NSF）的發展步履維艱，但即便其下屬所有研究所的預算均被削減，該基金會仍在去年秋季成功成立了數學計算機輔助推理研究所（ICARM）。該研究所的使命是支持數學領域新推理技術的應用，其中多項技術均涉及神經人工智能與符號人工智能。作為研究所所長，我曾以《AI人工智能時代的數學》為題發表過多版演講，梳理了各類新興技術，包括形式化與證明助手、符號人工智能與自動推理，以及機器學習與神經網絡。這些技術雖各有不同，卻存在有趣的交叉與互動。

迄今為止，形式化方法的早期實踐者為數學形式化庫Mathlib做出了貢獻，多個合作項目已借助該庫驗證了當代數學研究成果，部分成果的驗證甚至早于常規同行評審流程，或是在未開展同行評審的情況下完成。SAT求解器等自動推理工具解決了組合數學、代數學、數論與離散幾何領域的多個公開問題；機器學習技術被用于挖掘計算數據中的模式及數據間的關聯，助力新研究成果的發現，且這些成果均已通過傳統證明方式得到驗證，該技術還被用于尋找具有研究價值的組合對象，包括某些猜想的反例；神經網絡則被用于求解偏微分方程、識別具有研究意義的現象，以及尋找能催生此類現象的參數設置。盡管這些技術目前仍屬于小眾領域，且僅有為數不多的顯著成果，但相關進展足以表明，它們必將對數學學科產生重大影響。

神經網絡將機器學習與符號方法相結合，被應用于數學定理的證明工作。這一應用有時表現為利用語言模型和智能主體系統撰寫非形式化的數學論證過程，有時則是借助其構建形式化證明，而這些證明的正確性會由Lean等證明檢查器進行驗證。許多系統會在兩種推理層面交替進行，既借鑒傳統數學文獻中的洞見，又依托形式化檢查器提供的強正確性驗證信號。該領域近期的發展尤為顯著。我在各類演講中對這些技術的整體態度始終較為樂觀：新興技術能夠助力我們更好地開展數學研究，完成以往無法實現的研究工作。它們不僅能對數學成果的驗證與發現產生積極作用，還會影響數學的教學與學習方式、數學知識的整理留存，以及數學思想的協作交流模式。

不過，這些演講也兼顧了人們對人工智能的諸多擔憂。我曾在論文《數學是否已過時？》https://arxiv.org/abs/2502.14874 中對這些擔憂進行過深入探討，近期也以《如何看待AI人工智能時代的數學之憂》為題發表過相關演講。我發現，將這些擔憂分為兩類會更便于分析，即對人工智能的一般性擔憂，以及對人工智能給數學領域帶來的具體影響的擔憂。

對人工智能的一般性擔憂，不僅涉及其對社會、經濟和環境的影響，還包括其對人類獨立思考與推理能力的沖擊，以及將人類的生活與生計寄托于行為不可控、原理未被完全理解的系統所存在的合理性問題。我在《數學是否已過時？》一文中提出，數學至少能為解決這些問題提供部分思路，因為它讓我們能夠提出精準的問題，并以可獨立驗證、查詢和審計的形式要求人工智能給出解釋與論證依據。數學為我們與人工智能的互動提供了方法，讓人類始終處于思考決策的核心位置，保持對自身決策的主導權。

本文探討的是第二類擔憂，即人工智能對數學行業產生的具體影響，由近期一系列值得我們深思的發展所引發。如今，技術的顛覆性已愈發明顯，而我們對這一事實的重視程度遠遠不夠。作為推動新興技術落地的研究所所長，我或許在這場技術變革中難辭其咎，但本文的核心觀點是：無論我們接受與否，人工智能已經到來，若我們無法主動迎接這一挑戰，所有人都將成為這場變革的被動參與者。為了我們的學生，也為了數學學科的發展，我們必須做好這件事。

2 近期研究進展

2024年初，彼時還是帝國理工學院交換生、正在洛桑聯邦理工學院訪學的西德哈斯·哈里哈蘭（Sidharth Hariharan）——如今是卡內基梅隆大學一年級博士生——與瑪麗娜·維亞佐夫斯卡（Maryna Viazovska）展開合作，啟動了維亞佐夫斯卡關于E?格在8維球填充中最優性證明的形式化項目。如今，他們采用的方法已成為形式化學術界的標準方法：先撰寫詳細的非形式化藍圖，為形式化工作提供指導。（參閱zzllrr小樂數學科普文章：）

克里斯·伯克貝克（Chris Birkbeck）與李瑞宇（Seewoo Lee）在同年夏天加入該項目，到了秋季，該項目成為西德哈斯在巴維克·梅塔（Bhavik Mehta）指導下完成碩士論文的研究基礎。2025年7月，維亞佐夫斯卡（Maryna Viazovska）在英國劍橋艾薩克·牛頓研究所舉辦的“大證明”會議上發表演講，匯報了該項目的進展，彼時該團隊已將項目面向公眾開放。

2025年秋季，項目推進十分順利。項目負責人通過社交媒體和每周的Zoom線上會議協調志愿者團隊開展研究，多家人工智能初創企業主動接洽，希望借助該項目測試其產品性能。該團隊積極接納人工智能技術，不僅接收人工智能生成的“拉取請求”，還對其進行修訂以符合項目的貢獻標準，并將其整合至代碼庫中，項目負責人也親自參與人工智能技術的實驗。

然而，幾周前，西德哈斯（Sidharth Hariharan）面色蒼白地來到我的辦公室，他剛得知，一家名為數學公司（Math Inc.）的企業為展示其最新證明智能體高斯（Gauss）的能力，完成了該項目最終結論的形式化證明。該公司曾在11月為該項目提供過協作支持，卻隨后突然中止溝通，轉為秘密研究。這并非該研究團隊所期望的人工智能協作模式，他們從未想過，這家企業會為了取得博人眼球的成果，投入大量計算資源攻關該項目——馬特·巴拉德（Matt Ballard）將這種行為貼切地描述為“過路式證明”。此后，該公司又在未獲得該團隊任何額外支持的情況下，利用高斯（Gauss）驗證了基于8維球填充結論推導的24維球填充相關成果 https://www.math.inc/sphere-packing

Lean社區的多位知名人士，包括維護團隊成員，紛紛伸出援手，協助項目負責人應對這一情況。團隊的擔憂之一是，該公司在新聞稿中會如何描述這一成果：高斯（Gauss）的成功，建立在人類研究者近兩年的創造性工作、研究框架搭建和規劃的基礎之上，若將其單純宣傳為人工智能的成就，對這些主要是青年研究者的團隊成員而言極不公平。

更大的擔憂則是，該公司會宣稱該項目“已完成”。事實上，單純的形式化證明本身幾乎毫無價值，因為維亞佐夫斯卡（Maryna Viazovska）的研究結論的正確性從未受到質疑。研究團隊開展該項目，實則是為了重新梳理這些研究成果，加深對其的理解，同時構建相關庫和基礎設施，為未來的研究工作提供支撐。而人工智能生成的證明往往冗長繁雜，且僅聚焦于手頭的具體任務，項目負責人擔心，這種自私的成果搶占行為，會讓團隊失去修訂代碼、將其完善至預期狀態的動力。

不過，數學公司（Math Inc.）最終與項目負責人展開合作，確保相關公告對該研究團隊的貢獻給予了恰當認可，并承諾將與團隊公開協作，修訂和優化代碼以符合項目標準。如今，學界對這種人機協作模式的良好發展持謹慎樂觀態度。從消極角度看，項目組織者只是在糟糕的處境中盡力挽回局面；而從積極角度看，我們都在從中學習如何讓人工智能更好地服務于數學研究。目前，這一模式的發展走向仍未可知：如果人工智能能夠減少形式化工作中的繁瑣環節，幫助我們更好地感受和理解數學，那我們將迎來更好的發展；但如果它阻礙了我們對數學的探索樂趣和理解深度，那我們將失去一些重要的東西。

在這場形式化定理證明的風波發生的同時，數學界還見證了一場非形式化定理證明的補充實驗。2月5日，11位數學家在arXiv平臺發布了10道面向AI人工智能的挑戰題First Proof（ https://arxiv.org/abs/2602.05192 參閱）他們的目的是評估人工智能輔助實際數學研究的能力，為此，團隊挑選了各自研究中遇到的問題，這些問題均已有約5頁篇幅的證明過程，但相關成果尚未發表。他們對Gemini 3.0深度思考版和ChatGPT 5.2專業版兩款商用系統進行了測試，結果卻不盡如人意。不過，他們也邀請了人工智能開發者用自研系統嘗試解決這些問題，并要求開發者在2月13日前公開研究結果，供學界共同評估。

部分人工智能開發者響應了這一邀請，該論文的作者們委托數學計算機輔助推理研究所（ICARM）在其Zulip社交平臺的相關頻道開展結果研討（http://icarm.zulipchat.com ，“首輪證明First Proof”頻道）并邀請數學家對人工智能的解題成果進行評價。開放人工智能公司（OpenAI）研發的模型針對其中一道問題給出的解法，被專家評價為“完全正確，且推導過程十分精妙”。表現最佳的是谷歌深度思維（Google DeepMind）研發的證明智能體阿勒西婭（Aletheia），該智能體正確解決了10道問題中的6道（https://arxiv.org/pdf/2602.21201.pdf 參閱）我想，對這樣的成果表現感到驚訝的，并非只有我一人。

這些發展表明，人工智能在非形式化和形式化數學研究中的表現正愈發出色。2022年11月ChatGPT首次發布時，我們還曾嘲笑它解答數學問題的糟糕表現；而去年夏天，已有四家企業宣稱其研發的人工智能系統能在國際數學奧林匹克競賽題中取得金牌水平，其中兩家的系統可生成非形式化解法，另外兩家則能生成形式化解法。如今，性能頂尖的人工智能系統已逐漸攻克普特南數學競賽的基準題。人工智能已能處理研究級的數學證明問題，這意味著，數學領域已再無“遮羞之地”。在不到四年的時間里，人工智能的定理證明能力從幾乎為零發展到如今的水平，而在此期間，人工智能研發的相關投資也出現了爆發式增長。我們必須直面一個事實：人工智能很快就能比人類更擅長證明數學定理。

3 現存擔憂

如今，我們陷入了一種尷尬的境地：人工智能正在完成那些我們曾認為只有人類才能做到的事。我們曾為自身的能力倍感自豪——能夠解決極具難度的問題，構建邏輯嚴謹的長篇論證，整合眾多復雜要素并做出精準的推導，但現在我們發現，人工智能也能做到這些。我們還曾為自己擁有深刻的洞見與直覺、能發現微妙的模式與關聯、能構建具有深遠意義的廣義理論而驕傲，而當代人工智能的應用也正朝著這些方向發展。

我們需要思考，這一切會給數學行業帶來怎樣的影響。高校數學家的工作價值究竟何在？從某種程度來說，這份工作的存在是因為有數學專業的學生——也就是熱愛數學、且父母愿意支持其學習的年輕人。我們不禁要問，若數學研究變成了向人工智能發出查詢指令，這份熱愛還能延續嗎？

同事們常對我說，即便國際象棋引擎的水平遠超人類棋手，職業棋手依然存在，但這一點安慰對我而言微不足道：我們不會要求孩子們從幼兒園到高中一直學習下國際象棋，而以國際象棋家教為業也難以維持生計。將對數學的熱愛比作對音樂和藝術的熱愛，或許是更貼切的類比，但音樂和藝術領域同樣面臨著發展支持不足的問題。如果我們為數學教學找到的最佳理由，僅僅是它能帶來審美享受或休閑樂趣，那么數學的發展將舉步維艱。

高校數學家的工作之所以具有實際價值，更重要的原因在于，我們為工程、商科、計算機科學、數據科學等領域開設服務性課程，而這些領域均獲得了企業和政府的大力支持。但我們不難想象，這種支持也可能逐漸減少。如今，學生早已能借助人工智能完成我們數十年來布置的各類作業，而我們為了遏制這種行為設置的課堂考試，實則是人為剝奪了他們使用職業發展中必會接觸到的工具的機會。如果我們不教工程師利用人工智能解決問題，那就是沒有盡到培養工程師的職責，而工程學院也將不再需要我們開設的課程。我們或許不會看到相關需求一夜之間消失，但學術環境的變化日新月異，一旦根基坍塌，便難以恢復。

4 建議與展望

我們不應被上文中的悲觀預警擊垮，而應相信數學的力量。正如我在《數學是否已過時？》一文中所言，在人工智能時代，利用精準的語言和抽象思維幫助我們理解周遭世界、高效推理并交流思想，依然具有至關重要的意義。技術的進步為我們實現數學研究目標提供了新的途徑，而人工智能終究只是一種技術，如何運用它，決定權掌握在我們手中。

在《數學是否已過時？》的結尾，我描繪了兩種未來圖景：一種是反烏托邦的，人類放棄數學，將思考決策的主導權讓渡給人工智能；另一種則是樂觀的，數學始終在思考決策過程中占據核心位置。而前文所描述的現狀，大致就是反烏托邦圖景的寫照。那么，對數學家而言，樂觀的發展圖景又將如何實現？答案其實很簡單：借助人工智能，更好地開展我們所熟知并熱愛的數學研究。如果人工智能能助力我們實現朗蘭茲綱領、證明哥德巴赫猜想、解決P≠NP問題，這難道是一件壞事嗎？我們理應期待人工智能為純數學和應用數學研究帶來的裨益。如果科學家、工程師和分析師能夠借助數學提供的定性和定量工具，高效運用人工智能設計出更優化的系統、取得更可靠的研究成果，那么數學的價值便已完全得以體現。

我們需要牢記自身的優勢：數學家是頂尖的問題解決者和理論構建者。面對人工智能在數學領域的應用，我們不應抗拒，而應主動掌握其主動權。僅僅緊跟技術發展、為人工智能研究者設計基準測試題是遠遠不夠的，我們需要積極參與到技術的落地應用中，讓其貼合數學研究的需求。同時，我們還要學會培養學生，讓他們擁有合理運用這些新技術的智慧，且務必確保核心的數學直覺與理解能力能夠有效傳遞給學生。

找到有效運用人工智能實現數學研究目標的方法并非易事，但數學家向來樂于迎接挑戰——事實上，挑戰越大，我們的動力便越強。只要我們直面人工智能的到來，堅守數學研究的核心價值，數學學科必將迎來蓬勃發展。我們所需做的，只是躬身入局，潛心鉆研。

參考資料

https://arxiv.org/abs/2603.03684

https://github.com/avigad

https://www.andrew.cmu.edu/user/avigad/talks.html

https://www.andrew.cmu.edu/user/avigad/Talks/lms-bcs.pdf

https://www.andrew.cmu.edu/user/avigad/Talks/rademacher1-intro.pdf

https://arxiv.org/abs/2502.14874

https://www.math.inc/sphere-packing

https://arxiv.org/abs/2602.05192

http://icarm.zulipchat.com

https://arxiv.org/abs/2602.21201

小樂數學科普近期文章

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

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

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

收藏、分享、轉載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！