Lean 工作流
证明工具
MathCode 直接处理选定工作区中的 Lean 文件。Agent 按需选择工具，/lean 提供可选指导。
| 工具 | 用途 |
|---|---|
LeanGoal |
查看明确源码位置的目标。 |
LeanCheck |
编译文件或临时候选，获取反馈。 |
LeanSearch |
通过选定的一个 provider 搜索声明。 |
LeanVerify |
严格验证一个完整限定名的声明。 |
只有成功的 LeanVerify 结果中 data.verified=true 才能判定证明完成。
默认超时为 1200 秒，timeout_s 可设到 3600 秒。Goal/check 反馈本身不是完成证书。
Agent 可以使用辅助引理、子目标、分支和定理复用。原子证明工具不会隐式保存定理、 添加公理或更新 vault。
定理库
/theorem-store store <file> <qualified-declaration>
/theorem-store sync
/theorem-store check
/theorem-store status
store 验证并存储一个显式指定的定理：重新检查源码与依赖，在 Stored.lean
中验证重命名后的声明，再构建可导入模块。发布失败会回滚库更新。
编译和发布分别有 300 秒构建预算。
sync 发现候选并询问要保存哪些声明；check 编译检查整库；status 显示存储
数量与 vault 信息。仅通过 MATHCODE_OBSIDIAN_VAULT 或 /obsidian on 激活
vault 后才会提供 LibSearch，否则可用 LeanSearch。
公理库
/axiomatize "A 比 B 快"
/axiomatize list
/axiomatize check
/axiomatize remove <name>
声明按 vault 保存，经过 Lean 编译检查与一致性审查。需要把这些假设放入证明上下文 时，请显式导入或引用；原子 Lean 调用不会自动注入已保存的假设。
Obsidian
/obsidian on
/obsidian off
/obsidian generate
修改证明后执行 generate，再用 Obsidian Graph View 查看依赖。引理笔记包含
从 Mathlib 查询的定义。生成操作会更新 MathCode 管理的笔记及可识别的旧投影，
保留其他用户笔记，遇到冲突文件名则失败。
论文 catalog ID 不能冲突。如果根据标题与作者生成的 ID 已属于另一篇论文， 请使用不同 ID 或另一个 vault。依赖环错误会指出相关 claim 和 catalog 修复方法。
可选反馈后端
符合条件的通用编译调用可以通过 MATHCODE_LEAN_REPL=1 使用进程内 REPL。
原子证明工具不使用这份缓存。
macOS 上可配置外部 Kimina Lean Server，为 LeanGoal 与 LeanCheck 提供反馈：
MATHCODE_KIMINA_SERVER=1
MATHCODE_KIMINA_CMD="/absolute/path/to/kimina-lean-server/.venv/bin/python -m server"
MATHCODE_KIMINA_CWD=/absolute/path/to/kimina-lean-server
MATHCODE_KIMINA_PROJECT_ROOT=/absolute/path/to/served-lean-project
声明的项目与 Lean 版本必须匹配当前项目。命令须直接启动 Python；使用 virtualenv
时，它必须位于 MATHCODE_KIMINA_CWD 下。MathCode 在仅绑定 loopback 的沙箱中
启动服务，移除 provider 凭据，只允许写入私有 scratch。启动、兼容性或传输失败时
回退到锁定工具链的子进程，并报告警告。
Kimina 反馈不是完成证书。LeanVerify 与隔离论文 Agent 始终使用新的隔离子进程。
Linux 和 Windows 在此反馈路径中使用锁定工具链的子进程；发行包本身仅支持
安装指南列出的平台。