AI导哈

Lean语言服务器协议模型上下文协议服务

一个高性能的Rust实现的Lean语言服务器协议（LSP）到AI助手的模型上下文协议（MCP）服务器，用于Lean 4证明辅助。

  • by LarsenClose
  • Rust
  • 本地部署
  • 1 星标
  • 更新于
在 GitHub 查看 LarsenClose/rust-lean-mcp

使用说明

防锈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 如果省略，服务器会自动检测精益项目根：

  1. 从 file_path 每次工具调用的参数（查找 lakefile.lean, lakefile.toml，或 lean-toolchain)
  2. 从服务器的工作目录
  3. 返回错误并显示明确信息

多个精益项目在同一会话中工作——每个项目都有自己的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 warnings

CI对每个PR运行6个必需的检查：Rustfmt、Clippy、测试（ubuntu+macOS）、文档和覆盖率。

许可证

麻省理工学院

相关 MCP