AxProver MCP Server

@Axiomatic-AI

Basic information

About AxProver MCP Server

An MCP server for building Lean4 code, and automated theorem proving

AxProver MCP Server config

Add this server to your MCP-compatible client using the configuration below.

{
  "mcpServers": {
    "ax-prover": {
      "type": "streamable-http",
      "url": "https://prover.axiomatic-ai.com/mcp/"
    }
  }
}

AxProver MCP Server tools

Tool list not available yet

This listing does not currently have a tool list to display. This does not mean the server has no tools; check its documentation for supported capabilities.

This server requires authentication. Tool discovery may require signing in or credentials from the provider.

Fetch the live tool list directly from this server's endpoint using the button above.

Overview

What is AxProver?

AxProver is an MCP server for Lean 4 that compiles source code and automatically proves theorems using Mathlib. It is designed for developers and mathematicians working with Lean 4 who want to offload theorem proving and compilation to cloud services.

How to use AxProver?

Add the server to your MCP client configuration (e.g., claude_desktop_config.json) with the type streamable-http and URL https://prover.axiomatic-ai.com/mcp/. Authentication uses OAuth 2.1 via GitHub, handled automatically by the client. Submit jobs with lean4_build or lean4_prove_theorems, then poll for results using lean4_get_job_status.

Key features of AxProver

Compile Lean 4 code in a Mathlib-enabled sandbox.
Automatically prove theorems containing sorry.
Asynchronous job execution with immediate job_id return.
Poll job status until completion or failure.
OAuth 2.1 authentication via GitHub.

Use cases of AxProver

Compiling Lean 4 projects without local environment setup.
Proving unfinished Lean 4 theorems with AI assistance.
Integrating automated theorem proving into MCP-compatible clients.
Rapidly testing Lean 4 code snippets against Mathlib.

Frequently asked questions

What does AxProver do?

AxProver lets you compile Lean 4 code and automatically prove theorems using Mathlib, all through an MCP server. Code is sent to external cloud services for compilation and AI processing.

How is authentication handled?

The server uses OAuth 2.1 via GitHub. Your MCP client automatically manages the authentication flow.

What tools are available?

Three tools: `lean4_build` (compile), `lean4_prove_theorems` (prove theorems with `sorry`), and `lean4_get_job_status` (poll for results). Submit tools are asynchronous and return a `job_id`.

Are jobs synchronous or asynchronous?

All submit tools are asynchronous. They return a `job_id` immediately; use `lean4_get_job_status(job_id)` to poll until status is `completed` or `failed`.

Where does my code execute?

Code is sent to external cloud services for compilation and, if proving, also for AI processing.

Comments

More Other MCP servers

🚀 Model Context Protocol (MCP) Curriculum for Beginners

microsoft

This open-source curriculum introduces the fundamentals of Model Context Protocol (MCP) through real-world, cross-language examples in .NET, Java, TypeScript, JavaScript, Rust and Python. Designed for developers, it focuses on practical techniques for building modular, scalable,

16.7K

Senso MCP for Joomla

sensomedia

Senso MCP turns a Joomla 5 or 6 site into a remote MCP server. It runs inside Joomla itself (no extra server, no Node.js bridge) and is secured with OAuth 2.1 and Joomla's own ACL. The free pack lets an AI assistant crea

MaxKB

1Panel-dev

🔥 MaxKB is an open-source platform for building enterprise-grade agents. 强大易用的开源企业级智能体平台。

22.0K

Blender

ahujasid

Open-source MCP to use Blender with any LLM

23.6K

Screenpipe

screenpipe

YC (S26) | Open Computer History | Continuously record your company computer work, map your workflows, help you find work worth automating, and power your agents' context

22.0K