AxProver

Created By

Axiomatic-AI5 months ago

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

Overview Content Tools Comments

Overview

Axiomatic Prover — MCP Server

Lean 4 MCP server: compile and prove theorems with Mathlib.

Connect

Add to your MCP client (e.g. Claude Desktop claude_desktop_config.json):

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

Authentication uses OAuth 2.1 via GitHub — your MCP client handles the flow automatically.

Tools

Submit (async — returns a `job_id`)

Tool	Description
`lean4_build`	Compile Lean 4 source code in a Mathlib-enabled sandbox. Code is sent to external cloud services for compilation; if proving, also for AI processing.
`lean4_prove_theorems`	Automatically prove Lean 4 theorems that contain `sorry`. Code is sent to external cloud services for compilation and AI proving.

Poll

Tool	Description
`lean4_get_job_status`	Poll for the status and result of any ax-prover job.

All submit tools are asynchronous — they return a job_id immediately. Poll with lean4_get_job_status(job_id) until status is completed or failed.

Links

Project Info

Created At

5 months ago

Updated At

4 months ago

Author Name

Axiomatic-AI

Star

Language

License

Recommend Servers

View All

EdgeOne Pages MCP

@TencentEdgeOne

An MCP service designed for deploying HTML content to EdgeOne Pages and obtaining an accessible public URL.

TypeScript

a year ago

MCP Server for Milvus

@zilliztech

The Milvus MCP server enables AI applications to interact with Milvus vector databases using natural language commands. It allows AI models to perform vector searches, manage collections, and retrieve data without writing custom database queries. This integration facilitates seamless access to vector data, enhancing the capabilities of AI tools like Claude Desktop and Cursor.

a year ago

GBOX Android MCP

@babelcloud

GBOX provides environments for AI Agents to operate computer and mobile devices. Mobile Scenario: Your agents can use GBOX to develop/test android apps, or run apps on the Android to complete various tasks(mobile automation). Desktop Scenario: Your agents can use GBOX to operate desktop apps such as browser, terminal, VSCode, etc(desktop automation). MCP: You can also plug GBOX MCP to any Agent you like, such as Cursor, Claude Code. These agents will instantly get the ability to operate computer and mobile devices.

a year ago

Creationloop

@marino129

12 days ago

Puppeteer

@modelcontextprotocol

Browser automation and web scraping

a year ago

Filesystem

Secure file operations with configurable access controls

a year ago

Aiimagemultistyle

@codecraftm

A Model Context Protocol (MCP) server for image generation and manipulation using fal.ai's Stable Diffusion model.

a year ago

PostgreSQL

@modelcontextprotocol

Read-only database access with schema inspection

a year ago

12 days ago

12 days ago

@modelcontextprotocol

A Model Context Protocol server that provides time and timezone conversion capabilities. This server enables LLMs to get current time information and perform timezone conversions using IANA timezone names, with automatic system timezone detection.

5 months ago

302_browser_use_mcp

@302ai

Automatically create a remote browser to complete your specified tasks, developed based on Browser Use + Sandbox. 自动创建一个远程浏览器，完成你指定的任务，基于Browser Use + Sandbox开发。

a year ago

12 days ago

12 days ago

@modelcontextprotocol

Web and local search using Brave's Search API

a year ago

Mcp Server Chatsum

@chatmcp

summarize chat message

typescript

a year ago

Luxembourg Payments Mcp

@junter1989k-ai

12 days ago

Greece Payments Mcp

@junter1989k-ai

12 days ago

Aws Kb Retrieval Server

@modelcontextprotocol

An MCP server implementation for retrieving information from the AWS Knowledge Base using the Bedrock Agent Runtime.

a year ago

Redis

@modelcontextprotocol

A Model Context Protocol server that provides access to Redis databases. This server enables LLMs to interact with Redis key-value stores through a set of standardized tools.

a year ago

12 days ago

百度地图核心API现已全面兼容MCP协议，是国内首家兼容MCP协议的地图服务商。

a year ago

Github

@modelcontextprotocol

Repository management, file operations, and GitHub API integration

a year ago

12 days ago

12 days ago

Pakistan Payments Mcp

@junter1989k-ai

12 days ago

302_sandbox_mcp

@302ai

Create a remote sandbox that can execute code/run commands/upload and download files. 创建远程沙盒，可以执行代码/运行命令/上传下载文件

a year ago

mcp-server-flomo MCP Server

@chatmcp

Write notes to Flomo

JavaScript

a year ago

Qiniu MCP Server

@Qiniu

基于七牛云产品构建的 Model Context Protocol (MCP) Server，支持用户在 AI 大模型客户端的上下文中通过该 MCP Server 来访问七牛云存储资源、利用 Dora 服务进行图片操作等。如果有什么需求欢迎在下方评论，您也可以在 github 仓库中提 issue。

Python

a year ago

ShareMyPage

@Henning Witzel-Acikgöz

Host the HTML or Markdown pages your AI generates and share each as a link with comments, versioning, and access control. Create, update, and organize pages and read reviewer comments over MCP.

12 days ago

AxProver

Axiomatic Prover — MCP Server

Connect

Tools

Submit (async — returns a job_id)

Poll

Links

Recommend Servers

Submit (async — returns a `job_id`)