Lean 形式化智能体
Lean 相关模块通过提供可视化、智能双向反馈的定理系统，以及配套的形式化智能体支持，来将原本有着极高操作门槛的交互式定理推导流程简易化。
进入方式
Lean 无需独立的开关界面。要进入正式环境：
- 点击 New Project 并选择 Theorem Proving 作为工程类型，继而选择您需要的 Lean Editor 工具链版本。
- 或在项目页直接选择 Theorem Proving Templates 后进入即可。 在该工作区内，右侧的对话框将默认由基础体系的 Reaslingo (reaslab-agent) 接管，随时待命。
基础功能
- 富文本代码编辑器与 Infoview：完整的 Lean 4 生态支持。除了提供语法高亮以及悬停释义诊断等要素，当您将光标放在
proof块内部时，专属的 Infoview （右侧栏）会实时反馈未结目标与前提假设（Goal / Hypotheses）。 - 复合检索引擎引擎：带有 Project Search 以及深度语义检索 Semantic Search (支持Moogle等特性)，帮助随时调取缺失的环境引理。
- 跨模态内容识别：您能直接让 AI 理解 Markdown 文本、包含伪代码的 LaTeX、甚至 PDF 数据中的定理证明逻辑，进而原生地转化为 Lean
theorem声明的形式化代码框架！
AI 辅助自动完成形式化
辅助补全与完善已有 Lean 文件
在 Lean 项目中，AI 对话可用于辅助补全和完善已有 .lean 文件中的形式化内容。使用时，可以先将相关代码片段、整个文件或所在文件夹加入对话上下文，再明确说明希望 AI 完成的任务，例如补全 sorry、解释当前 proof state、补充缺失的中间引理，或在不改动整体结构的前提下对局部证明进行修改和优化。这样，AI 能够结合当前文件中的定义、定理和项目结构，更有针对性地生成结果，适合用于已有 Lean 文件的持续完善。
示例：
- 请阅读我刚刚添加的 Lean 文件，定位其中的
sorry，并补全可直接运行的证明代码。 - 请只处理第一个
sorry，不要修改其他定义。 - 请先解释当前 goal 和 hypotheses，再给出可尝试的 tactic 版本。
- 请在保持现有文件结构不变的情况下，补充这个定理缺失的证明部分。
形式化 Markdown、LaTeX 或 PDF 中的定理
ReasLab 支持将文本、文件和截图直接加入 AI 对话，因此可以把 Markdown 文件、LaTeX 片段或 PDF 材料作为输入，让 AI 将其中的数学定义、命题或定理改写为 Lean 形式。实际使用时，通常可先要求 AI 提取定理内容，再要求其生成对应的 Lean theorem 声明；若需要，还可以进一步要求它给出辅助定义、引理或证明草稿。
示例：
- 请将 Markdown 文件中的“定理 2.1”形式化为 Lean 4 的
theorem声明。 - 请识别 LaTeX 文件中的定义与主要定理，并先生成 Lean 中的定义部分。
- 请提取 PDF 中目标定理的数学表述，并将其改写为适合当前项目的 Lean 定理。
使用建议：
- 若原文描述较长，可先要求 AI 总结出准确的数学命题。
- 再要求 AI 按 Lean 的定义、定理、证明三个层次逐步生成。
- 对于较复杂的定理，可要求 AI 先给出
theorem声明和需要的辅助引理，再逐步补全证明。
直接要求 AI 形式化某个定理并组织到项目文件中
如果用户已经明确知道要形式化的定理内容，也可以直接在 AI 对话中给出命题，并结合项目中的文件或目录上下文，要求 AI 按现有工程结构生成 Lean 代码。这种方式适合在已有项目框架下新增形式化内容，或按目录规范生成新的 Lean 文件草稿。
示例：
- 请将该命题形式化为 Lean 定理，并生成适合加入当前项目的代码。
- 请参考当前目录结构，为这个命题生成一个新的 Lean 文件草稿。
- 请先给出
theorem声明，再补充证明思路和所需辅助引理。
使用建议：
- 尽量说明目标文件位置、命名风格和依赖的已有定义。
- 可先加入相关文件作为上下文，使生成结果与现有风格一致。
- 对生成代码应结合编辑器与 Infoview 进一步检查和修改。
范例流程
- 创建环境完毕，在资源库中准备好您的待证明命题，或者带有
sorry未完成补全标记的.lean文件。 - 结合 @ Add Context，或者右键想要证明的文件并选择 Add File to Chat。
- 按照如下方法输入您的自然科学转换与验证需求：
"我已经添加了一个 Markdown 文件上下文，请提炼其中的'定理2.1'并以此作为目标条件，在目前工程里帮我填补所有的 sorry 以通过验证流程。"
- 在侧边栏 Infoview 的验证提示辅助下，确认并采用大模型产出的逻辑代码与引理分支。
示例项目
(项目链接占位符)