定理证明服务器

Aristotle MCP服务器

Aristotle API的最小模型上下文协议（MCP）服务器，使LLM能够证明Lean中的定理并将数学问题形式化。

安装

此项目使用 uv 用于依赖性管理。

uv sync

配置

你需要一个亚里士多德API密钥。在您的环境中设置它：

export ARISTOTLE_API_KEY="your-api-key-here"

运行服务器

使用以下命令运行服务器 uv:

uv run main.py

这将通过stdio启动MCP服务器。

工具

• prove_lean_file(file_path)：提交精益文件以供证明。返回项目ID。
• prove_informal(file_path, formal_context_path)：提交一个自然语言问题。返回项目ID。
• prove_lean_code(lean_code)：提交精益代码字符串。返回项目ID。
• prove_informal_text(text, formal_context_path)：提交自然语言字符串。返回项目ID。
• get_project_status(project_id, save_solution_to)：检查状态并检索解决方案代码。
• list_recent_projects()：列出最近的项目。

资源

• aristotle://projects：最近项目的JSON列表。
• aristotle://projects/{project_id}：特定项目的详细状态和内容。