在 Lean 中配置 LLM 证明助手，主要通过安装和配置特定的插件或工具包来实现，核心是建立 Lean 环境与 LLM服务之间的桥梁。以下是基于主流工具 LeanCopilot 和 llmstep 的详细配置步骤与效率提升方法。

一、环境准备与核心工具安装

首先，确保你有一个可用的 Lean 4 项目（例如基于 mathlib4）。然后，通过 Lake包管理器添加 LLM 助手工具。

1. 安装 LeanCopilot (推荐)

LeanCopilot 是目前功能最全面的 LLM 证明助手集成工具，提供战术建议、自动证明搜索（LlmAesop）和智能前提检索。

在你的 Lean 项目根目录的 lakefile.lean 中添加依赖：

-- lakefile.lean
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git"

然后，在终端执行 lake update 和 lake exe cache get 来同步依赖。

2. 安装 llmstep (轻量级替代)

llmstep 是一个专注于为当前证明目标生成下一步战术的轻量级插件。

-- lakefile.lean
require llmstep from git "https://github.com/yourorg/llmstep.git" @ "main"
-- 注意：需替换为实际的 git 仓库地址

二、配置 LLM 服务端点

工具安装后，需配置其连接的 LLM。通常支持本地模型（通过 Ollama、LM Studio）和云端 API（如 OpenAI、Anthropic）。

1. 配置 LeanCopilot

创建一个配置文件（如 LeanCopilot.toml）或在环境变量中设置。以下是配置 OpenAI API 的示例：

# LeanCopilot.toml[llm]
provider = "openai"
model = "gpt-4o" # 或 "gpt-4-turbo", "gpt-3.5-turbo"
api_key = "your-api-key" # 建议通过环境变量 OPENAI_API_KEY 设置base_url = "https://api.openai.com/v1" # 可选，用于自定义端点

对于本地模型（如通过 Ollama 运行的 codellama 或 qwen2.5-coder）：

[llm]
provider = "ollama"
model = "codellama:7b"
base_url = "http://localhost:11434/v1"

2. 配置 llmstep

llmstep 通常需要一个独立的 Python 服务器来运行 LLM 并与其通信。你需要启动其服务器并配置 Lean 客户端连接。

# 启动 llmstep 服务器 (假设已克隆仓库)
cd path/to/llmstep
python server.py --model openai:gpt-4 --api-key $OPENAI_API_KEY

在 Lean 中，可能需要设置连接此服务器地址的环境变量。

三、在 Lean 中使用 LLM 助手提升验证效率

配置完成后，你可以在 Lean 证明中调用相关命令或策略。

1. 使用战术建议 (Tactic Suggestions)

在 VS Code 的 Lean Infoview 中，当你的光标位于 by 块或证明目标处时，LeanCopilot 可以自动或手动触发战术建议。

• 手动触发：在证明中使用 #gen_tactics 命令或调用相应的函数。
• 交互式选择：Infoview 会显示 LLM 生成的多个候选战术，点击即可应用。

import LeanCopilot

theorem test (p q : Prop) (h1 : p → q) (h2 : p) : q := by -- 将光标停留在此行，LeanCopilot 可能在 Infoview 中建议 `apply h1 at h2` 或 `exact h1 h2`
  exact h1 h2 -- LLM 可能生成的建议之一

2. 使用自动证明搜索 (LlmAesop)

LlmAesop 是 LeanCopilot 的核心功能，它将 LLM 的广度创意与 Aesop 规则引擎的深度搜索结合，能自动完成中等难度的证明。

import LeanCopilot

theorem add_comm_variant (n m : Nat) : n + m = m + n := by
  llmAesop? -- 使用 `llmAesop?` 命令尝试自动搜索证明
  -- 如果成功，工具会自动填充完整的证明脚本

你可以通过配置调整 llmAesop 的行为，例如限制搜索深度、调整温度参数等，以平衡成功率和速度。

3. 使用智能前提检索 (Premise Selection)

在复杂的上下文中，LLM 可以帮助从庞大的数学库（如 mathlib4）中检索出可能相关的前提（定理、定义），这是传统自动化证明器（如 simp、aesop）的盲点。

import LeanCopilot

-- 在证明中，LLM 可以分析当前目标，并从导入的模块中推荐可能用到的定理。
-- 此功能通常集成在后台，辅助 `llmAesop` 或战术建议。

四、高级配置与优化建议

配置项	目的	建议值/方法
LLM 模型选择	平衡成本、速度与证明能力。	云端：gpt-4o > gpt-4-turbo > gpt-3.5-turbo。本地：codellama、qwen2.5-coder。
温度 (Temperature)	控制生成多样性。	证明生成建议较低值（如0.1-0.3），以保持确定性；创意性前提检索可稍高（如 0.7）。
上下文长度	提供给 LLM 的证明状态信息量。	确保包含足够的本地假设和当前目标。LeanCopilot 会自动优化此上下文。
证明搜索限制	控制 llmAesop 资源消耗。	设置最大节点数 (maxRuleApplications) 和超时时间，防止卡死。
缓存机制	避免重复查询相同目标，节省成本与时间。	启用 LeanCopilot 的本地缓存功能。

代码示例：配置 LlmAesop 参数

-- 在你的证明文件中，可以局部配置 llmAesop
set_option trace.llmAesop true in -- 打开调试追踪
set_option llmAesop.maxRules 200 in -- 限制最大规则应用次数
theorem my_complex_theorem ... := by
  llmAesop (config := { maxDepth := 10, temperature := 0.2 }) -- 传入自定义配置

五、验证效率提升的实际表现

通过上述配置，你将获得以下效率提升：

1. 战术构思自动化：对于琐碎或模式化的证明步骤（如重写、应用引理），LLM 能即时提供准确建议，减少查阅文档和手动尝试的时间。
2. 中等难度证明自动化：llmAesop 能够自动完成许多原本需要人工分解和搜索的引理证明，将分钟级工作压缩至秒级。
3. 知识库导航：在庞大的 mathlib4 中，LLM 驱动的智能检索能快速定位可能有用的定理，克服了传统搜索的关键词依赖障碍。
4. 教学与学习：对于学习者，LLM 助手能提供实时、交互式的反馈和下一步提示，降低入门门槛。

核心注意事项：LLM 生成的内容必须经过 Lean 内核的严格验证。任何语法正确但逻辑错误的建议都会被内核拒绝，这保证了最终证明的绝对正确性。因此，配置的终极目标是建立一个“LLM 生成候选，Lean 内核裁决”的高效协作循环。

---

参考来源

• LeanCopilot震撼发布：LLM驱动的定理证明助手如何变革Lean开发体验
• 开源亮点：Lean Copilot - 引领定理证明的革新之路
• 推荐文章：【llmstep】—— 让证明过程智能化的Lean 4助手
• Numina-Lean-Agent：结合LLM与Lean的数学自动化证明系统
• LeanCopilot实战案例：用AI辅助证明解决数学难题的完整过程