Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@Aristotle MCP Server prove that the sum of two even numbers is even in Lean"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
A minimal Model Context Protocol (MCP) server for the Aristotle API, enabling LLMs to prove theorems in Lean and formalize mathematical problems.
This project uses uv for dependency management.
uv syncRelated MCP server: Lean LSP MCP
You need an Aristotle API key. Set it in your environment:
export ARISTOTLE_API_KEY="your-api-key-here"Run the server using uv:
uv run main.pyThis will start the MCP server over stdio.
prove_lean_file(file_path): Submit a Lean file for proving. Returns Project ID.
prove_informal(file_path, formal_context_path): Submit a natural language problem. Returns Project ID.
prove_lean_code(lean_code): Submit Lean code string. Returns Project ID.
prove_informal_text(text, formal_context_path): Submit natural language string. Returns Project ID.
get_project_status(project_id, save_solution_to): Check status and retrieve solution code.
list_recent_projects(): List recent projects.
aristotle://projects: JSON list of recent projects.
aristotle://projects/{project_id}: Detailed status and content of a specific project.
Checks the status of a specific Aristotle project. Returns full project data including solution if available.
| Name | Required | Description | Default |
|---|---|---|---|
| project_id | Yes | ||
| save_solution_to | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It mentions that it 'Returns full project data including solution if available,' which hints at read-only behavior and output content, but lacks details on permissions, error handling, rate limits, or whether it's idempotent. For a tool with no annotation coverage, this is insufficient.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is extremely concise with two sentences that directly state the tool's function and output. Every word earns its place, and it's front-loaded with the core purpose, making it efficient and well-structured.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (2 parameters, no annotations, but has an output schema), the description is minimally adequate. The output schema likely covers return values, so the description doesn't need to detail them, but it lacks context on usage, parameters, and behavioral traits, leaving gaps in completeness.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The description doesn't explain the parameters beyond what the schema provides. With 0% schema description coverage, it fails to compensate by adding meaning to 'project_id' or 'save_solution_to.' However, since there are only 2 parameters and one is optional with a default, the baseline is slightly above minimal, but it doesn't enhance understanding.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose with a specific verb ('Checks') and resource ('Aristotle project'), making it immediately understandable. However, it doesn't explicitly differentiate from sibling tools like 'list_recent_projects' or the various 'prove_' tools, which would require a 5.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It doesn't mention when to choose 'get_project_status' over 'list_recent_projects' or any of the 'prove_' tools, nor does it specify prerequisites or exclusions for usage.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Lists the most recent projects submitted to Aristotle.
| Name | Required | Description | Default |
|---|---|---|---|
| limit | No | ||
| save_to | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It states the tool lists projects but lacks details on permissions, rate limits, pagination, or what 'submitted to Aristotle' entails. This leaves significant gaps in understanding how the tool behaves in practice.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, efficient sentence with no wasted words. It is front-loaded with the core purpose, making it easy to scan and understand quickly, which is ideal for conciseness.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's low complexity (2 parameters, no annotations, but has an output schema), the description is minimally adequate. It states what the tool does but lacks details on usage, parameters, and behavioral traits. The output schema may cover return values, but the description doesn't provide enough context for full understanding.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the schema provides no parameter details. The description doesn't mention parameters at all, failing to compensate for the coverage gap. However, with only 2 parameters and a default 'limit' of 10, the baseline is 3 as the tool is simple, but no value is added beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Lists') and resource ('most recent projects submitted to Aristotle'), making the purpose understandable. However, it doesn't differentiate from sibling tools like 'get_project_status' which might also retrieve project information, leaving room for ambiguity in tool selection.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided on when to use this tool versus alternatives. The description mentions 'most recent projects' but doesn't specify scenarios or exclusions, such as whether this is for monitoring submissions or retrieving metadata, nor does it reference sibling tools for comparison.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submits a file containing natural language mathematics (Text, Markdown, LaTeX) to be formalised and proved. Returns the Project ID immediately.
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | ||
| formal_context_path | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries full burden for behavioral disclosure. It mentions that the tool 'Returns the Project ID immediately,' which is useful context about response timing. However, it doesn't disclose critical behavioral traits: whether this is a long-running operation, what happens to the submitted file, authentication requirements, rate limits, or error conditions. For a tool that submits files for processing, this is a significant gap.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is appropriately concise with two clear sentences. The first sentence explains the core functionality, and the second provides important behavioral context about immediate Project ID return. There's no wasted language, though it could be slightly more structured with explicit parameter mentions.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given that an output schema exists (which presumably documents the Project ID return), the description doesn't need to explain return values. However, for a tool with 2 parameters (one undocumented), no annotations, and multiple sibling tools, the description is incomplete. It covers the basic purpose and immediate response but misses parameter explanations, usage differentiation, and important behavioral context about the formalization/proof process.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
With 0% schema description coverage for both parameters, the description must compensate but fails to do so. It mentions 'file_path' implicitly through 'file containing natural language mathematics' but doesn't explain what format or constraints this path should have. It doesn't mention 'formal_context_path' at all, leaving this parameter completely undocumented. The description adds minimal value beyond what's implied by the tool name.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Submits a file containing natural language mathematics... to be formalised and proved.' It specifies the action (submits), resource (file with mathematics content), and outcome (formalization and proof). However, it doesn't explicitly differentiate from siblings like 'prove_informal_text' which likely serves a similar purpose with text input instead of file input.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. With siblings like 'prove_informal_text', 'prove_lean_code', and 'prove_lean_file', there's no indication of when file-based informal proof is preferred over text-based or Lean-based alternatives. The description only states what the tool does, not when to choose it.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submits natural language mathematics directly to be formalized and proved. Returns the Project ID immediately.
| Name | Required | Description | Default |
|---|---|---|---|
| text | Yes | ||
| formal_context_path | No |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It states the tool 'submits' content and 'returns the Project ID immediately', implying an asynchronous operation with a quick initial response. However, it lacks details on permissions, rate limits, error handling, or what 'formalized and proved' entails in terms of time or resources.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is highly concise with two sentences that are front-loaded and waste no words. Each sentence adds value: the first explains the core action, and the second clarifies the immediate return, making it efficient and well-structured.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (asynchronous proof submission with 2 parameters), no annotations, and an output schema present (which handles return values), the description is minimally adequate. It covers the basic purpose and immediate response but lacks details on parameter usage, behavioral traits, and differentiation from siblings, leaving gaps for an agent to infer correctly.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the schema provides no parameter details. The description mentions 'natural language mathematics' which hints at the 'text' parameter, but doesn't explain the 'formal_context_path' parameter at all. It adds minimal meaning beyond the bare schema, failing to compensate for the low coverage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Submits natural language mathematics directly to be formalized and proved') and the resource (mathematical content), making the purpose understandable. However, it doesn't explicitly differentiate from sibling tools like 'prove_informal' or 'prove_lean_code', which likely handle similar proof tasks but with different input formats or contexts.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It mentions 'natural language mathematics' but doesn't specify scenarios where this is preferred over other proof tools like 'prove_lean_code' or 'prove_lean_file', nor does it mention prerequisites or exclusions.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submits Lean code directly to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately.
| Name | Required | Description | Default |
|---|---|---|---|
| lean_code | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It states that the tool 'submits' code and 'returns the Project ID immediately,' indicating an asynchronous or queued operation with a quick acknowledgment. However, it lacks details on permissions, rate limits, error handling, or what 'Aristotle' entails (e.g., a proof assistant), making behavioral traits insufficiently transparent for a tool with no annotation support.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is highly concise and front-loaded: two sentences that efficiently convey the action and immediate outcome. Every word earns its place, with no redundant or vague phrasing, making it easy to parse quickly.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (submission to a proof system), lack of annotations, and an output schema (which handles return values), the description is partially complete. It covers the core purpose and acknowledgment behavior but misses usage guidelines, parameter details, and behavioral context like error cases. The output schema reduces the need to explain returns, but other gaps remain, making it adequate but with clear omissions.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The input schema has 1 parameter with 0% description coverage, so the description must compensate. It implies 'lean_code' is the code to submit, but adds no details on format, constraints, or examples. Since schema coverage is low, the description provides minimal semantic value beyond the parameter name, meeting the baseline for moderate schema coverage but not fully compensating for the gap.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Submits Lean code directly to Aristotle to fill in 'sorry' placeholders.' It specifies the verb ('submits'), resource ('Lean code'), and target system ('Aristotle'), and distinguishes it from siblings like 'prove_lean_file' by specifying direct code submission. However, it doesn't explicitly differentiate from 'prove_informal' or 'prove_informal_text', which slightly reduces clarity.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives like 'prove_lean_file' (for files) or 'prove_informal' (for informal proofs). It mentions 'fill in 'sorry' placeholders,' which implies a context of incomplete proofs, but lacks explicit when/when-not instructions or prerequisites, leaving usage ambiguous.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submits a local Lean file to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately.
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes |
| Name | Required | Description |
|---|---|---|
| result | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It mentions that the tool 'Returns the Project ID immediately,' which hints at asynchronous processing and a follow-up tool like 'get_project_status.' However, it lacks details on permissions, rate limits, error handling, or what happens if the file is invalid. For a submission tool with zero annotation coverage, this is a significant gap.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is highly concise and front-loaded, consisting of two sentences that directly state the action and immediate outcome. Every word earns its place, with no redundant information or fluff, making it easy for an AI agent to parse quickly.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (submission with asynchronous processing), lack of annotations, and presence of an output schema (which likely covers the return value), the description is minimally adequate. It explains the core action and hints at follow-up needs but misses details like error conditions or integration with sibling tools. With an output schema, it doesn't need to explain return values, but behavioral aspects are under-specified.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The description doesn't explicitly discuss parameters, but with only one parameter ('file_path') and 0% schema description coverage, it implies the parameter's purpose through context: submitting a 'local Lean file.' This adds meaningful semantics beyond the bare schema, compensating for the low coverage. Since there's only one parameter, the baseline is high, but it doesn't specify format or constraints.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Submits a local Lean file to Aristotle to fill in 'sorry' placeholders.' It specifies the verb ('submits'), resource ('local Lean file'), and target system ('Aristotle'). However, it doesn't explicitly differentiate from siblings like 'prove_lean_code' or 'prove_informal', which likely handle different input formats or proving methods.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It doesn't mention sibling tools like 'prove_lean_code' (which might handle code snippets instead of files) or 'prove_informal' (which might handle informal proofs), nor does it specify prerequisites such as needing a valid Lean file with 'sorry' placeholders. Usage is implied but not explicitly stated.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
get_project_statuslist_recent_projectsprove_informalprove_informal_textprove_lean_codeprove_lean_fileScored across 6 tools
There is significant overlap between prove_informal, prove_informal_text, prove_lean_code, and prove_lean_file, as all four handle proof submission with only minor input format differences. This creates ambiguity for an agent trying to select the right tool, especially between the informal text and file variants. The get_project_status and list_recent_projects are distinct, but the core proving tools are poorly differentiated.
The naming follows a consistent snake_case pattern throughout, which is good. However, there is a minor inconsistency: most tools use verb_noun (e.g., get_project_status, prove_informal), but list_recent_projects uses verb_adjective_noun, which slightly deviates from the pattern. Overall, the naming is mostly predictable and readable.
With 6 tools, the count is reasonable for a server focused on mathematical proof automation. It covers key operations like project listing, status checking, and proof submission. However, the set feels slightly thin as it lacks tools for managing or updating existing projects, but it is well-scoped for the core workflow.
The tool surface covers basic submission and status checking, but there are notable gaps. For example, there are no tools to update, cancel, or delete projects, and no way to retrieve proof results beyond status. This could lead to dead ends for agents needing to manage project lifecycles, though core submission workflows are supported.
Architecture compiler for AI code. 11 tools, 92 actions, 872 Lean4 proofs, 100/100 self-cert.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
Formally verified AI safety APIs. Pay-per-call via USDC (x402). 75+ endpoints, no signup.
Curated knowledge API for AI agents - skill packs, semantic search, validated patterns.
