AxProver

Name: AxProver
Author: Axiomatic-AI

@Axiomatic-AI

Repository

About AxProver

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

Basic information

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/"
    }
  }
}

Tools

No tools detected

We auto-extract tools from the README. The maintainer can list them under a ## Tools heading to populate this section.

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.

FAQ from AxProver

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

Reactive Resume

amruthpillai

A one-of-a-kind resume builder that keeps your privacy in mind. Completely secure, customizable, portable, open-source and free forever. Try it out today!

39.5K