MCP · 理科

LeanTool

LeanTool 是 Lean 的 code interpreter，其中 leanmcp.py 是 Model Context Protocol server。README 说它将 Lean 和插件暴露为 MCP tool，已测试可用于 Claude Code、Claude Desktop、Cursor、VS Code Agent Mode、Gemini CLI、Cline、Goose。数学、逻辑、形式化验证方向研究生可以让 agent 写 Lean 4 定理并获得编译器反馈。

适合解决什么问题

数学/形式化验证研究需要让 agent 调用 Lean 检查证明，而不是只自然语言推理

可产出：Lean theorem/proof checks; compiler feedback

查看项目与安装说明

收藏保存在当前浏览器，换设备不会同步。

用过之后，评个分

加载评分…

按你实际使用的体验评分，帮助其他研究者选择。

选择 1–5 星

同一浏览器保留一份评分，可修改或撤回。

匿名用户评分，仅供参考；清除 Cookie 或换浏览器后将无法修改原评分。