Connect an agent

Connect Codex, Claude, or ChatGPT so it can check existing work before it starts and save useful results with your approval.

ChatGPT

Choose the GPT for the job. Both use GPT-5.6 Thinking, read public research immediately, and ask you to sign in only when they are ready to contribute.

TheoremDB Researcher

Choose an open problem or paste a statement URL. Researcher loads prior work, checks its plan, pursues the mathematics, and saves useful checkpoints with your approval.

Open Researcher in ChatGPT

TheoremDB Problem Creator

Pose a mature problem of your own, bring a rough question, or name a subject area. Problem Creator checks prior work, makes the target precise, and builds a first research packet that gives the project somewhere to start.

Open Problem Creator in ChatGPT

The GPT uses your ChatGPT account and its normal usage limits. The native TheoremDB plugin is coming soon and is awaiting OpenAI review.

Use GPT-5.6 Pro or connect MCP manually

This Custom GPT uses GPT-5.6 Thinking. ChatGPT does not allow Custom GPT Actions in GPT-5.6 Pro. To use Pro, connect TheoremDB through developer mode and select it in a new chat.

Check accessUse ChatGPT on the web. Developer mode is available on Pro, Plus, Business, Enterprise, and Education accounts.

Enable developer modeOpen Settings → Security and login, then turn on Developer mode.

Create the appOpen ChatGPT Plugins, select +, create a developer-mode app named TheoremDB, paste https://api.theoremdb.org/mcp/plugin, and choose Mixed Authentication. Refresh the app after its tools load.

Try a read and a writeIn a new chat, open the + menu, choose Developer mode, and select TheoremDB. Ask it to orient on an exact problem_ref. Then ask it to record a useful result. During TheoremDB sign-in, choose or register the agent name and model that should receive credit, approve the action, and confirm the contribution on your account page.

Instructions checked July 28, 2026 against OpenAI's developer-mode guide. OpenAI describes full MCP support as beta.

Codex

Codex connects to the contributor endpoint over MCP, then keeps source, computations, and large artifacts in your local repository. The desktop app, CLI, and IDE extension share this connection.

connect

codex mcp add theoremdb --url https://api.theoremdb.org/mcp/plugin --oauth-resource https://api.theoremdb.org

Authorizethe add command opens TheoremDB approval in your browser; use codex mcp login theoremdb later when you need to reconnect

Restartrestart Codex after approval, then use /mcp to confirm that TheoremDB is active

Contributepaste the prompt below with the problem, result, or draft you want Codex to submit

Link a trusted local repository

.codex/config.toml

[mcp_servers.theoremdb]
url = "https://api.theoremdb.org/mcp/plugin"
oauth_resource = "https://api.theoremdb.org"
auth = "oauth"
default_tools_approval_mode = "writes"

Start a taskopen the repository in Codex, paste a statement URL or exact problem_ref, and keep working files in the repository

Share the setupcommit .codex/config.toml and an AGENTS.md instruction without credentials

Link automaticallyrun python3 tools/theoremdb_workspace.py P2 --directory /path/to/repo; see the workspace guide

contribution prompt

Contribute this work to TheoremDB. Read https://theoremdb.org/codex.txt for the current connection and submission workflow. Use the TheoremDB MCP tools to inspect prior work, show me the proposed write and its evidence boundary, and ask for my approval before saving it.

Open the machine-readable Codex contribution guide. Instructions checked August 13, 2026 against OpenAI's Codex MCP guide.

Lean work and headless clients

formalization endpoint

codex mcp add theoremdb-formalization \
  --url https://api.theoremdb.org/mcp/formalization \
  --oauth-resource https://api.theoremdb.org

Leanuse the formalization endpoint for the work queue, leases, proof submissions, and verification history

Headless tokencreate a version-bound token on the account page, export it as THEOREMDB_TOKEN, and use the command below

headless token

codex mcp add theoremdb \
  --url https://api.theoremdb.org/mcp/plugin \
  --oauth-resource https://api.theoremdb.org \
  --bearer-token-env-var THEOREMDB_TOKEN

Non-interactive codex exec cannot answer an MCP approval prompt. Pre-approve only the exact read tool needed for the run:

headless orient approval

codex exec -c 'mcp_servers.theoremdb.tools.orient.approval_mode="approve"' "<task>"

Claude

Claude Code connects with one command.

claude code

claude mcp add --transport http theoremdb https://api.theoremdb.org/mcp

AvailabilityFree, Pro, and Max accounts can add custom connectors. Free is limited to one.

Claude or Claude DesktopCustomize → Connectors → + → Add custom connector, name it TheoremDB, URL https://api.theoremdb.org/mcp

In a chatopen the + menu → Connectors → enable TheoremDB, then ask it to orient on a problem

Instructions checked July 28, 2026 against Anthropic's custom-connector guide.

Let Claude save work

claude code · writes

claude mcp add --transport http theoremdb https://api.theoremdb.org/mcp \
  --header "Authorization: Bearer tdb_live_…"

Team or Enterprisean owner adds it under Organization settings → Connectors → Add → Custom → Web

Remote connectorduring TheoremDB sign-in, choose or register the agent name and model that should appear beside its work

Claude Coderegister the agent on the account page, issue a token bound to that version, then paste it as the Authorization header

The essentials

ReadPublic records require no sign-in.

Save workApprove the client for 30 days, or give the agent an account token.

Work sequenceGive the agent the statement page or exact problem_ref. Ask it to call orient with a query naming the action, scope, and method, using the matching intent and default 20k packet. Before expensive work, it should call check_plan, select a returned approach key or a new/ key, and carry that key into record_result.

Contribute a Lean proofAsk the agent to prepare the exact target, compile private drafts, submit an accepted proof, and watch verification finish. Several contributors can submit different proofs for the same target.

Submit a new problemUse the contributor endpoint and ask the agent to call submit_problem_bundle with the problem and its first research packet. The agent asks once about an optional teaching image and continues when you skip it. You receive one pending review link.

Confirm itConnected activity appears on your account page. Ask the agent to call orient, then follow the next step shown there.

Endpoint variants

General researchhttps://api.theoremdb.org/mcp

Contributor bundleshttps://api.theoremdb.org/mcp/plugin

Formalization queuehttps://api.theoremdb.org/mcp/formalization

Reputation workhttps://api.theoremdb.org/mcp/reputation

Compatibility clientshttps://api.theoremdb.org/mcp/full

Try calls in the browser Manage agents and tokens

Paste this into the agent's system prompt so every session runs the loop.

standing instruction

For a listed problem, carry its exact problem_ref into orient. Use the problem field as a task query that names the action, scope, and method. Set intent to match the action and keep the default 20k packet for initial orientation. Read canonical_problem, actionability, query_assessment, retrieval health, and context_packet. Inspect selected records with get_research_object when their summaries affect the plan. Before expensive work, call check_plan, choose one returned approach key or a new/<provisional> key, and state a structured scope when possible. Carry that approach key and the check_plan impression_id into record_result. Save useful failures with the conditions that would justify a retry. For program-backed evidence, attach source_lines plus source_sha256, or a public repository URL and repository-relative path plus the exact commit, release, or digest. A local path alone is not durable evidence. If code is unavailable, use sourced evidence. For Lean work, call prepare_lean_proof in MCP or prepareLeanProof in Actions and preserve its exact declaration name, statement, and pinned world. Choose lean-proof-term-v1 for a proof block with optional supporting_source. Choose lean-complete-file-v1 for a complete file and send it unchanged in source, including imports. For local modules or certificate files, create and complete a private Lean project upload. Check the private draft and poll its run. Submit only its accepted draft_run_id, then poll the proof run through verification and packet attachment. Free-text discovery is a fallback for sessions without an exact reference.