モデルコンテキストプロトコル Axiom Lean Engineのサーバー — Lean を公開 AIエージェントへの検証と操作ツール。

インストール

1. 無料の API キーを作成する: [https://axle.axiommath.ai/app/console.]
2. 顧客を接続して下さい:

##Claude(ウェブ、デスクトップ、モバイル)

1. 開いた カスタマイズ → コネクター →Add → カスタム コネクタを追加。
2. 名前: Axle。 リモート MCP サーバー URL: [https://mcp.axiommath.ai/mcp] 。 *Addをクリックします。 3。 [Add] をクリックして、デフォルトのクライアント設定を承諾します。 4。Connectをクリックし、サインインページでAPIキーを貼り付けます。 5。 チャットで、+**メニュー→コネクタを開き、Axleをオンにします。

##チャットGPT

有料プランと開発者モード(Settings → Security and login)が必要です。

1. ChatGPT プラグイン →+ を開きます。
2. 名前: Axle。 MCP サーバー URL: [https://mcp.axiommath.ai/mcp] 。 認証: OAuth. 3。 それを作成し、サインインページでAPIキーを貼り付けます。 4。 チャットでは、** +** → Developer mode メニューからアクスルを追加します。

##Claudeコード

次に、[/mcpを実行し、開いたページでAPIキーを貼り付けます。 スキップする ブラウザは、キーを直接渡します。

##その他のMCPクライアント(Cursor、Windsurf、VSコード、Cline、…)

AXLE MCP Server

A Model Context Protocol server for Axiom Lean Engine — exposes Lean verification and manipulation tools to AI agents.

Installation

1. Create a free API key: https://axle.axiommath.ai/app/console.
2. Connect your client:

Claude (web, desktop, mobile)

1. Open Customize → Connectors → Add → Add custom connector.
2. Name: Axle. Remote MCP server URL: https://mcp.axiommath.ai/mcp. Click Add.
3. Click Add again to accept the default client settings.
4. Click Connect and paste your API key on the sign-in page.
5. In a chat, open the + menu → Connectors and switch Axle on.

ChatGPT

Needs a paid plan and Developer mode (Settings → Security and login).

1. Open ChatGPT Plugins → +.
2. Name: Axle. MCP server URL: https://mcp.axiommath.ai/mcp. Authentication: OAuth.
3. Create it and paste your API key on the sign-in page.
4. In a chat, add Axle from the + → Developer mode menu.

Claude Code

claude mcp add --transport http axle https://mcp.axiommath.ai/mcp

Then run /mcp and paste your API key on the page that opens. To skip the browser, pass the key directly:

claude mcp add --transport http axle https://mcp.axiommath.ai/mcp \
  --header "Authorization: Bearer your_api_key_here"

Other MCP clients (Cursor, Windsurf, VS Code, Cline, …)

{
  "mcpServers": {
    "axle": {
      "type": "http",
      "url": "https://mcp.axiommath.ai/mcp",
      "headers": {
        "Authorization": "Bearer your_api_key_here"
      }
    }
  }
}

To run the server locally instead (enables file_uri, which reads Lean files from disk):

{
  "mcpServers": {
    "axle": {
      "command": "uvx",
      "args": ["--from", "axiom-axle-mcp", "axle-mcp-server"],
      "env": {
        "AXLE_API_KEY": "your_api_key_here"
      }
    }
  }
}

Tools

Most tools are generated from the AXLE API’s /v1/endpoints — verify_proof, check, merge, sorry2lemma and friends. Alongside them the server provides: