LEANCAT：Lean 中形式化范疇論的基準套件（第一部分：1-范疇）

LEANCAT：Lean 中形式化范疇論的基準套件（第一部分：1-范疇）

LEANCAT: A BENCHMARK SUITE FOR FORMAL CATE-GORY THEORY IN LEAN (PART I: 1-CATEGORIES)

https://www.arxiv.org/pdf/2512.24796

摘要

大語言模型（LLMs）在形式化定理證明方面取得了快速進展，但當前的基準測試未能充分衡量現代數學中所依賴的抽象能力和基于庫的推理能力。與 FATE 對前沿代數的強調相呼應，我們推出了 LeanCat1——一個面向范疇論形式化的 Lean 基準測試。范疇論是數學結構的統一語言，也是現代證明工程的核心層，本基準旨在對結構性、接口級推理能力進行壓力測試。第一部分“1-范疇”包含 100 個完全形式化的陳述級任務，通過 LLM 輔助結合人工評分的方式，按主題歸類并劃分為三個難度等級（簡單、中等、高難）。當前最佳模型在 pass@1 下解決 8.25% 的任務（按難度分別為 32.50% / 4.17% / 0.00%），在 pass@4 下解決 12.00%（50.00% / 4.76% / 0.00%）。我們還評估了使用 LeanExplore 搜索 Mathlib 的 LeanBridge 方法，發現其性能持續優于單模型基線。LeanCat 旨在作為一個緊湊、可復用的檢查點，用于追蹤人工智能與人類在 Lean 中實現可靠、研究級形式化方面的進展。

1 引言
近期大語言模型（LLMs）與智能體訓練（agentic training）的進展重新激發了端到端形式化定理證明的前景。在形式化方面，諸如 OpenAI 早期基于 Lean 的證明器（Polu 等，2022）和 DeepMind 的 AlphaProof（Hubert 等，2025）等系統表明，結合形式驗證反饋的強化學習能夠生成非平凡的 Lean 證明。更近的工作中，專用證明器如 Seed-Prover 1.5（Chen 等，2025）進一步顯示，大規模智能體強化學習與測試時擴展（test-time scaling）可顯著提升在既有基準上的形式化成功率。這些成果表明，形式化證明生成已不再局限于玩具領域，而緊密的工具反饋循環（檢索–生成–驗證）可能成為決定性因素。

盡管神經定理證明取得了穩步進展，當前的形式化基準仍未能充分考察基于庫的、高度抽象的推理能力。廣泛使用的數據集如 miniF2F（Zheng 等，2022）和 FIMO（Liu 等，2023）主要源自奧數風格的問題，而面向大學水平的套件如 ProofNet（Azerbayev 等，2022）和 PutnamBench（Tsoukalas 等，2024）則聚焦于本科競賽或教材內容。這些基準雖具價值，但往往獎勵的是簡短巧妙的技巧或計算能力，而非在豐富抽象框架內持續、系統的推理。相比之下，現代研究型數學以高度普遍性書寫，圍繞可復用的接口組織，并深度依賴龐大的定義與引理庫——其成功較少依賴單一關鍵洞察，而更多取決于對抽象結構的駕馭、定義的管理，以及在長程推理中連貫地組合庫知識的能力。

范疇論為這種能力提供了一個天然的壓力測試：作為現代數學的接口語言——范疇、函子、自然變換、伴隨、極限/余極限、單子等——其形式化證明通常依賴于圖式推理（diagrammatic reasoning）和泛性質（universal-property）推理，即構造具有正確自然性或唯一性保證的態射，并證明各類結構族之間的交換性。然而，現有形式化基準極少直接針對這一抽象層次。

為彌合這一空白，我們提出了 LeanCat——一個包含 100 道在 Lean 4（mathlib）中形式化的范疇論問題的基準，旨在檢驗自動證明器是否能在成熟的庫內部運作并組合高層抽象，而非僅解決孤立的謎題。LeanCat 通過將前沿從抽象代數轉向范疇論，補充了以代數為核心的基準（如 FATE 系列，Jiang 等，2025）。

我們的基線評估揭示了一個顯著的抽象鴻溝：在五個強模型中，表現最佳者在 pass@1 下僅達到 8.25%，在 pass@4 下為 12%；一旦任務涉及庫導航和長程抽象管理，準確率便從“簡單”到“高難”急劇下降（見圖 1）。我們還觀察到，生成看似合理的自然語言論證與生成可編譯的 Lean 代碼之間存在持續差距，凸顯出明顯的“自然語言到形式化”瓶頸（見圖 2）。

據我們所知，LeanCat 是范疇論基準系列的首個組成部分。本文聚焦于 1-范疇理論。我們設想未來將擴展至更豐富的結構，例如幺半范疇（monoidal categories）、富范疇（enriched）與辮范疇（braided）設定，乃至最終的 2-范疇及高階范疇接口。

除基準測試外，我們認為這一方向對以下兩方面具有重要意義：(i) 對人類數學而言，通過厘清哪些抽象庫級推理環節仍難以形式化，以及數學庫在何處需要加強；(ii) 對人工智能而言，通過迫使模型在抽象感知規劃、相關引理檢索和基于編譯反饋的穩健精調等方面取得進展。

我們的主要貢獻總結如下：

? LeanCat 基準（1-范疇）：我們提出了 LeanCat，包含 100 道在 Lean 4（mathlib 4.19.0）中形式化的范疇論問題。任務涵蓋八個主題簇（從基本范疇性質到單子），精心設計以覆蓋可復用的抽象接口，而非競賽式技巧。

? 難度標注流程：我們提出一種結合模型評估與專家判斷的分級方法。每道題目均獲得多個 1–10 分的評分（來自先進 LLM 的嘗試和人類形式化者），并通過賦予人類評分更高權重進行聚合，最終劃分為“簡單/中等/高難”三類（數量分別為 20/42/38）。

? 基線評估：我們在統一條件下對當前最先進的證明器進行基準測試。評估（第 3–4 節）包括 ChatGPT-5.1 和 ChatGPT-5.2（OpenAI, 2025a;b）、Claude 4.5（Anthropic, 2025）、Google 的 Gemini 3 Pro（Gemini Team, Google, 2025）、高級思維鏈推理器 DeepSeek-V3.2-Thinking 與 DeepSeek-V3.2-Speciale（Liu 等, 2025），以及智能體模型 Kimi K2（Kimi K2 Team 等, 2025）。在 pass@1 下，最佳模型解決 8.25% 的 LeanCat 任務；在 pass@4 下，最佳成績為 12%。我們按難度提供詳細分解，并識別出主要失敗模式（庫缺失、抽象不匹配、多步推理停滯）。

? 通過 LeanBridge 實現檢索增強證明：我們評估了一種“檢索–分析–生成–驗證”循環，該流程整合了 mathlib 檢索（通過 LeanExplore）與編譯器反饋，展示了工具增強的工作流如何在部分問題上提升魯棒性。

2 LeanCat 基準設計

2.1 基準結構與內容

數據來源：我們的基準問題分為兩大部分：抽象部分與具體部分：

• 抽象部分：問題主要選自范疇論領域的標準、廣泛使用的教材，特別是《Category Theory in Context》（Riehl, 2017）和《Categories for the Working Mathematician》（Mac Lane, 1998），并包含少量改編自未發表講義（Kong; Zheng）的問題。
• 具體部分：問題主要選自《Abstract and Concrete Categories》（Adámek 等, 1990），該書提供了關于可具體化性、單射性及相關主題的系統性習題。
• 其他：除上述核心來源外，我們還納入了受研究論文及高級社區驅動文獻啟發的問題（Chen, 2021; Adámek 等, 2021）。

每個 LeanCat 問題在陳述層面是自包含的：提供定理的形式化陳述（通常附有非正式描述，如上文“問題列表”所示），且所有必需的定義均存在于 Lean 環境中（或已在 Mathlib 中預置，或作為問題設置的一部分引入）。在可能的情況下，我們借鑒了范疇論文獻中的已知定理；許多任務被專門設計或調整，以檢驗 AI 證明器可能遇到的邊界情況與接口交互。在若干高難度案例中，相關引理并不現成可用，迫使人工形式化者推導中間結果。這一特性使 LeanCat 成為對自動證明器的特別嚴苛測試——它們不能僅依賴現有庫事實的機械套用。

LeanCat 包含 100 個范疇論定理陳述，每個均完全形式化于 Lean 4（即每個問題以 Lean 定理聲明形式給出，所需定義與上下文均已提供）。問題按八個主題簇組織，反映范疇論的核心領域：

• 基本范疇性質（問題 1–18）：關于范疇與態射的基本結論，包括單態射與滿態射的性質、始對象/終對象、冪等元分解，以及范疇構造示例。
• 伴隨函子（問題 19–29）：涉及伴隨函子的構造與判定，這是范疇論的核心概念。問題包括證明熟悉函子具有左/右伴隨，以及通用伴隨性準則（如逗號范疇條件，問題 19）和具體實例（問題 28）。這些任務檢驗證明器操作普遍性質、在逐點推理與圖式推理間切換的能力。
• 反射與余反射子范疇（問題 30–33）：關于一類特殊子范疇的抽象性質與具體示例（例如，對 Set 和 Top^CH 的反射子范疇進行分類）。
• 具體范疇（問題 34–41）：具有忠實遺忘函子到集合范疇及相關概念的范疇。這些問題高度具體，與拓撲學、序理論、集合論等數學領域大量重疊。其設計旨在檢驗模型將抽象概念與具體例子聯系起來的能力。
• 極限與余極限（問題 42–73）：這是最大的簇，涵蓋極限、余極限及相關范疇構造的一系列結果。其中許多陳述處于 Lean 的 Mathlib 當前覆蓋范圍的前沿，某些（如問題 46 或 67）甚至需要開發新的形式化定義。該簇強調證明器串聯多個范疇事實的能力。
• 余完備化（問題 74–78）：本部分基于最近關于余完備化的研究成果。它要求 LLM 引入新定義，然后證明建立在這些定義之上的關鍵定理——而這些定理目前在 Mathlib 中尚不存在。
• 阿貝爾范疇（問題 79–90）：涉及阿貝爾范疇與同調代數概念的任務。阿貝爾范疇是高度結構化的范疇（每個態射均有核與余核等），推廣了模范疇或阿貝爾群范疇。這些陳述鏡像同調代數的標準結果，但將其形式化于 Lean 需要謹慎處理比集合論對應物更復雜的范疇抽象（如核對象、正合序列）。解決它們可能需要證明器引入關于核、像或正合性的創造性輔助引理——這對自動化工具而言是一項艱巨任務。
• 單子（問題 91–100）：最后一個簇聚焦于單子及其相關構造（克萊斯利與艾倫伯格-摩爾范疇）。單子是一個高層概念，封裝了一種“計算”或結構的形式；在 Lean 中證明其性質通常要求雙層推理（既推理單子的代數定律，也推理范疇論條件，如余等化子保持性）。該簇為 AI 在范疇論背景下處理高度抽象代數結構的能力提供了寶貴測試。

2.2 精選工作流

LeanCat 通過一個三階段工作流構建而成，融合了專家篩選、LLM 輔助起草與嚴謹的人工驗證：

1. 收集。三位范疇論專家從既定資源中（如上所述）篩選候選問題，旨在覆蓋核心接口（如伴隨、極限/余極限、單子）與代表性證明模式（圖追逐、泛性質、自然性）。
2. 形式化。對于每個選定的問題，我們首先使用多個 LLM 起草 Lean 4 語句。隨后由這三位范疇論專家審核草稿，僅保留語義正確的形式化陳述。對于模型未能生成正確陳述的問題，我們在西萊克大學組織了一場為期三天的工作坊，召集 Lean 專家共同撰寫缺失的陳述，并（在可行時）編寫相應證明。
3. 評審。最后，兩位具備扎實數學背景與 Lean 專業知識的獨立評審員進行全面一致性檢查，確認編譯無誤、修正定義不匹配，并確保形式化陳述準確表達預期的數學含義。

陳述級任務。LeanCat 是一個陳述級基準：每項任務僅包含一個需證明的獨立定理，而非逐步引導至最終目標的中間引理序列。此設計旨在評估通用的、基于庫的證明能力——檢索、定義管理、抽象導航——而非獎勵針對特定問題的提示工程。

范圍與難度。總體而言，LeanCat 在范疇論主題覆蓋上廣博，在深度上深入：即使看似簡單的定理也可能需要分層抽象與對可復用接口的細致運用，從而映射數學家在大型形式化庫內工作的實際方式。

形式化標準。所有基準文件遵循嚴格統一的規范：(i) 每個 Lean 文件在最終定理后恰好包含一個 sorry；(ii) 自然語言問題描述（LaTeX 格式）作為注釋緊跟在形式化語句之前；(iii) 宇宙層級被明確固定，以避免范疇論發展中常見的歧義與不穩定性。

2.3 難度標注流程

我們并未單純依賴問題作者的直覺，而是實施了一套系統化的“LLM+人工”評分流程，以10分制對問題難度進行評分，再將分數劃分為三個等級：簡單、中等和高難。該方法旨在同時捕捉人類專家與自動化求解器的視角，其精神類似于 FATE 的精選流程（結合專家判斷與模型反饋進行難度排序）。

我們的流程如下：

• LLM 難度評分：對每個模型而言，若其生成了正確證明，則貢獻一個“證明分”；若該模型尚未有正確證明，但其生成了正確的陳述，則貢獻一個較小的“陳述分”。一個問題的總分是所有模型貢獻的加權和；難度則定義為 Diff = max(0, 10 - PF 分數 - ST 分數)，因此未被任何模型解決的問題難度為10，而所有證明列均為綠色（即所有模型均成功）的問題難度為0。
• 人工難度評分：與此同時，兩位具備 Lean 專業知識和范疇論背景的人類數學家，獨立地在相同的1–10分難度尺度上對每個問題進行評分。他們考慮的因素包括證明長度、論證復雜性，以及是否需要非顯而易見的引理。人工評分往往與直覺相符：例如，一個簡單的圖追逐可能評分為2/10，而一個跨越多個定義的復雜構造可能評分為9/10。
• 聚合：我們將評分合并，賦予人工評分和 LLM 評分各50%的權重。最終，我們將數值分數映射到難度類別。我們根據分數分布設定了閾值：大致而言，≤6 分為“簡單”，≥8.5 分為“高難”，其余為“中等”。這些切分點清晰地將數據集劃分為 20 個簡單題、42 個中等題和 38 個高難題，詳見表4。

這種聯合標注程序比單一專家分類提供了更豐富的洞察。它有效地將大模型作為“第二意見評分者”。由此產生的難度標簽已在分析中證明具有實用價值：例如，最佳模型所解決的全部七個問題（第4節）均來自“簡單”集合；而得分 ≥9（即“最難的高難”題）的所有問題，在所有模型中均無一成功——這是我們的難度排名與實際可解性相一致的量化證據。

3 實驗與結果
3.1 評估協議

我們在 LeanCat 上采用標準化的 pass@k 協議評估證明器性能，該協議借鑒了代碼生成與自動定理證明領域的先前工作。具體而言，對于每個模型–問題對，我們在相同的提示和工具設置下最多采樣 k 次獨立的證明嘗試；只要其中任意一次嘗試能夠成功編譯并通過驗證，即視為該問題已解決。我們同時報告 pass@1 和 pass@4：pass@1 反映單次嘗試的可靠性，而 pass@4 則體現有限采樣和迭代多樣性帶來的收益。除非另有說明，所有評估均在相同條件下進行（包括相同的模型設置、上下文長度限制和驗證流程），以確保模型間的可比性。

環境與輸入：每個 LeanCat 問題均以統一格式提供給模型：我們給出完整的 Lean 形式化陳述（包括精確的定理名稱、假設和結論），以及相關上下文，如導入的庫和定義。因此，模型所看到的形式化目標與人類使用 Lean 時所見完全一致。不提供任何非形式化提示或分解后的中間引理——模型必須僅憑定理陳述和標準庫知識自行構造證明。該設置模擬了一個現實場景：AI 證明器被要求在僅給定定義的情況下證明一個新定理。

自動證明生成：
語言模型作為證明器：對于基于 API 的大語言模型（如 GPT-5.2、Claude、Gemini），我們直接提示模型生成 Lean 證明腳本。為保持評估一致性，我們采用與 FATE-Eval（Jiang 等，2025）相同的提示模板（見清單 1）。模型輸出一個證明項或策略腳本，隨后我們將其送入 Lean 進行驗證。

驗證：若 Lean 定理證明器接受某次證明嘗試作為給定陳述的有效證明，則該嘗試被視為成功。我們對 Lean 進行了自動化封裝，以自動檢查模型輸出。如果模型輸出不完整或不正確（無法通過類型檢查），則該次嘗試計為失敗。在 pass@k 評估中，模型不會“看到”驗證結果；每次嘗試彼此獨立。

Pass@k 計算：我們計算 pass@1 為模型在單次嘗試中生成正確證明的問題所占比例。pass@4 則為在四次嘗試中至少有一次成功的問題所占比例。由于 LeanCat 包含 100 道問題，這些百分比可直接對應解決的問題數量。我們注意到，LeanCat 中的所有問題權重大致相等（每道題均為一個獨立定理），因此簡單的通過率是衡量整體能力的有效指標。我們還分別統計每個難度類別（簡單/中等/高難）內的 pass@1，以觀察性能隨難度增加而下降的情況。

我們采用統一的評估設置：每次嘗試的輸出上限為 50,000 個 token，Lean 驗證時間限制為 5 分鐘；所有模型均在同一 Lean 環境（Lean 4 + Mathlib 4.19.0）下運行，以確保一致性。若模型超出 token 預算或未能在時限內完成驗證，則該次嘗試計為失敗。然而在實踐中，這些資源限制很少成為決定性因素：大多數嘗試要么迅速找到證明（通常在 30 秒內，除 DeepSeek 等推理模型外），要么幾乎立即陷入停滯（往往僅生成幾十個 token 后即失敗）。

我們強調，pass@4 并非意在模擬真實使用場景（現實中不會對每個定理運行模型四次）；而是提供一種樂觀的上界估計——假設我們能從少量模型嘗試中完美挑選出最佳結果。在理想情況下（各次嘗試相互獨立），pass@4 可能顯著高于 pass@1。但如我們將看到的，LeanCat 中的提升幅度相當有限。這表明，當模型在一次嘗試中失敗時，除非采用不同策略進行引導，否則重復嘗試通常會得到相似的結果。

初步數據顯示，對于表現最好的模型，從 pass@1 到 pass@4 僅增加了 1–2 道題的解決數量，進一步印證了 LeanCat 任務的高難度。

LeanBridge：LeanBridge 實現了一個“檢索–分析–生成–驗證”循環，通過集成 Mathlib 檢索和驗證器反饋來增強大語言模型。給定一個問題，我們首先使用其自然語言陳述作為查詢，通過 LeanExplore 檢索相關的 Mathlib 實體（如定義、引理）。隨后，將檢索到的代碼片段作為上下文提供給模型，用于分析并生成 Lean 證明代碼。

每份生成的證明腳本都會在一個干凈的 Lean 環境中進行檢查；只有當腳本能通過類型檢查且不包含 sorry 或 admit 時，才被視為候選解。為防止出現表面“通過”但語義不符的淺層證明，所有被接受的候選解還需由人類專家進一步審核，確保其在語義上與原始問題陳述一致。

若驗證失敗，LeanBridge 會解析編譯器返回的錯誤信息，判斷是否需要進一步檢索；然后將新檢索到的信息與驗證器反饋一并加入上下文，并提示模型修改證明。除非另有說明，該循環在以下兩個階段均最多執行 4 次迭代：(i) 自然語言到形式化陳述的轉換，以及 (ii) 自然語言定理的證明生成。

3.2 基線結果與分析

我們在上述協議下評估了五個最先進的模型在 LeanCat 上的表現。主要發現總結如下：

• 整體成功率仍較低。在 pass@1（首次嘗試）中，最佳模型（Claude Opus 4.5）解決了 8.25% 的問題；GPT-5.2 解決 5.5%，DeepSeek Reasoner 解決 4%，Gemini 3 Pro 為 3.25%，Kimi 為 2%。所有模型中，僅有 10 道不同的題目在首次嘗試時被至少一個模型解決，意味著 91.75% 的題目在 pass@1 下未被解決。允許每題最多四次嘗試可提升結果，但未改變整體格局：Claude Opus 4.5 的 pass@4 達到 12%，DeepSeek Reasoner 為 9%，Gemini 3 Pro 為 8%，GPT-5.2 為 7%，Kimi 為 4%。總計，在 pass@4 下有 14 道不同題目被至少一個模型解決。
• 清晰的“簡單–中等–高難”差距。性能隨我們標注的難度等級單調下降。例如，Claude Opus 4.5 在簡單題上 pass@1 達到 32.5%，中等題為 4.17%，高難題為 0%（pass@4 分別為 50%、4.76%、0%）。GPT-5.2 呈現相似趨勢（pass@1 下分別為 27.5%、0%、0%）。即使在“簡單”子集中，絕對成功率也遠未飽和，表明一旦需要非平凡的抽象和庫導航，LeanCat 的“基礎難度”已超出當前模型穩定處理的能力范圍。
• 案例研究（典型成功）：問題 82。該問題能被有效將范疇論“簡潔性”概念轉化為具體線性代數的模型穩定解決。成功的解法認識到：在向量空間范疇 Vect? 中，一個簡潔對象必須是一維的，然后利用一個非零向量和簡潔性條件構造出一個顯式的同構。該證明優雅地連接了抽象范疇論與初等向量空間性質，展示了對結構化定義如何在具體范疇中體現的清晰理解。
• 重試僅部分有效，表明搜索方差大且脆弱。從 pass@1 到 pass@4，最強模型僅獲得微小的絕對提升（Claude Opus 4.5 +5），但顯著提升了某些較弱模型（如 DeepSeek Reasoner 從 3 提升至 8）。這一模式符合高方差行為：許多問題要么迅速解決，要么完全無法有效處理；額外嘗試僅在模型恰好采樣到可行策略或召回正確庫引理時才有幫助。
• 錯誤分析：庫知識缺口為主導，其次是抽象錯配與計劃不完整。對失敗運行的人工檢查揭示了三種反復出現的失敗模式：(i) 庫知識缺口：模型常無法回憶正確的 Mathlib 定義/引理或其可用形式，導致陷入死胡同或捏造引理名稱；(ii) 抽象錯配：當預期證明是范疇/結構化的時，部分嘗試轉向逐點推理，這在 Lean 中通常無效，除非具備充分的上下文設置；(iii) 多步計劃不完整：模型可能提出幾個局部目標后便停滯，無法將中間事實整合成連貫的端到端證明。純語法層面的錯誤確實存在，但比這些語義/策略性失敗更少見。

總體而言，這些基線結果證實：相較于早期的 Lean 基準，LeanCat 對當前基于 LLM 的證明器要困難得多。即使進行多次嘗試，中等/高難題的成功率依然稀少，這指向對改進的庫檢索、更好的抽象感知證明規劃以及更可靠的策略探索的需求。

4 討論與未來工作

LeanCat 作為基準（及其系列）：
LeanCat 旨在成為抽象數學中基于大語言模型的定理證明的一個可復用檢查點。本文介紹了 LeanCat-1（1-范疇理論），并將其視為更廣泛的 LeanCat 系列的首個組成部分。我們計劃后續擴展至更豐富的范疇接口，例如幺半范疇（monoidal categories）和高階范疇結構（如雙范疇 / 嚴格 2-范疇），這些結構已在 Mathlib 生態系統中有所體現。

庫集成：
所有 LeanCat 問題均在 Lean 4 中形式化；隨著解決方案被發現，它們可被合并回 Mathlib，從而形成一個反饋循環：基準 → 解決方案 → 更強大的庫與求解器 → 剩余更難的前沿問題。

LeanCat 所強調的能力：
我們的結果凸顯了當前自動證明器面臨的三個持續性瓶頸：(i) 庫感知能力（查找并應用正確的 Mathlib 引理）；(ii) 抽象控制能力（保持在恰當的范疇層級進行推理，而非滑向逐點/元素級推理）；(iii) 長程一致性（在多個相互依賴的步驟中維持連貫的證明計劃）。

未來工作與更廣泛影響：
在基準方面，我們將把 LeanCat 從 1-范疇擴展至更多主題簇和多定理任務，并逐步覆蓋更高層次的抽象——例如增設“幺半范疇”軌道和“2-范疇”軌道（其中幺半范疇可通過單對象雙范疇的視角理解），從而在抽象程度提升時更精細地診斷證明器失敗的具體環節。

在求解器方面，有前景的方向包括：對 Mathlib 的更強檢索能力、將證明分解為輔助引理的分層策略，以及多智能體流水線（規劃器/驗證器/引理建議器）。

對人類數學而言，我們期望 LeanCat 式的檢查點能幫助識別庫中缺失的接口和可復用引理，指導形式化工作的優先級；對人工智能而言，它們為提升“抽象感知規劃”和“基于庫的推理”能力提供了具體目標。

最后，將 LeanCat 移植到其他證明助手（如 Coq 或 Isabelle）將支持跨系統的比較，并促進證明工程方法的遷移與共享。

原文：https://www.arxiv.org/pdf/2512.24796