AxProver

Name: AxProver
Author: Axiomatic-AI

@Axiomatic-AI

代码仓库

关于 AxProver

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

基本信息

分类

其他

传输方式

stdio

发布者

Axiomatic-AI

提交者

Leopoldo Sarra

配置

使用下面的配置,将此服务器添加到你的 MCP 客户端。

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

工具

未检测到工具

工具是从 README 中自动提取的。维护者可以在 ## Tools 标题下列出工具,即可填充这部分内容。

概览

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.

其他分类下的更多 MCP 服务器

Unity MCP ✨

justinpbarnett

Unity MCP acts as a bridge between AI assistants and your Unity Editor. Give your LLM tools to manage assets, control scenes, edit scripts, and automate tasks within Unity.

12.2K

🚀 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