広告掲載
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.

コメント

「その他」の他のコンテンツ

ICSS

chokcoco

不止于 CSS

20.7K

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

Glasswarp

Glasswarp

See and control a real Windows PC you own — from any MCP client, locally or remotely. Observe (UIA + screenshots), click/type/drag/scroll, launch apps, owner Live View. BYOH: your machine, your key.

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

Hindsight

vectorize-io

Hindsight: Agent Memory That Learns

50.4K
広告掲載