LeanCopilot：把 LLM 推理塞进 Lean 的 tactic 层
LLMs as Copilots for Theorem Proving in Lean
秒懂
- 它是什么？
- LeanCopilot 让 Lean 4 项目通过 lakefile 链接一个 C++ 推理库，在证明脚本里直接调用 suggest_tactics、search_proof、select_premises。它的价值在于把模型推理做成 tactic 而不是外部脚本，代价是版本必须与 Lean 和 mathlib 严格对齐。
- 适合谁用？
- LeanCopilot 适合已经在 Lean 4 上维护 mathlib 依赖、并且愿意把推理运行时作为构建产物一起管理的团队；如果你的项目还在 Lean 4.3.0-rc2 之前的版本，或者你无法接受把 Hugging Face 模型缓存到 ~/.cache/lean_copilot/ 并链接 ctranslate2，那它就不是合适的工具，此时用命令行调用外部模型的脚本更省事。决定采用前先做三件事：确认 lakefile 里 moreLinkArgs 的 -L 路径与实际包路径一致，确认 LEAN_COPILOT_VERSION 与 mathlib 的 Lean 版本能同时编译通过，以及确认 select_premises 依赖的 mathlib 快照是否覆盖你需要的定义。
- 能商用吗？
- 可以。MIT 是宽松许可证：你可以使用、修改并销售基于它的软件，只需保留版权和许可证声明。
- 还在维护吗？
- 在维护。仓库最近一次提交在 1 天前。
- 用什么语言写的？
- 主要是 C++（依据 GitHub 的语言统计）。
以上回答依据项目的 GitHub 数据（最近同步于 2026年9月15日）和我们的分析，不构成法律意见。
开源项目深度解析
它解决的是交互式证明里的哪一段空白
在 Lean 4 里写证明，瓶颈通常不在最后一步的化简，而在「下一步该用哪个引理、哪个 tactic」这个反复试错的过程。mathlib 的规模让 premise 检索变成人力难以穷举的工作，aesop 这类自动化又依赖预先写好的规则集。LeanCopilot 的定位是把语言模型接到这个环节上：README 写明它允许 LLM 在 Lean 中「natively」用于证明自动化，具体形态是建议 tactic、建议 premise、以及搜索多步证明。目标用户是已经在 Lean 4 项目里工作的研究者与形式化工程师，不是想学 Lean 的初学者，因为所有入口都是 tactic，前提是你能读懂当前 goal。
三个 tactic 各自做什么，边界在哪里
suggest_tactics 生成候选 tactic，README 的示例截图里可以点击其中一条直接插入证明；它还接受前缀参数，例如传入 simp 就把生成约束在 simp 系列上。search_proof 把 LLM 生成的 tactic 与 aesop 组合起来搜索多步证明，找到后同样可以点击插入。select_premises 返回一批可能有用的 premise，依据是 LeanDojo 的 retriever，检索范围是 Lean 与 mathlib4 的一个固定快照，README 给出了该快照的 commit。这三者的能力差别值得说清楚：suggest_tactics 和 search_proof 面向「写下一步」，select_premises 面向「找已有引理」。固定快照这一点是硬约束，如果你的证明依赖快照之后新增的定义，检索结果里不会出现它。
模型推理是怎么进到 Lean 进程里的
LeanCopilot 的主体是 C++，README 说明它使用 ctranslate2 作为推理后端，这也是 lakefile 里必须写 -lctranslate2 的原因。模型不是 Lean 代码，而是 CTranslate2 格式的预编译模型，通过 lake exe LeanCopilot/download 从 Hugging Face 拉到 ~/.cache/lean_copilot/。README 列出的内置模型包括 ct2-leandojo-lean4-tacgen-byt5-small 和 ct2-leandojo-lean4-retriever-byt5-small，以及对应的 premise 嵌入模型。架构上这是一个链接进 Lean 可执行文件的本地推理库，不是通过 HTTP 访问的服务，因此 GPU 加速与否取决于是否装了 CUDA 和 cuDNN，README 把这两项列为可选但推荐。它也支持把模型放到云端，或者自带模型，README 的 Advanced Usage 一节说明这是给想改默认行为的高级用户准备的。
接入一个 Lean 包需要改哪几行
接入分两步，先改 lakefile，再拉模型。lakefile.lean 里要加 moreLinkArgs，README 给的写法是 #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]；如果用 lakefile.toml，对应键是 moreLinkArgs 数组。然后是依赖声明，lakefile.lean 里写 require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"，稳定 Lean 版本填具体版本号如 v4.33.0，最新的不稳定版本填 main。之后依次执行 lake update LeanCopilot、lake exe LeanCopilot/download、lake build。原生 Windows 用户还需要把 <path_to_your_project>/.lake/packages/LeanCopilot/.lake/build/lib 加进系统 Path 变量。README 明确要求项目使用的 Lean 版本不低于 lean4:v4.3.0-rc2，并且提醒版本要与其他依赖（例如 mathlib）兼容。
版本对齐是这套方案最贵的地方
LeanCopilot 的发布节奏跟着 Lean 走，从最近的 release 看，v4.33.0 与 v4.32.0 相隔不到一天，v4.31.0 到 v4.32.0 大约两个月。这意味着它必须持续跟进 Lean 与 mathlib 的版本，而你的项目也被绑上这条线。README 把「确保版本与其他依赖如 mathlib 兼容」单独写出来，说明这不是可以忽略的细节。实际成本在于：升级 mathlib 时你要同时确认 LEAN_COPILOT_VERSION 是否已有对应 tag，若没有就得指向 main，而 main 对应的是不稳定 Lean 版本。构建层面还有一层，README 说明下游包通常下载预编译 release，但在没有发布对应平台的 release 时会自动回退到从源码构建，那时就需要 CMake >= 3.7 和 C++17 编译器，Intel macOS 被 README 点名为这种情况。
什么时候它不合适
如果你的 Lean 版本低于 4.3.0-rc2，README 直接排除了这条路。如果你只在偶尔需要提示时用一次模型，为它引入 C++ 工具链、ctranslate2 链接参数和一份模型缓存并不划算，写个脚本把当前 goal 发给外部 API 更轻。还有一个更隐蔽的限制来自 select_premises：它检索的是固定快照，README 强调这一点，所以它对快照内的引理有效，对你自己项目里新写的定义没有覆盖。另外，README 的 Caveats 一节在目录中出现但正文未在提供的材料里展开，其中列出的具体限制无法从现有信息确认，采用前应当直接读该节。
与直接用 aesop 或外部脚本的差别
aesop 是 Lean 社区常用的自动化 tactic，走的是规则集与搜索，不涉及模型权重。LeanCopilot 的 search_proof 并不是替代 aesop，README 写的是把 LLM 生成的 tactic 与 aesop 组合来搜索多步证明，也就是说 aesop 仍在搜索回路里，模型负责提供候选动作。这个组合方式决定了它的行为特征：搜索空间由模型建议裁剪，命中率取决于模型对当前 goal 的理解，而不是规则集的完备性。另一条路是纯外部方案，即在 Lean 之外调用模型，把建议贴回来。差别在于 LeanCopilot 的推理发生在 Lean 进程内，省掉了进程间往返，代价是模型与 Lean 版本被编译期绑定，升级不再是换一个 Python 包那么简单。
许可与后续维护的账怎么算
仓库使用 MIT 许可，这对把它作为依赖引入商业或学术项目都不构成额外障碍，但要注意模型权重是单独从 Hugging Face 下载的，其许可条款与仓库代码的 MIT 不同，README 只给出了模型页面链接，没有在正文中说明权重许可，采用前需要自行查看对应模型页。维护成本主要落在版本跟进上：Lean 与 mathlib 每次大版本更新，你都要重新确认 LEAN_COPILOT_VERSION 的取值并重跑 lake update LeanCopilot 与 lake build。模型缓存位于 ~/.cache/lean_copilot/，属于用户级目录，多用户机器或 CI 环境需要考虑缓存是否共享，README 未涉及这一场景。
编辑结论
LeanCopilot 适合已经在 Lean 4 上维护 mathlib 依赖、并且愿意把推理运行时作为构建产物一起管理的团队；如果你的项目还在 Lean 4.3.0-rc2 之前的版本，或者你无法接受把 Hugging Face 模型缓存到 ~/.cache/lean_copilot/ 并链接 ctranslate2，那它就不是合适的工具，此时用命令行调用外部模型的脚本更省事。决定采用前先做三件事：确认 lakefile 里 moreLinkArgs 的 -L 路径与实际包路径一致，确认 LEAN_COPILOT_VERSION 与 mathlib 的 Lean 版本能同时编译通过，以及确认 select_premises 依赖的 mathlib 快照是否覆盖你需要的定义。
社区笔记