防锈mcp
一个高性能的Rust实现 精益lsp-mcp --模型上下文协议（MCP）服务器，将Lean 4的语言服务器协议连接到AI助手。
安装
来源
git clone https://github.com/LarsenClose/rust-lean-mcp.git
cd rust-lean-mcp
cargo install --path crates/lean-mcp-server先决条件
- 精益4 随着
lake在你的路上 - 精益项目
lakefile.lean（或lakefile.toml)以及lean-toolchain
用法
使用克劳德代码
添加到您的 ~/.claude.json （全球）或项目 .mcp.json:
{
"mcpServers": {
"lean-lsp": {
"command": "rust-lean-mcp"
}
}
}服务器会从工具调用中的文件路径自动检测您的精益项目——否 --lean-project-path 大多数工作流程都需要。
具有明确的项目路径
rust-lean-mcp --lean-project-path /path/to/lean/project自动检测
当 --lean-project-path 如果省略，服务器会自动检测精益项目根：
- 从
file_path每次工具调用的参数（查找lakefile.lean,lakefile.toml，或lean-toolchain) - 从服务器的工作目录
- 返回错误并显示明确信息
多个精益项目在同一会话中工作——每个项目都有自己的LSP客户端。
工具
26个MCP工具用于精益4验证辅助：
| 类别 | 工具 |
|---|---|
| 证明状态 | lean_goal, lean_term_goal, lean_proof_diff, lean_goals_batch |
| 代码智能 | lean_hover_info, lean_completions, lean_references, lean_declaration_file, lean_code_actions |
| 文件分析 | lean_diagnostic_messages, lean_file_outline, lean_project_health |
| 搜索 | lean_leansearch, lean_loogle, lean_leanfinder, lean_state_search, lean_hammer_premise, lean_local_search |
| 战术 | lean_multi_attempt （并行和顺序）， lean_run_code |
| 构建 | lean_build |
| 验证 | lean_verify |
| 小部件 | lean_get_widgets, lean_get_widget_source |
| 分析 | lean_profile_proof |
| 批次 | lean_batch |
建筑
3格工作空间：
crates/
├── lean-lsp-client/ # Standalone async Lean 4 LSP client (no MCP dependency)
├── lean-mcp-core/ # Business logic, models, utilities (no MCP/LSP dependency)
└── lean-mcp-server/ # MCP server binary (rmcp + tool handlers)发展
cargo test --all
cargo fmt --all -- --check
cargo clippy --all-targets -- -D warningsCI对每个PR运行6个必需的检查：Rustfmt、Clippy、测试（ubuntu+macOS）、文档和覆盖率。
许可证
麻省理工学院