AI人工智能正在改變我們撰寫形式化證明的方式——萊昂納多?德?莫拉（Leonardo de Moura）

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

AI 將深度參與下一代證明輔助工具的構建，但工具優劣的核心標準不變：高表達類型、易讀規范、強自動化、可編程生態、優質工具鏈、可擴展性；技術迭代是進步的標志，目標是推動形式化數學的實用化與普及化。

作者：萊昂納多?德?莫拉（Leonardo de Moura）2026-2-18

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

作者簡介

萊昂納多?德?莫拉（Leonardo de Moura）是亞馬遜云科技（AWS）自動化推理小組的高級首席應用科學家。在業余時間，他投身于非營利組織 Lean FRO 的工作，擔任首席架構師一職 —— 該組織由他與塞巴斯蒂安?烏爾里希（Sebastian Ullrich）共同創立，他對此深感自豪。他同時還受聘擔任 Lean FRO 的董事會成員，積極為該組織的發展壯大貢獻力量。

2023年加入亞馬遜云科技之前，自2006年起，他曾在微軟研究院（Microsoft Research）的 RiSE 研究小組任職長達 17 年，擔任高級首席研究員。更早之前，他曾就職于美國斯坦福國際研究院（SRI International），擔任計算機科學家。

他的研究領域包括自動化推理、定理證明、決策過程以及可滿足性問題（SAT）與可滿足性模理論（SMT）。他是多款自動化推理工具的主要架構師，其中包括 Lean、Z3、Yices 1.0 以及 SAL。

萊昂納多在自動化推理領域的研究成果斬獲了多項頗具聲望的獎項，其中包括計算機輔助驗證大會（CAV）獎、海法獎、埃爾布朗獎，此外，他還憑借 Z3 與 Lean 兩次榮獲美國計算機協會編程語言專業組（ACM SIGPLAN）編程語言軟件獎。他的研究成果也被《紐約時報》，以及《連線》、《量子雜志》、《自然新聞》、《科學美國人》等眾多科普期刊報道。

如今，語言模型只需極少的人工指導，就能生成數千行經過驗證的數學證明代碼，且相關成本還在持續下降。這一突破令人振奮，同時也引出一個自然而然的問題：當人工智能承擔更多證明工作時，證明輔助工具的選擇會起到怎樣的作用？

我認為答案是：它的重要性非但沒有降低，反而愈發凸顯。

證明輔助工具絕非僅服務于人工智能的工具，它更是人類與人工智能協同工作的核心環境。人類需要在其中查閱定義、理解定理表述、指導證明策略，并基于已驗證的結論進行拓展；人工智能則需要高效生成證明、從反饋中學習，并借助自動化能力提升效率。一款設計精良的證明輔助工具能夠同時滿足雙方的需求，而隨著人工智能在證明工作中占據更大比重，那些促成這種高效協作的設計選型，其影響也會變得愈發關鍵。

人工智能放大基礎架構的價值

當人工智能生成證明時，它會在目標系統的約束框架內運行。如果該系統具備表達力強的類型系統、強大的自動化功能和易讀的符號體系，人工智能就能充分利用這些優勢。就連錯誤提示的設計也至關重要：結構化、可操作的診斷信息能幫助人工智能高效修正錯誤，這與優質的錯誤提示對人類用戶的幫助如出一轍。系統的表示形式決定了人工智能能否簡潔地表達數學思想，而當我們的目標是將形式化證明拓展至整個數學領域、而非局限于某一本教科書時，簡潔性的重要性不言而喻。

不妨這樣理解：計算器的出現并未讓數學變得無足輕重，它幫我們省去了繁瑣的算術運算，讓我們得以專注于真正的問題本身。但計算器的實用價值，完全取決于你所采用的數學框架——表示形式至關重要。

這一道理同樣適用于人工智能與證明輔助工具的關系。若語言模型基于的系統具備依賴類型、類型類和設計良好的策略語言，它就能在恰當的抽象層級上表達數學思想。由此生成的證明更簡短、結構更清晰，人工智能也能在更高的抽象層面開展工作。這是一種會不斷疊加的優勢。

可擴展性是真正的試金石

將拓撲學的一個章節進行形式化，已是一項令人贊嘆的成果。但構建一個包含數十萬條定理、且能長期維護的庫，則是全然不同的挑戰。這本質上是一個工程問題，而工程問題的解決效果，對設計選型的細節高度敏感。

簡潔、結構良好的證明，是訓練人工智能的優質數據；基于這些數據訓練出的人工智能，又能生成更出色的證明；優質的證明反過來會提升庫的實用性，進而吸引更多用戶和貢獻者。這是一個良性循環的飛輪，而證明輔助工具正是驅動飛輪轉動的核心。越來越多的證據印證了這一點：谷歌深度思維（Google DeepMind）研發的強化學習系統AlphaProof，在2024年國際數學奧林匹克競賽中斬獲銀牌，其底層正是基于一款擁有龐大且結構良好的庫的證明輔助工具。正如谷歌深度思維的普什米特·科利（Pushmeet Kohli）所指出的，該系統的“可擴展性與驗證能力”是取得突破的關鍵支撐。無獨有偶，Harmonic公司（https://harmonic.fun ）研發的Aristotle系統，在2025年國際數學奧林匹克競賽中達到金牌水準，同樣基于這一技術基礎；字節跳動的SEED Prover系統也在該賽事中獲得銀牌，底層框架亦別無二致。三支獨立的團隊，在最高水平的賽事中攻克同一難題，卻不約而同地選擇了具備表達力強的類型系統、龐大的庫和可編程生態的證明輔助工具。不止這三家：Axiom Math（https://axiommath.ai ）、Math Inc（https://www.math.inc ）、Logical Intelligence（https://logicalintelligence.com ）等公司，也都在同一技術基礎上開展研發。可見，底層工具的選擇，是它們取得成功的關鍵因素，絕非偶然。

快速的證明校驗速度也同樣重要。當人工智能在反饋循環中探索數千種證明方案時，內核的運算速度會直接決定單位時間內人工智能的學習效率。這是一個現實存在的工程約束，證明輔助工具的研發者應當重視這一點。但僅有校驗速度是遠遠不夠的：一個運算速度快、卻缺乏自動化功能和高效類型系統的內核，只能快速校驗冗長繁瑣的證明；而設計精良的系統生成的證明足夠簡潔，校驗速度往往不會成為瓶頸。這兩方面的優化是相輔相成的。

正是強大的自動化能力、表達力強的類型系統和清晰的定義歸約機制，才讓簡潔的證明成為可能。它們是支撐人類與人工智能在恰當抽象層級開展工作的基礎設施。

從理論走向實踐

理論上，任何數學內容都可以在集合論或其他具備足夠表達力的基礎框架中實現形式化。這一點毋庸置疑，就像任何程序都能在圖靈機上運行一樣。

但從“理論上可形式化”到“實踐中可落地”的鴻溝，恰恰是證明輔助工具設計需要攻克的核心問題。依賴類型讓抽象代數、范疇論和現代代數幾何的形式化成為現實，避免了陷入繁瑣的編碼冗余；類型類則讓龐大的數學庫具備可導航性和可組合性。證明輔助工具絕非僅僅是一個校驗證明的內核，它是一整套完整的環境，決定了大規模場景下哪些數學內容的表達和維護具備實際可行性。

易讀的規范說明：人類的信任契約

證明輔助工具能保證證明的正確性，但正確性本身還不夠。必須有人去閱讀定理的表述，并確認其準確捕捉了我們想要表達的數學思想。這是一份無論自動化程度多高都無法規避的人類契約。

能夠編寫讓數學家可以審閱和理解的定義與定理表述，是證明輔助工具的核心要求。這一點直接取決于類型系統的表達力和符號機制的設計質量。現代工具進一步強化了這一能力：集成開發環境（IDE）支持鼠標懸停查看術語類型、跳轉至定義、交互式探索庫內容，這些功能讓那些不會親自撰寫證明，但能夠閱讀和驗證表述的人，也能接觸到形式化數學。學習閱讀形式化規范說明，遠比學習撰寫它們容易，而優質的工具讓閱讀過程變得更加便捷。當定義清晰易懂、工具易用性高時，數學家就能直接參與到形式化庫的使用和驗證中；反之，若定義被冗余的編碼所掩蓋，無論驗證了多少定理，非形式化數學與形式化數學之間的鴻溝都將始終存在。

當人工智能負責生成證明時，這一點就更為關鍵。如果一個定理的形式化表述你完全無法解讀，那么即便它的證明經過了驗證，對你而言也毫無價值。你需要信任的，不僅是證明本身，還有規范說明。

有人可能會提出，人工智能可以在形式化表述與自然語言之間進行翻譯，這樣無論底層采用何種形式化框架，人類都能閱讀通俗易懂的版本。但這種做法恰恰會在最需要保證正確性的環節，引入新的潛在錯誤源。形式化表述才是信任的基石。試想一個對抗性場景：有人聲稱證明了一項重要成果，此時你需要審閱的是真實的形式化表述，而非人工智能生成的摘要。易讀的形式化規范說明并非人工智能可以替代的便利功能，而是信任的基礎。

自動化作為“博弈步驟”

我認為有一種理解證明自動化的方式十分實用：證明器所具備的每一種策略或決策過程，都相當于博弈中的一步棋。如果一個系統只有基礎的操作步驟（如應用引理、重寫術語、展開定義），那么即便是常規的推理過程，也需要冗長的步驟序列才能完成；而具備強大自動化能力的系統，則能提供“一步到位”的操作，實現原本需要數百步才能完成的推理。

這對人工智能而言意義重大。用語言模型去完成數百步低層級的證明推導，就如同用語言模型去計算復雜的算術表達式——雖然理論上可以做到，但使用專用工具顯然效率更高。強大的策略能讓人工智能省去繁瑣的常規工作，專注于數學上真正具有挑戰性的決策：高層級的證明策略、引理的選擇、關鍵的分支劃分。工具應當負責其擅長的領域，人類和人工智能則聚焦于更核心的創造性工作。

正因如此，投入研發證明自動化技術（決策過程、簡化器、通用策略），對人類用戶而言絕非只是提升使用體驗的改進，它還能直接提升人工智能生成證明的質量與效率。你為系統添加的每一種強大策略，都是人工智能可以利用的新能力。

理想的自動化工具應當兼具強大性與可控性。能一步完成目標證明的策略固然有價值，但更具價值的是那些可以交互式運行的策略，讓人工智能能夠逐步指導決策過程。這賦予了人工智能選擇權：當簡單操作足夠時，可將策略作為單一的強力步驟使用；當問題復雜時，則可采取更精細的控制方式。不透明的自動化工具或許有用，但透明且可操控的自動化工具，才能帶來革命性的改變。

可編程的生態系統

一款同時兼具編程語言屬性的證明輔助工具，其疊加優勢往往容易被低估。當策略、自動化組件、元程序和經過驗證的代碼都采用同一種語言編寫時，所有模塊都會相互賦能、形成合力。任何人（包括人工智能）都能編寫新的自動化組件，無需切換開發環境或編程語言。“使用系統”與“擴展系統”之間的界限將不復存在。

這一點對人工智能的集成尤為重要。當人工智能不僅能撰寫證明，還能編寫新的策略、構建定制化決策過程、拓展系統功能時，就會形成一個正向反饋循環：系統越完善，越能助力人工智能；人工智能越強大，越能反過來優化系統。

展望未來

下一代頂尖的證明輔助工具，很可能會在人工智能的大規模協助下構建。在Lean FRO（https://lean-lang.org ）團隊，我們早已將人工智能納入開發流程。它帶來了顛覆性的改變，如今我們已經無法想象脫離人工智能去開發Lean系統。在我們的代碼倉庫中，隨處可見由人工智能參與撰寫的提交記錄。這一趨勢只會愈演愈烈：人工智能將協助我們進行系統設計、生成核心庫、編寫自動化組件，并測試系統的人機交互體驗。但評判一款證明輔助工具優劣的標準從未改變——它仍需具備表達力強的類型系統、易讀的規范說明、強大的自動化能力、可編程的生態系統、優質的工具鏈和卓越的可擴展性。人工智能改變的是我們構建證明輔助工具的方式，而非衡量其優劣的核心標準。

當下已有的各類系統、它們的庫、設計決策，以及在實踐中積累的成敗經驗，都將成為構建下一代系統的訓練數據和設計藍本。過往的努力絕非徒勞，而是奠定未來發展的堅實基礎。

沒有任何技術能夠永遠存在，這恰恰是進步的標志，而非失敗。我們的目標并非構建一個能永久存續的系統，而是推動形式化數學的發展進程，讓形式化數學、經過驗證的軟硬件變得切實可行、易于獲取且具備實用價值，讓下一代技術能站在更高的起點上出發。如果未來出現了真正更優越的系統，那就意味著我們的使命已經達成。

我所關心的是，這一發展進程始終由真正的技術進步驅動。在人工智能時代，評判優質證明輔助工具的標準已然清晰，且其重要性正前所未有地凸顯。

參考資料

https://leodemoura.github.io/blog/2026/02/18/proof-assistants-in-the-age-of-ai.html

https://lean-lang.org

https://harmonic.fun

https://axiommath.ai

https://www.math.inc

https://logicalintelligence.com

小樂數學科普近期文章

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

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

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

收藏、分享、轉載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！