MCP

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

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.