AxProver について
AxProverは、Mathlibを使ってコードをコンパイルしたり定理証明を自動化したりするLean 4ユーザー向けのMCPサーバーです。処理は非同期で、ジョブの状態を確認できます。
主な機能
- 01MathlibサンドボックスでLean 4コードをコンパイル
- 02sorryを含む定理を自動証明
- 03非同期ジョブの送信
- 04ジョブの状態と結果を確認
活用シーン
- 01Mathlibを使ったLean 4コードのコンパイル
- 02sorryを含む定理の自動証明
- 03送信した証明ジョブの追跡
MCP 対応
AxProverはストリーミング可能なHTTPでMCPクライアントに接続し、GitHub経由のOAuth 2.1を使用します。コード構築、定理証明、ジョブ状態確認のツールを提供します。
設定
リモートサーバーはインストール不要です。クライアントを選んで設定をコピーするか、ワンクリックで導入できます。
エンドポイント
https://prover.axiomatic-ai.com/mcp/インストールコマンドをコピー
Claude CodeTerminal
claude mcp add --transport http ax-prover-base https://prover.axiomatic-ai.com/mcp/Cursor.cursor/mcp.json
{"mcpServers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}Cursor で開くVS Code.vscode/mcp.json
{"servers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}VS Code で開くClaude Desktopclaude_desktop_config.json
{"mcpServers":{"ax-prover-base":{"type":"http","url":"https://prover.axiomatic-ai.com/mcp/"}}}Windsurf~/.codeium/windsurf/mcp_config.json
{"mcpServers":{"ax-prover-base":{"serverUrl":"https://prover.axiomatic-ai.com/mcp/"}}}コマンドはターミナルで実行し、JSON は各クライアントの MCP 設定に貼り付けて再起動します。認可が必要なサーバーは初回接続時にログインを求めます。
ツール
詳細
Axiomatic Prover — MCP サーバー
Mathlib を使用して定理をコンパイルし、証明する Lean 4 MCP サーバーです。
接続
MCP クライアントに追加します（例：Claude Desktop の claude_desktop_config.json）。
{
"mcpServers": {
"ax-prover": {
"type": "streamable-http",
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}
認証には GitHub 経由の OAuth 2.1 を使用します。MCP クライアントがフローを自動的に処理します。
ツール
送信（非同期 — job_id を返します）
| ツール | 説明 |
|---|---|
lean4_build | Mathlib 対応のサンドボックスで Lean 4 のソースコードをコンパイルします。コンパイルのためにコードは外部クラウドサービスに送信され、証明を行う場合は AI 処理のためにも送信されます。 |
lean4_prove_theorems | sorry を含む Lean 4 の定理を自動的に証明します。コンパイルと AI による証明のために、コードは外部クラウドサービスに送信されます。 |
ポーリング
| ツール | 説明 |
|---|---|
lean4_get_job_status | ax-prover の任意のジョブのステータスと結果をポーリングします。 |
送信ツールはすべて非同期です。すぐに job_id を返します。
ステータスが completed または failed になるまで、lean4_get_job_status(job_id) でポーリングしてください。
リンク
コメント
Markdown 対応
AI アプリケーションが外部のツールやデータソースに統一的な方法で接続するためのオープンなプロトコルです。クライアントはモデルとの対話を担い、MCP サーバーはツール・リソース・プロンプトテンプレートを提供します。標準メッセージでやり取りするため、1 つのサーバーを複数のクライアントで再利用できます。