lean-dojo/LeanCopilot

解決的問題

Lean Copilot 將大型語言模型（LLMs）直接整合至 Lean 定理證明器中，自動化形式化證明構建中繁瑣的部分。它透過建議證明的下一步，或自動搜尋完整證明，幫助使用者克服「空白頁面」的困境。

工作原理

本專案在 Lean 與 LLM 之間提供原生橋接。使用者可透過 CTranslate2 在本機執行模型，或透過 API 連接遠端模型。它實現了三個主要功能：

• 策略建議：產生可用於推進證明的潛在下一步策略，使用者可點擊套用。
• 證明搜尋：將 LLM 生成的策略與 aesop 搜尋引擎結合，尋找多步證明。
• 前提選擇：使用檢索模型從 Lean 和 mathlib4 中識別與目前目標相關的有用數學前提。

適用對象

專為使用 Lean 定理證明器的數學家與電腦科學家設計，希望藉由 AI 協助加速形式化工作。

主要亮點

• 彈性的模型支援：支援 LeanDojo 內建模型、本機模型（含或不含 GPU）、以及自訂遠端模型。
• 原生整合：作為 Lean 依賴項運作，允許使用者直接在 Lean 編輯器中觸發 LLM 推理。
• 可擴展的 API：提供 TextToText 與 TextToVec 接口，讓開發者可在 Lean 中建構自訂證明自動化或其他基於 LLM 的應用程式。
• 跨平台支援：支援 Linux、macOS 與 Windows（含 WSL）。