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

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

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

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

作者簡介

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

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

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

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

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

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

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

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

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

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

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

可擴(kuò)展性是真正的試金石

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

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

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

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

從理論走向?qū)嵺`

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

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

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

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

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

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

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

自動化作為“博弈步驟”

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

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

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

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

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

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

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

展望未來

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

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

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

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

參考資料

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ù)學(xué)科普近期文章

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

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點(diǎn)贊、在看、在聽

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

查看原始文章出處

點(diǎn)擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

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