Lean Copilot：LLMs 在 Lean 中的证明助手

1. 项目介绍

Lean Copilot 是一个开源项目，它利用大型语言模型（LLMs）作为 Lean 证明助手，支持自动提出证明策略、查找前提并搜索多策略证明。项目的目标是通过与 Lean 用户的交互形成正向反馈循环，从而优化 LLMs 在数学证明中的表现。^1

2. 项目快速启动

安装要求

确保安装了以下软件：

• CMake：版本至少为 3.7
• C++17 兼容的编译器
• Git LFS：可选但推荐（特别是如果你有CUDA GPU）

添加 Lean Copilot 依赖

修改你的 lakefile.lean 文件，添加 Lean Copilot 作为依赖项：

package «your-package» [
  moreLinkArgs := [
    "-L /lake/packages/LeanCopilot/lake/build/lib",
    "-lctranslate2"
  ]
]
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"

替换 LEAN_COPILOT_VERSION 为你所需的 Lean Copilot 版本。

下载内置模型

执行以下命令来下载 Lean Copilot 的内置模型：

lake exe LeanCopilot/download

构建项目

运行以下命令来构建你的项目：

lake build

3. 应用案例和最佳实践

策略建议

导入 LeanCopilot 后，使用 suggest_tactics 命令生成证明策略建议：

import LeanCopilot
open LeanCopilot

meta def my_proof : tactic unit := do
  suggest_tactics,
  -- 点击建议的策略并在证明中使用它

证明搜索

使用 search_proof 函数结合 LLM 生成的策略与 AESOP（一种 Lean 4 自动化工具）来搜索多策略证明：

open LeanCopilot

meta def my_search_proof : tactic unit := do
  search_proof,
  -- 单击找到的策略插入编辑器

前提选择

使用 Lean Copilot 提取潜在有用的前提：

open LeanCopilot

meta def my_premise_selection : tactic unit := do
  premise_selection,
  -- 查看并应用选择的前提

4. 典型生态项目

LeanDojo: 提供内置模型以及一个测试环境，可用于训练和评估 Lean Copilot。 mathlib4: Lean 4 的主要数学库，Lean Copilot 可从中选取前提。