AI导哈

定理证明服务器

Aristotle-MCP是一个自动化定理证明服务器，允许用户提交Lean项目、检查任务状态、下载结果和管理证明任务。

  • by Vilin97
  • Python
  • 本地部署
  • 更新于
在 GitHub 查看 Vilin97/aristotle-mcp

使用说明

亚里士多德

MCP服务器 亚里士多德 自动定理证明器。允许Claude Code（或任何MCP客户端）提交精益项目、检查作业状态、下载结果和管理验证作业。

设置

  1. 从获取API密钥 亚里士多德和谐
  2. 安装：
pip install git+https://github.com/Vilin97/aristotle-mcp.git
  1. 设置API密钥：
export ARISTOTLE_API_KEY=your-key-here

或者把它放在 .env 文件在您的工作目录中。

使用Claude代码

添加到您的Claude Code MCP配置中（例如。 ~/.claude/settings.json):

{
  "mcpServers": {
    "aristotle": {
      "command": "aristotle-mcp",
      "env": {
        "ARISTOTLE_API_KEY": "your-key-here"
      }
    }
  }
}

工具

工具 说明
submit_file 提交一份精益文件进行证明
submit_directory 提交多文件精益项目
submit_prompt 提交一道简单的英语数学题
get_status 检查项目状态
list_projects 列出最近的项目
download_result 下载已完成的结果
extract_result 下载并提取结果
cancel_project 取消正在运行的作业
refresh_status 轮询更新状态

依赖项

相关 MCP