Lean 4 工具

ReasLab 提供浏览器内的 Lean 4 工作区，集成项目环境准备、语言服务器反馈、交互式 Infoview、代码导航、Unicode 输入、搜索与 AI 辅助。本指南以当前界面中的 Mathlib 项目为例。

本指南包含

可根据想要完成的任务直接查找对应章节：

想要完成的任务	对应章节
开始使用一个 Lean 仓库	打开 Lean 项目
查看目标、期望类型和消息	在 Infoview 中读取证明状态
检查错误和行内反馈	诊断与 Code Lenses
查看符号信息或跳转到声明	导航与重命名 Lean 代码
输入数学符号	插入 Unicode 符号
查找文本、定义或引理	搜索 Lean 代码
解决常见初始化或编辑器问题	故障排查

打开 Lean 项目

从资源管理器（Explorer）打开一个 .lean 文件。ReasLab 会定位项目根目录，读取其中的 lean-toolchain 与 Lake 配置，并在启动 Lean 语言服务器前准备运行环境。

底部状态栏中的初始化入口会分别显示各个准备阶段：

• Toolchain：安装或激活项目指定的 Lean 版本。
• Packages：解析并准备 Lake 配置中声明的依赖包。
• Cache：下载或准备可用缓存，包括 Mathlib 缓存。
• 状态与版本：出现对勾表示初始化完成；右下角版本入口显示当前工具链，例如 Lean v4.34.0-rc2。

首次打开项目时，这些阶段可能需要一定时间，完成前 Infoview 会保持等待状态。若某个阶段失败，可打开初始化面板查看对应日志，并使用工作区中显示的重试操作。

所有阶段准备完成后，ReasLab 会自动启动 Lean 分析，日常编辑与检查不需要再执行独立的手动构建命令。创建新项目时，可在 New Project 中选择 Lean 版本并决定是否包含 Mathlib；导入已有仓库时，ReasLab 会遵循仓库现有的工具链与 Lake 配置。

在 Infoview 中读取证明状态

Infoview 用于显示 Lean 在当前光标位置掌握的证明信息。打开 Lean 文件后，点击编辑器工具栏中的眼睛图标 Toggle Lean Infoview。

将光标移到定理、证明项或 tactic 代码块中，可以查看：

• Tactic state：当前未完成目标、局部变量、类型类实例、假设，以及 ⊢ 后的目标。
• Expected type：Lean 在当前项位置期望得到的类型。
• Messages：与当前位置相关的反馈，并可通过其中的按钮返回对应源码位置。
• All Messages：当前文件收集到的诊断与信息输出。

声明完成时，Lean 可能显示 Goals accomplished!。如果 Infoview 显示 No info found，请把光标从空白区域移到定理声明、证明项或某条 tactic 中，并等待当前文件处理完成。

诊断与 Code Lenses

项目初始化完成后，Lean 会在编辑过程中持续反馈问题与证明进度。

• 错误、警告和提示通过编辑器装饰与 gutter 标记显示。
• 同一组反馈也会汇总到 Infoview 的 Messages 和 All Messages。
• Goals accomplished! 等简短结果可以直接显示在代码旁。
• Show Code Lenses 和 Hide Code Lenses 用于控制这些行内结果，不需要关闭 Infoview。
• Lean 处理大型文件时，底部状态栏会显示当前文件与处理进度。

应等待处理状态稳定后，再把临时消息视为最终结果。处理完成后，诊断信息会与当前文档保持同步，不需要执行独立的手动构建。

悬停信息

悬停信息用于快速了解 Lean 符号，不需要离开当前文件。

将鼠标放在声明、定理、引理、类型或导入符号上，可以查看其签名、文档说明和来源 import。这些信息由当前 Lean 语言服务器提供，因此需要先完成项目初始化与文件处理。

只需要了解符号上下文时使用悬停；需要阅读声明源码时使用定义跳转。

导航与重命名 Lean 代码

右键点击符号可打开语言感知的导航菜单。可根据需要在声明之间移动、查看调用关系，或安全地重命名项目符号。

根据目标选择相应操作：

目标	操作
打开符号的声明	Go to Definition（转到定义）
打开符号类型的声明	Go to Type Definition（转到类型定义）
查找所有使用位置	Find All References（查找所有引用）
查看调用方	Show Incoming Calls（显示传入调用）
查看被调用项	Show Outgoing Calls（显示传出调用）
浏览当前文件中的声明	Document Outline（文档大纲）
查找工作区符号	Go to Symbol in Workspace（转到工作区符号）
重命名项目符号	Rename Symbol（重命名符号）

转到定义的操作步骤如下：

1. 将光标放在声明、定理、引理、类型或导入符号上。
2. 右键选择 Go to Definition。
3. ReasLab 会打开声明所在文件，并把光标定位到源码位置。

当前项目内的定义会在普通编辑器标签页中打开。Lean、Mathlib 或其他依赖中的定义会在只读 preview 标签页中打开，因此可以检查依赖源码而不会修改它。需要查看符号“类型本身”的声明时，应使用 Go to Type Definition。

若导航没有返回结果，请等待项目初始化和当前文件分析完成，然后把光标直接放在可解析符号上重试。

语法高亮与编辑辅助

编辑器将 Lean 语言感知能力与常用编辑功能结合，帮助用户快速识别声明与证明结构。

• 语法与语义 token 会区分命令、声明、标识符、类型、tactic、字面量和注释。
• 括号匹配和彩色嵌套括号有助于追踪复杂表达式。
• 常用单字符括号和双引号支持自动闭合。
• 工具栏和命令面板提供撤销、重做、行注释、文件内搜索等操作。
• 状态栏显示当前文件路径、光标行列、编码、同步状态、服务状态和 Lean 版本。

这些辅助功能不会改变 Lean 语义，而是让较长证明文件的编辑与检查更加清晰。

插入 Unicode 符号

ReasLab 同时支持可视化符号面板和 Lean 风格的反斜杠缩写，用于输入数学符号。

可根据使用习惯选择输入方式：

• 点击编辑器工具栏中的 Symbols Palette 打开符号面板。
• 按 Essential、Greek Letters、Logic & Arrows、Relations、Operators、Sets & Numbers、Brackets & Quotes 和 Miscellaneous 分类浏览。
• 按缩写或字符搜索符号，然后点击结果插入到当前光标位置。
• 在编辑器中输入反斜杠缩写，并按空格接受补全，例如 \forall → ∀、\exists → ∃、\to → →、\le → ≤。
• 将鼠标悬停在已插入的 Unicode 符号上，可查看生成该符号的一种或多种缩写。

不熟悉符号时可使用面板浏览；需要反复输入时，使用反斜杠补全会更高效。

搜索 Lean 代码

ReasLab 提供三种搜索方式。可根据是否知道准确文本、数学概念或目标 Lean 声明类型来选择。

搜索方式	适用场景	使用方式
Project Search	在当前项目中查找准确文本	在左侧活动栏选择 Project Search；结果按文件分组，点击后定位到匹配行。
Semantic Search	用自然语言或 Lean 相关术语描述概念	在活动栏选择 Semantic Search，打开 Semantic，输入查询并选择 Aggregated Interleaved、Lean Search、Moogle 或 State Search。
Lean/Local Search	查找当前 Lean 环境可用的引理、定理和定义	打开 Lean/Local，在项目可用的声明中搜索。

也可以先在编辑器中选中代码，再从右键菜单选择 Search with Semantic Search。已知名称时优先使用 Project Search；按概念查找时使用 Semantic Search；需要结果与当前项目 Lean 环境一致时使用 Lean/Local Search。

配合 ReasLingo 工作

ReasLingo 在编辑器与 Infoview 旁提供 AI 辅助，并把当前项目作为上下文。

• 在聊天框输入 @ 可引用项目文件或文件夹。
• 选中代码后使用 Add to Chat，可围绕具体证明片段提问。
• 可以让智能体解释证明状态、寻找合适引理或起草证明。
• 接受生成内容前，应使用实时 Infoview 验证 Lean 代码。

ReasLingo 可以加快探索与起草过程，但 Lean 的检查结果仍是正确性的最终依据。完整工作流见 Lean 形式化指南。

故障排查

大多数反馈缺失或导航无结果的问题，都是因为项目初始化或当前文件处理尚未完成。

• Infoview 一直等待：打开底部初始化状态，等待 Toolchain、Packages 和 Cache 全部就绪。
• Infoview 显示 No info found：把光标放在定理、证明或 tactic 内部，并等待文件处理完成。
• 悬停或导航不可用：确认项目初始化完成，且状态栏显示了预期的 Lean 版本。
• 找不到 Infoview 面板：点击编辑器工具栏中的 Toggle Lean Infoview。
• 没有行内消息：点击 Show Code Lenses。

若这些检查仍未解决问题，请参阅故障排查，继续检查通用工作区与连接状态。