Repolode
提交项目
lean-dojo

lean-dojo/LeanCopilot

为 Lean 定理证明器提供基于大语言模型的证明自动化，包括策略建议、证明搜索和前提选择。

在 GitHub 查看官网
Star
1,341
Fork
129
未关闭 Issue
0
最近提交
25天前

这是什么？

Lean Copilot 让大语言模型直接运行在 Lean 4 定理证明器中，用于辅助编写形式化证明。它提供 suggest_tactics 生成下一步证明策略，search_proof 结合 aesop 搜索多步证明，以及 select_premises 从 Lean 和 mathlib4 中检索可能有用的前提。

项目内置了来自 LeanDojo 的模型，可从 Hugging Face 下载，并通过 CTranslate2 在本地运行，支持有或没有 GPU 的环境。用户也可以通过通用的生成器和编码器接口，或外部 API 服务器接入自己的本地或远程模型。

Lean Copilot 以 Lean 包的形式通过 lakefile 配置引入，要求 Lean 版本至少为 v4.3.0-rc2，支持 Linux、macOS、Windows 和 WSL。

核心功能

  • 01根据当前证明状态生成策略建议，可用前缀约束输出。
  • 02结合 LLM 生成的策略与 aesop 搜索多步证明。
  • 03借助 LeanDojo 检索器从 Lean 和 mathlib4 中选取相关前提。
  • 04通过 CTranslate2 在本地运行内置或自定义模型，也可接入远程外部 API。
  • 05提供通用的 LLM 推理接口，可用于定理证明之外的场景。

适用场景

  • 在编写 Lean 证明时获取下一步策略建议。
  • 自动搜索简单目标的多步证明。
  • 在不知道引理名称时，从 mathlib4 中查找相关定理。
  • 在 Lean 内构建基于 LLM 的自定义证明自动化或其他应用。

快速上手

  1. 1

    在 lakefile 中添加 LeanCopilot 依赖声明

  2. 2

    获取 LeanCopilot 包

    lake update LeanCopilot
  3. 3

    从 Hugging Face 下载内置模型

    lake exe LeanCopilot/download
  4. 4

    构建你的项目

    lake build

使用前须知

  • 需要 Lean 版本至少为 lean4:v4.3.0-rc2。
  • 在 Linux 上，lean_exe 目标需要额外的链接器配置才能构建。
  • search_proof 有时会生成错误的证明。
  • select_premises 仅覆盖 Lean 和 mathlib4 的固定快照。

收录于专题

本地运行大模型

标签

#lean#theorem-proving#llm#formal-verification#mathematics#ctranslate2#formal-mathematics#lean4#llm-inference#machine-learning

常见问题

LeanCopilot 是什么？
为 Lean 定理证明器提供基于大语言模型的证明自动化，包括策略建议、证明搜索和前提选择。 Lean Copilot 让大语言模型直接运行在 Lean 4 定理证明器中，用于辅助编写形式化证明。它提供 suggest_tactics 生成下一步证明策略，search_proof 结合 aesop 搜索多步证明，以及 select_premises 从 Lean 和 mathlib4 中检索可能有用的前提。
LeanCopilot 可以免费使用吗？用的什么许可证？
LeanCopilot 以 MIT 许可证开源。用于商业产品前，请先确认许可证条款。
LeanCopilot 还在维护吗？
活跃维护中。LeanCopilot 最近一次提交是在 2026年10月13日。
LeanCopilot 适合用来做什么？
在编写 Lean 证明时获取下一步策略建议。 自动搜索简单目标的多步证明。 在不知道引理名称时，从 mathlib4 中查找相关定理。 在 Lean 内构建基于 LLM 的自定义证明自动化或其他应用。
LeanCopilot 怎么安装和运行？
在 lakefile 中添加 LeanCopilot 依赖声明 获取 LeanCopilot 包: lake update LeanCopilot 从 Hugging Face 下载内置模型: lake exe LeanCopilot/download 构建你的项目: lake build
在哪里获取 LeanCopilot？
源代码和安装说明在 GitHub 上：https://github.com/lean-dojo/LeanCopilot

概要由 AI 根据项目 README 生成；GitHub 数据每日更新。

相关项目