LeanCopilot：把 LLM 拉進 Lean 4 的 tactic 迴圈
LLMs as Copilots for Theorem Proving in Lean
秒懂
- 它是什麼？
- LeanCopilot 讓大型語言模型以原生 tactic 的形式在 Lean 4 中運作，提供 tactic 建議、結合 aesop 的多步證明搜尋與前提檢索。本文整理它的依賴設定、模型下載流程、可換模型的介面，以及版本綁定與硬體需求帶來的實際限制。
- 適合誰用？
- LeanCopilot 適合已經在使用 Lean 4 與 mathlib4、且願意被綁在特定 Lean 版本上的團隊或個人；如果你的專案需要頻繁升級 Lean 或依賴 nightly 版本，維護成本會直接落在你身上，因為套件版本必須與 Lean 版本對齊。若你只是想要一個獨立的聊天式助手，或不想處理 Git LFS、CUDA 與 ctranslate2 連結設定，這個專案不是合適的起點。
- 可以商用嗎？
- 可以。MIT 是寬鬆授權：你可以使用、修改並販售以它為基礎的軟體，只需保留著作權與授權聲明。
- 還在維護嗎？
- 有在維護。儲存庫最近一次提交在 1 天前。
- 用什麼語言寫的？
- 主要是 C++（依據 GitHub 的語言統計）。
以上回答依據專案的 GitHub 資料（最近同步於 2026年9月15日）與我們的分析，不構成法律意見。
開源專案深度解析
LeanCopilot 要解的是編輯器裡那個空白的證明狀態
寫 Lean 4 的人多半遇過同一種停頓：目標就在眼前，tactic 名稱也想得到幾個，但要一個一個試，或者要翻 mathlib4 找那個名字記不全的引理。LeanCopilot 把這個停頓當成主要問題，做法是把 LLM 的推論直接接進 Lean 的 tactic 系統，讓模型產生的東西以 tactic 的形式出現在證明腳本裡，而不是出現在另一個視窗、需要人手動複製貼上。
它的目標使用者寫得很明確：已經在用 Lean 4 做形式化數學的人，以及想拿 Lean 當平台去測 LLM 證明能力的研究者。README 的第一段把範圍講清楚了，除了建議 tactic 與前提，還包括搜尋證明；同時允許使用 LeanDojo 內建的模型，或自帶模型在本機（有無 GPU 皆可）或雲端執行。
這裡有個容易忽略的定位差異。它不是把 LLM 當成一個外部服務來呼叫，而是要求你的 Lean 專案把 LeanCopilot 當成 dependency 拉進來。也就是說，你換來的是原生整合，付出的是專案結構上的耦合。
三個 tactic 與一個推論介面：實際的資料流
從 README 可見的介面來看，LeanCopilot 提供三種 tactic，加上一個通用的 LLM 執行入口。
suggest_tactics 產生 tactic 建議，使用者可以點選其中一條直接套用到證明中。它支援前綴約束，README 給的例子是傳入 simp 來限制生成結果的走向，這在實際使用上比無約束生成實用得多，因為 Lean 的 tactic 空間很大，能先縮小範圍就少掉很多無效候選。
search_proof 把 LLM 生成的 tactic 與 aesop 結合，用來搜尋多步證明。這是一個明確的架構決定：LLM 負責提出候選，aesop 負責在搜尋空間裡展開與收斂。找到證明之後，使用者可以點選把它插入編輯器。
select_premises 回傳一份可能有用的前提清單。README 說它目前使用 LeanDojo 的 retriever，從 Lean 與 mathlib4 的固定快照中挑選前提，並在敘述中附上該 mathlib4 快照的 commit hash。這一點值得留意：檢索的範圍是凍結的，不是跟著你專案當下的 mathlib4 版本走。
最後是執行任意 LLM 推論的能力。README 明講這個入口不限於定理證明，可以用來建構自訂的證明自動化或其他 LLM 應用。模型可以跑在本機，也可以跑在遠端。
把 LeanCopilot 掛進 lakefile：那些不能漏的設定
安裝流程有幾個步驟是不能省略的，漏掉任何一個都會在建置階段出問題。
第一步是連結參數。你必須在 lakefile.lean 的 package 區塊加入 moreLinkArgs，內容是 -L./.lake/packages/LeanCopilot/.lake/build/lib 與 -lctranslate2 兩個參數。README 給的範例是：
package «my-package» { moreLinkArgs := #[ "-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2" ] }
如果你的專案用 lakefile.toml，對應寫法是 moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]。這兩個參數之所以必要，是因為底層推論依賴 ctranslate2，連結階段要能找到它。
第二步是宣告依賴。在 lakefile.lean 中加入 require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"，引號要保留。版本怎麼填，README 給了明確規則：穩定版 Lean（例如 v4.33.0）就把 LEAN_COPILOT_VERSION 設成該版本；最新不穩定版 Lean（例如 v4.34.0-rc1）則設成 main。兩種情況都要確認與 mathlib 等其他依賴相容。若用 lakefile.toml，改寫成 [[require]] 區塊，欄位是 name、git 與 rev。
第三步，原生 Windows 使用者要把 <path_to_your_project>/.lake/packages/LeanCopilot/.lake/build/lib 加進系統環境變數 Path。
接著執行 lake update LeanCopilot，再執行 lake exe LeanCopilot/download，把內建模型從 Hugging Face 下載到 ~/.cache/lean_copilot/。README 也提供手動下載的替代路徑，對應四個模型倉庫：ct2-leandojo-lean4-tacgen-byt5-small、ct2-leandojo-lean4-retriever-byt5-small、premise-embeddings-leandojo-lean4-retriever-byt5-small、ct2-byt5-small。最後跑 lake build。
前置條件方面，README 列出 Git LFS，以及選用但建議的 CUDA 與 cuDNN。若你是直接建置 LeanCopilot 本身而非下游套件，還需要 CMake 3.7 以上與支援 C++17 的編譯器。下游套件通常下載預建版本，但在沒有發布預建檔的平台上（README 舉的例子是 Intel macOS）會自動退回從原始碼建置，這時前述工具鏈就變成必需。
自帶模型與預建系統庫：進階使用者才碰的兩條路
README 把 Advanced Usage 明確標示為進階使用者專屬，用途是改動 suggest_tactics、search_proof 或 select_premises 的預設行為，例如換模型或調超參數。
Tactic APIs 這條線的文件指向 LeanCopilotTests/TacticSuggestion.lean，裡面示範如何設定 suggest_tactics，包括指定不同模型與調整生成數量等。這意味著預設模型並非唯一選項，tactic 層是可參數化的。
Model APIs 與 Bring Your Own Model 則是更底層的替換點。搭配前面提到的通用 LLM 推論入口，這條路讓你把推論後端換成本機模型或雲端服務，而不必改動 Lean 這一側的呼叫方式。
還有一項 Using Prebuilt System Libraries。這對在意建置時間的人有實際意義：C++ 專案的完整建置成本不低，能沿用系統既有函式庫就能省下部分時間。不過 README 的清理版本在這一段沒有展開細節，實際可用範圍需要回到倉庫原文確認。
整體來看，這套介面的設計意圖是分層：最上層是三個開箱即用的 tactic，中間是可以調參數的 tactic API，底層是可以整組換掉的模型介面。三層的門檻遞增，對只想試用的人來說，停在第一層就夠了。
版本綁定與平台落差：這個套件最硬的三個限制
第一個限制是 Lean 版本。README 用警告標示專案必須使用至少 lean4:v4.3.0-rc2，而依賴宣告的版本規則又把套件版本與 Lean 版本綁在一起。穩定版對穩定版，不穩定版對 main。這代表你無法自由選擇 LeanCopilot 的版本，只能選擇與你 Lean 版本相容的那一個。
第二個限制是檢索範圍。select_premises 從 Lean 與 mathlib4 的固定快照中挑選前提，README 直接列出該快照的 commit hash。如果你的專案用的是更新的 mathlib4，檢索回傳的引理名稱未必與你當下的環境一致。這不是錯誤，而是設計上的取捨：固定快照讓模型與嵌入索引可以預先算好，代價是與最新 mathlib4 之間存在落差。
第三個限制是平台。支援平台列為 Linux（優先）、macOS（優先）、Windows 與 Windows WSL。括號裡的「優先」是作者自己標的，說明不同平台受到的關注程度不同。原生 Windows 還需要額外設定 Path 環境變數。至於 Intel macOS，README 明說沒有發布預建檔，會自動退回從原始碼建置。
還有一個 README 自己承認的區塊叫 Caveats。清理後的版本只保留了標題，內容沒有出現在提供的材料裡。這是必須誠實說明的地方：這一段的具體警告我無法從手邊材料確認，讀者應該直接去看倉庫原文。
與 IDE 外掛式 AI 補全的差別在哪
把 LLM 接進證明助理，最直覺的替代方案是在編輯器外掛裡做補全：模型看到游標附近的文字，回傳一段建議，使用者按 Tab 接受。Copilot 這類工具就是這個模式。
差別在於回饋迴路的位置。外掛式補全的模型看不到 Lean 的證明狀態，它看到的是文字。LeanCopilot 的 tactic 是在 Lean 內部執行的，search_proof 能把 LLM 生成的 tactic 交給 aesop 去實際展開搜尋，這件事在外掛模式裡做不到，因為外掛沒有辦法驅動 Lean 的 tactic 引擎。
代價是耦合。外掛可以對任何語言、任何專案生效，裝了就用；LeanCopilot 要求你的專案宣告依賴、設定連結參數、下載模型、通過建置。前者是低摩擦低上限，後者是高摩擦但能碰到證明狀態。
還有一個方向相反的替代方案：完全不使用 LLM，只依靠 aesop、simp 這類既有自動化。對許多常規引理來說這已經足夠，而且沒有模型下載與 GPU 的負擔。LeanCopilot 的 search_proof 本身就把 aesop 當成搜尋引擎，這也側面說明兩者不是互斥關係。
維護成本與授權：導入前該算的帳
維護成本主要來自版本對齊。Lean 生態的版本迭代速度快，README 的版本規則要求你的 LEAN_COPILOT_VERSION 與 Lean 版本匹配，並且要與 mathlib 等依賴相容。倉庫的發布節奏看起來相當密集，從提供的資料可見 2026 年 6 月到 8 月之間就有三個版本（v4.31.0、v4.32.0、v4.33.0），其中兩個相隔不到一天。對使用者來說，這既代表上游跟得緊，也代表你每隔一段時間就要重新對齊一次。
建置成本則取決於你是否需要從原始碼編譯。下游套件通常下載預建版本，但在沒有預建檔的平台上會退回原始碼建置，此時 CMake 3.7 以上與 C++17 編譯器就成為必要條件。
模型檔案是另一筆成本。內建模型需要透過 lake exe LeanCopilot/download 下載到 ~/.cache/lean_copilot/，加上 Git LFS 的前置要求，首次設定的時間不會太短。若改用自帶模型，成本轉移到模型本身的部署與推論資源上。
授權是 MIT。這是寬鬆授權，允許修改與再散布，通常只需要保留著作權與授權聲明。但這裡只談套件本身：內建模型是從 Hugging Face 上的個別倉庫下載的，那些倉庫可能有各自的授權條款，與 LeanCopilot 的 MIT 是兩回事。要用於商業情境的話，模型那一側的條款需要另外確認。以上是一般性說明，不構成法律意見。
編輯結論
LeanCopilot 適合已經在使用 Lean 4 與 mathlib4、且願意被綁在特定 Lean 版本上的團隊或個人；如果你的專案需要頻繁升級 Lean 或依賴 nightly 版本，維護成本會直接落在你身上，因為套件版本必須與 Lean 版本對齊。若你只是想要一個獨立的聊天式助手，或不想處理 Git LFS、CUDA 與 ctranslate2 連結設定，這個專案不是合適的起點。導入前先確認三件事：你的 lakefile 是否已加入 moreLinkArgs 與 -lctranslate2、lake exe LeanCopilot/download 是否能成功把模型放進 ~/.cache/lean_copilot/、以及你鎖定的 Lean 版本在倉庫中是否有對應的 release 標籤。
社群筆記