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

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

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

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

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

作者簡介

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

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

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

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

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

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

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

人工智能放大基礎(chǔ)架構(gòu)的價值

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

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

這一道理同樣適用于人工智能與證明輔助工具的關(guān)系。若語言模型基于的系統(tǒng)具備依賴類型、類型類和設(shè)計良好的策略語言，它就能在恰當?shù)某橄髮蛹壣媳磉_數(shù)學思想。由此生成的證明更簡短、結(jié)構(gòu)更清晰，人工智能也能在更高的抽象層面開展工作。這是一種會不斷疊加的優(yōu)勢。

可擴展性是真正的試金石

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

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

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

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

從理論走向?qū)嵺`

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

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

易讀的規(guī)范說明：人類的信任契約

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

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

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

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

自動化作為“博弈步驟”

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

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

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

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

可編程的生態(tài)系統(tǒng)

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

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

展望未來

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

當下已有的各類系統(tǒng)、它們的庫、設(shè)計決策，以及在實踐中積累的成敗經(jīng)驗，都將成為構(gòu)建下一代系統(tǒng)的訓練數(shù)據(jù)和設(shè)計藍本。過往的努力絕非徒勞，而是奠定未來發(fā)展的堅實基礎(chǔ)。

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

我所關(guān)心的是，這一發(fā)展進程始終由真正的技術(shù)進步驅(qū)動。在人工智能時代，評判優(yōu)質(zhì)證明輔助工具的標準已然清晰，且其重要性正前所未有地凸顯。

參考資料

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

小樂數(shù)學科普近期文章

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

讓數(shù)學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

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

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數(shù)學科普不迷路！