# aristotle-mcp

MCP server for the [Aristotle](https://aristotle.harmonic.fun) automated theorem prover. Lets Claude Code (or any MCP client) submit Lean projects, check job status, download results, and manage proving jobs.

## Setup

1. Get an API key from [aristotle.harmonic.fun](https://aristotle.harmonic.fun)
2. Install:

```bash
pip install git+https://github.com/Vilin97/aristotle-mcp.git
```

3. Set your API key:

```bash
export ARISTOTLE_API_KEY=your-key-here
```

Or put it in a `.env` file in your working directory.

## Usage with Claude Code

Add to your Claude Code MCP config (e.g. `~/.claude/settings.json`):

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

## Tools

| Tool | Description |
|------|-------------|
| `submit_file` | Submit a single Lean file for proving |
| `submit_directory` | Submit a multi-file Lean project |
| `submit_prompt` | Submit a plain-English math problem |
| `get_status` | Check project status |
| `list_projects` | List recent projects |
| `download_result` | Download completed results |
| `extract_result` | Download and extract results |
| `cancel_project` | Cancel a running job |
| `refresh_status` | Poll for updated status |

## Dependencies

- [`aristotlelib`](https://aristotle.harmonic.fun) — Aristotle Python SDK
- [`mcp`](https://pypi.org/project/mcp/) — Model Context Protocol SDK