Aristotle MCP Server

Note: This project was 100% vibe-coded with Claude Code.

An MCP (Model Context Protocol) server that wraps Aristotle, Harmonic's automated theorem prover for Lean 4. This enables AI assistants to strategically invoke theorem proving during Lean development—filling in sorry statements, verifying lemmas, or formalizing natural language into Lean code.

What is Aristotle?

Aristotle is a cloud-based theorem proving service by Harmonic that can automatically fill in proofs in Lean 4. Given Lean code with sorry placeholders, Aristotle attempts to find valid proofs using advanced search techniques.

To use this MCP server, you'll need an API key from aristotle.harmonic.fun.

Tools Provided

Tool	Description
prove	Fill in sorry statements in Lean code snippets
prove_file	Prove all sorries in a Lean file with automatic import resolution
formalize	Convert natural language math to Lean 4 code
check_proof	Poll async proof jobs for completion
check_prove_file	Poll async file proof jobs for completion
check_formalize	Poll async formalization jobs for completion

Installation

Prerequisites

Install uv (the fast Python package manager):

# macOS
brew install uv

# Or via shell script (macOS/Linux)
curl -LsSf https://astral.sh/uv/install.sh | sh

Get Your API Key

1. Sign up at aristotle.harmonic.fun
2. Copy your API key
3. Add it to your shell configuration (~/.zshrc or ~/.bashrc):

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

Then restart your terminal or run source ~/.zshrc.

Adding to Claude Code

Option 1: Command Line (Recommended)

claude mcp add aristotle -e ARISTOTLE_API_KEY=$ARISTOTLE_API_KEY -- uvx --from git+https://github.com/septract/lean-aristotle-mcp aristotle-mcp

This registers the server with your API key from the environment. Use --scope user to make it available across all projects:

claude mcp add aristotle --scope user -e ARISTOTLE_API_KEY=$ARISTOTLE_API_KEY -- uvx --from git+https://github.com/septract/lean-aristotle-mcp aristotle-mcp

Option 2: JSON Configuration

Add to your ~/.claude.json:

{
  "mcpServers": {
    "aristotle": {
      "type": "stdio",
      "command": "uvx",
      "args": ["--from", "git+https://github.com/septract/lean-aristotle-mcp", "aristotle-mcp"],
      "env": {
        "ARISTOTLE_API_KEY": "${ARISTOTLE_API_KEY}"
      }
    }
  }
}

The ${ARISTOTLE_API_KEY} syntax expands to your shell environment variable.

Verify Installation

claude mcp list              # Check server is registered
claude mcp get aristotle     # Test the connection

Or inside Claude Code, run /mcp to see connection status.

Adding to Claude Desktop

Add to your claude_desktop_config.json:

{
  "mcpServers": {
    "aristotle": {
      "command": "uvx",
      "args": ["--from", "git+https://github.com/septract/lean-aristotle-mcp", "aristotle-mcp"],
      "env": {
        "ARISTOTLE_API_KEY": "your-api-key-here"
      }
    }
  }
}

Note: Claude Desktop doesn't expand environment variables, so you must include your actual API key.

Mock Mode (Testing Without API Key)

To test the MCP server without making real API calls:

claude mcp add aristotle-mock -e ARISTOTLE_MOCK=true -- uvx --from git+https://github.com/septract/lean-aristotle-mcp aristotle-mcp

Or set in your configuration:

{
  "env": {
    "ARISTOTLE_MOCK": "true"
  }
}

Usage Notes

• Proofs take time: Aristotle proofs can take anywhere from a few minutes to several hours depending on complexity. Simple proofs may complete in 1-5 minutes, but complex proofs can take significantly longer. The tools support async mode (wait=False) for non-blocking operation—this is strongly recommended for anything non-trivial.
• Lean 4 only: Aristotle works with Lean 4, not Lean 3 or earlier versions.
• Mathlib support: File-based proving automatically resolves Lake dependencies including Mathlib.

Async Workflow

All proving tools support synchronous (wait=True, default) and asynchronous (wait=False) modes.

Synchronous Mode (Simple)

prove(code, wait=True)        → Returns filled proof when complete
prove_file(file, wait=True)   → Writes solution file when complete
formalize(desc, wait=True)    → Returns Lean code when complete

Asynchronous Mode (Non-blocking)

Use async mode for long-running proofs to avoid blocking:

1. Submit:    prove_file(file, wait=False)     → Returns project_id
2. Poll:      check_prove_file(project_id)     → Returns status (save=False by default)
3. Save:      check_prove_file(project_id, output_path="out.lean", save=True)

Key points:

• check_prove_file defaults to save=False — it only checks status without writing files
• To save the result, call with save=True
• If output_path is omitted, uses the path from the original prove_file call (stored for 30 days)
• You can override output_path to save to a different location
• check_proof and check_formalize return the code directly in the response (no save parameter needed)

Context Files

• prove accepts context_files (a list) — multiple Lean files can provide imports
• formalize accepts context_file (singular) — only one context file supported

This difference reflects the underlying aristotlelib API.

Local Development

Clone the repository and install in editable mode:

git clone https://github.com/septract/lean-aristotle-mcp.git
cd lean-aristotle-mcp
make venv
source .venv/bin/activate
make install-dev  # Includes dev dependencies

Run the development server:

make run          # Uses real API
make run-mock     # Uses mock responses

The project uses a Makefile for common tasks. Run make help for all options.

make check      # Run lint + type-check
make test       # Run mock tests (no API key needed)
make test-api   # Run live API tests (requires ARISTOTLE_API_KEY)
make verify     # Full verification suite

Troubleshooting

"spawn uvx ENOENT" error

This means uv isn't in Claude's PATH. On macOS, GUI applications don't always inherit your shell PATH. Solutions:

1. Restart Claude after installing uv
2. Use full path: Replace uvx with the full path (e.g., /opt/homebrew/bin/uvx)
3. Check installation: Run which uvx in terminal to verify uv is installed

"ARISTOTLE_API_KEY not set" error

Make sure you've:

1. Added export ARISTOTLE_API_KEY="..." to your shell config
2. Restarted your terminal
3. Included -e ARISTOTLE_API_KEY=$ARISTOTLE_API_KEY when adding the server

License

MIT - see LICENSE for details.

Links

• Aristotle API - Get your API key
• Harmonic - Company behind Aristotle
• aristotlelib on PyPI - Python client library
• Model Context Protocol - MCP specification