广告合作
MCP.so
登录

AxProver MCP Server

@Axiomatic-AI

代码仓库

基本信息

分类

其他

传输方式

stdio

认证方式

oauth

作者

Axiomatic-AI

提交者

Leopoldo Sarra

关于 AxProver MCP Server

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

AxProver MCP Server 配置

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

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

AxProver MCP Server 工具

工具列表暂未提供

当前收录暂时没有可展示的工具列表，不代表服务没有工具。请查阅项目文档了解支持的能力。

此服务需要认证，获取工具列表可能需要登录或使用服务提供方的凭据。

点击上方按钮,直接连接服务器端点实时获取工具列表。

概览

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.

常见问题

1

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.

2

How is authentication handled?

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

3

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`.

4

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`.

5

Where does my code execute?

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

评论

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

Blender

ahujasid

Open-source MCP to use Blender with any LLM

23.6K

Activepieces

activepieces

AI Agents & MCPs & AI Workflow Automation • (~400 MCP servers for AI agents) • AI Automation / AI Agent with MCPs • AI Workflows & AI Agents • MCPs for AI Agents

23.2K

Handl

Handl speaks the Model Context Protocol. Your whole billing operation — projects, invoices, clients, reports, approvals — as tools any AI assistant can call, inside your autonomy rules.

Yuppsy

Yuppsy MCP: build and publish real estate websites from your AI assistant. Yuppsy lets your AI assistant create live websites for real estate agents and individual property listings. You don't need a designer or any code

MCP Toolbox for Databases

googleapis

MCP Toolbox for Databases is an open source MCP server for databases.

15.9K
广告合作