AtpMcp

AtpMcp

AtpClient の4つの定理証明バックエンド、SystemOnTPTP、StarExec、Isabelle、LocalExecを、Claude Codeやその他のMCPホスト向けのツールとして公開する MCP サーバーです。

stdio（JSON-RPC 2.0）でMCPリビジョン 2026-07-28 を話します。このリビジョンのみをサポートしており、initialize ハンドシェイクが必要なクライアント（2025-11-25以前）は拒否されます。

Dockerですぐに開始

イメージにはサーバー、Erlang、E proverが含まれているため、Dockerだけで始められます。プロジェクトの .mcp.json にサーバーを追加します。

{
  "mcpServers": {
    "atp": {
      "command": "docker",
      "args": ["run", "-i", "--rm", "ghcr.io/jcschuster/atp_mcp:latest"]
    }
  }
}

これにより、設定なしでSystemOnTPTP（tptp.org上のすべての証明器）とローカルのE（backend: "local_exec" を指定した query_backend）を利用できます。

Isabelleも利用する場合は、latest-isabelle タグを使用してください（amd64、数GB。HOLセッションにはコンテナに数GBのRAMが必要です）。サーバーは最初のIsabelle呼び出し時にIsabelle自体を起動するため、最大1分かかることがあります。同じセッション内のそれ以降の呼び出しでは再利用されます。

サーバーを設定するには、プロジェクトを /work にマウントします。サーバーはそこで atp_mcp.exs を探し、ファイルが読み込む環境変数を渡します。

{
  "mcpServers": {
    "atp": {
      "command": "docker",
      "args": [
        "run",
        "-i",
        "--rm",
        "-v",
        "${PWD}:/work:ro",
        "-e",
        "STAREXEC_USER",
        "-e",
        "STAREXEC_PASS",
        "ghcr.io/jcschuster/atp_mcp:latest"
      ],
      "env": { "STAREXEC_USER": "me", "STAREXEC_PASS": "…" }
    }
  }
}

Claude Codeでは、.claude/settings.json でサーバーも承認してください。

{
  "enabledMcpjsonServers": ["atp"]
}

イメージを自分でビルドするには、次のようにします。

docker build -t atp_mcp .                             # SystemOnTPTP + E
docker build -t atp_mcp:isabelle --target isabelle .  # + Isabelle/HOL

escriptのインストール

Dockerを使わない場合は、escript（Elixir 1.20／OTP 29）をインストールします。

mix escript.install hex atp_mcp
export PATH="$HOME/.mix/escripts:$PATH"

そして .mcp.json で "command": "atp_mcp" を使用します。ローカルバックエンドは、その後 PATH 上にあるものを使用します。local_exec には eprover、Isabelleバックエンドには isabelle が必要です。

設定

escriptはプロジェクトの config/*.exs を読み込みません。起動時に次のうち最初に見つかった設定ファイルを読み込みます。

1. atp_mcp --config PATH；
2. ATP_MCP_CONFIG 環境変数；
3. 作業ディレクトリにある atp_mcp.exs。MCPホストではプロジェクトルート（コンテナ内の /work）です。

このファイルは通常のElixir Config で、起動時に評価されます。秘密情報をファイルに書き込まず、環境変数から読み込んでください。

# atp_mcp.exs
import Config

config :atp_client, :sotptp,
  default_system: "Vampire",       # a bare name runs the latest version
  default_time_limit_sec: 30

config :atp_client, :local_exec,
  binary: "vampire",
  args: ["--mode", "casc", "-t", "30"],
  cpu_timeout_s: 30

config :atp_client, :starexec,
  base_url: "https://starexec.example.org/starexec",
  username: System.get_env("STAREXEC_USER"),
  password: System.get_env("STAREXEC_PASS")

設定がない場合：

• SystemOnTPTP はtptp.orgと最新の E を使用します。

• eprover が PATH 上にある場合、LocalExec は eprover --auto --tstp-format --cpu-limit=30 を実行します。

• isabelle が PATH 上にある場合、Isabelle は空きポートで atp_mcp という名前の常駐サーバーを起動します。すでに起動していれば再利用します。コンテナ外では、このサーバーはMCPプロセス終了後も動作し続けるため、後続のセッションでは起動時間を省けます。isabelle server -n atp_mcp -x で停止できます。自分で起動したサーバーを使う場合は、代わりに次のように設定します。

  config :atp_client, :isabelle,
    host: "isabelle.example.org",
    port: 9999,
    password: System.get_env("ISABELLE_PASSWORD")
  

  また、ローカルサーバーが起動しないように config :atp_mcp, isabelle_autostart: false を設定してください。

• StarExec にはデフォルト設定がありません。base_url、username、password が必要です。

すべての設定については、AtpClientのドキュメントを参照してください。

セットアップの確認

atp_mcp doctor は、各バックエンドについて解決された設定と、接続可能かどうかを表示します。MCPホストがサーバーを実行する方法と同じ方法で実行してください。

$ docker run --rm -v "$PWD:/work:ro" ghcr.io/jcschuster/atp_mcp doctor
atp_mcp 0.8.0
config file: /work/atp_mcp.exs

sotptp - SystemOnTPTP
  url: "https://tptp.org/cgi-bin/SystemOnTPTPFormReply"
  default_system: "Vampire"
  default_time_limit_sec: 30
  check: OK
…

確認するバックエンドを指定すると、そのバックエンドのみをチェックします（atp_mcp doctor sotptp local_exec）。いずれかのチェックに失敗すると終了ステータス1を返します。パスワードは設定済みか未設定かのみ表示されます。

ツール

複数バックエンド共通（統合 AtpClient.Backend）

list_backends

サーバーが公開するすべてのバックエンド（sotptp、isabelle、local_exec、starexec）と、人が読めるラベルを一覧表示します。

describe_szs

SZS オントロジーのテキストリファレンスを返します。これは、すべての証明器の判定結果が報告される語彙です。Success ステータス（Theorem、Unsatisfiable、Satisfiable、CounterSatisfiable、ContradictoryAxioms、…）と NoSuccess ステータス（GaveUp、Timeout、ResourceOut、MemoryOut、Forced、InputError、…）を、ニーモニックと定義とともにすべて一覧表示するため、エージェントは MCP セッションを離れずに判定結果の意味を判断できます。判定結果が照合されるテーブル Tptp.Szs.Ontology から生成されます。引数は不要です。

verify_backend

バックエンドの設定と到達可能性を確認します。OK または内容を説明するエラーを返します。

引数	型	必須	説明
backend	string	はい	sotptp | isabelle | local_exec | starexec

バックエンド固有のオーバーライドキー（base_url、password、binary、…）は、バックエンドの verify/1 にそのまま渡されます。

query_backend

統一された c:AtpClient.Backend.query/2 エントリポイントを通じて、TPTP 形式の問題を任意のバックエンドに送信し、SZS オントロジーの判定結果（Theorem、Unsatisfiable、Satisfiable、CounterSatisfiable、GaveUp、Timeout、ResourceOut、…）を返します。語彙の全一覧は describe_szs を呼び出してください。

引数	型	必須	説明
backend	string	はい	sotptp | isabelle | local_exec | starexec
problem	string	はい	TPTP 問題テキスト
time_limit_sec	integer	いいえ	これを尊重するバックエンド（sotptp）で適用される制限時間
raw	boolean	いいえ	SZS 判定結果の代わりに、システムの出力をそのまま返します

バックエンドごとのオーバーライドはそのまま渡されます（例：local_exec の binary、isabelle の timeout_ms、starexec の base_url、および local_exec のバイナリまたは starexec のソルバーの背後にある証明器の SystemOnTPTP 名を指定し、その出力を読み取るための system）。

SystemOnTPTP

list_provers

SystemOnTPTP で利用可能なすべての定理証明器システムを一覧表示します。

run_prover

TPTP の問題を指定した証明器に送信し、SZS ステータスを返します。

引数	型	必須	説明
problem	string	はい	TPTP 問題テキスト
system_id	string	はい	list_provers の証明器 ID、または最新バージョンを指定する単独の名前（Vampire）
time_limit_sec	integer	いいえ	秒単位の制限時間
raw	boolean	いいえ	SZS 判定結果の代わりに、証明器の出力をそのまま返します

compare_provers

同じ問題を複数の証明器に同時に実行し、指定されたシステムごとに指定順で 1 行ずつ、すべての結果を並べて返します。単独の名前を指定すると、実行されたバージョンが表示されます。

Vampire (Vampire---5.0.1): CounterSatisfiable
E---3.5.1: CounterSatisfiable
Nope: not a system on SystemOnTPTP (see list_provers)

引数	型	必須	説明
problem	string	はい	TPTP 問題テキスト
system_ids	string[]	はい	比較する証明器 ID または単独の名前
time_limit_sec	integer	いいえ	証明器ごとの制限時間（秒）

Isabelle

prove_isabelle

手書きの Isabelle/HOL 理論を、設定済みの Isabelle サーバーに送信します。理論テキストは設定された共有ディレクトリに書き込まれ、use_theories 経由で処理されます。TPTP/THF 問題には、代わりに backend: "isabelle" を指定して query_backend を使用してください。こちらは prove_tptp 経由で処理されます。セッション、ホスト、ポート、パスワードは設定からのみ取得されます。

引数	型	必須	説明
theory	string	はい	Isabelle 理論テキスト（全体または本文のみ）
theory_name	string	はい	理論名（.thy ファイル名にも使用）
timeout_ms	integer	いいえ	use_theories の全体タイムアウト（ミリ秒）
raw	boolean	いいえ	判定結果ではなく、Isabelle のメッセージテキストを返す

診断

lint_problem

TPTP 問題に対して構文と型の診断を実行します。デフォルトでは、プロセス内の tptp リンター（Tptp.analyze/2）と SystemOnTPTP 上の TPTP4X を組み合わせます。簡易チェックのみを行うには、backends: ["local"] を渡します。ローカルチェックですでにエラーが見つかった場合、TPTP4X はスキップされます。各指摘は line:column [severity] (source) message [code] の形式で報告され、リンターがヒントを提示する場合はそのヒントも含まれます。その後に、宣言されたシンボルとその型が続きます。

2:8 [warning] (tptp) "axim" is not a TPTP formula role [TPTP0401]
    hint: expected one of axiom, hypothesis, definition, …
2:12 [error] (tptp4x) Invalid role, exiting [TPTP4X]

Symbols:
  plus : $i > $i (declared at 1:14)

引数	型	必須	説明
problem	string	はい	TPTP 問題テキスト
backends	string[]	いいえ	["local", "tptp4x"] のサブセット。デフォルトでは両方を実行

例

MCP サーバーがアクティブになったら、Claude Code に次のように尋ねることができます。

「SystemOnTPTP 上でこの TPTP 問題を証明できる証明器はどれですか？ Vampire、E、Satallax を比較してください。」

Claude は compare_provers を直接呼び出し、SZS の結果を報告します。

「この問題をローカルの E ビルドで実行してから、SystemOnTPTP で妥当性を確認してください。」

Claude は query_backend を 2 回呼び出します。1 回目は backend: "local_exec"、2 回目は backend: "sotptp" を指定し、判定結果を比較します。

エージェントスキル

skills/atp-mcp/SKILL.md は、エージェントにこれらのツールの使い方を教える Agent Skill です。TPTP の各方言と、それらを受け付ける証明器、リンティング後に証明を行うワークフロー、各 SZS 判定から導ける結論について説明します。また、自動形式化、証明の検証、反例の発見など、証明器が役立つタスクも紹介しているため、エージェントは促されなくてもツールを活用できます。Claude Code で使用するには、ディレクトリをプロジェクト内の .claude/skills/ または ~/.claude/skills/ にコピーしてください。

キャンセルと進行状況

時間のかかるツール呼び出しは、それぞれ専用の Task 内で実行されます。MCP ホストは次の操作ができます。

• 実行中のリクエスト ID を指定して notifications/cancelled を送信し、呼び出しを中止します。呼び出し元が終了すると、各 AtpClient バックエンドは上流の処理を終了します。

  • LocalExec は Port のクローズを通じて証明器のバイナリに SIGKILL を送信します。
  • StarExec はリモートジョブに対して DELETE を実行します。
  • Isabelle はセッションを切断し、サーバー上の実行中の use_theories タスクを中止します。
  • SystemOnTPTP はローカル接続を閉じますが、リモートの証明器は :time_limit_sec まで実行されます。SOTPTP にはリモートキャンセル用のエンドポイントがありません。

• 呼び出しの実行中に定期的な notifications/progress フレームを受け取るには、tools/call に _meta.progressToken を設定します。ハートビートはデフォルトで 5 秒ごとに送信されます。次の方法で変更できます。

  config :atp_mcp, heartbeat_ms: 10_000
  

追記：MCP Tasks 拡張

MCP Tasks（今すぐ呼び出し、後からタスクハンドルで取得）は、ATP ワークフローにほぼそのまま適合します。リビジョン 2026-07-28 で、Tasks はコアプロトコルから公式拡張 io.modelcontextprotocol/tasks に移されました。MCP ホストがこの拡張に対応すれば、ここにある長時間実行ツールはタスクを返すようになり、StarExec のような submit_job / await_job の組み合わせも自然に実現できます。

ライセンス

MIT.