Skip to main content
Glama
Sign In
aristotle-mcp

aristotle-mcp

by crosedev
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Remote

aristotle-mcp

MCP server for the Aristotle 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

  2. Install:

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

  1. Set your API key:

export ARISTOTLE_API_KEY=your-key-here

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

Related MCP server: Aristotle MCP Server

Usage with Claude Code

Add to your Claude Code MCP config (e.g. ~/.claude/settings.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

This server cannot be deployed

Shareable, User-Owned Context BackendPeople, applications, and agents read, write, and coordinate together in one context lake. Reach it over MCP, a CLI, a Python SDK, or REST.fulcradynamics.comAd

Resources

Related MCP Connectors

Related MCP Servers

  • logosphere

    jdhart81
    A
    license
    Not graded
    quality
    B
    maintenance
    Provides an MCP server for building inspectable reasoning graphs, capturing arguments and evidence, and verifying conditional conclusions using Lean.
    Apache 2.0