Model Context Protocol (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 for kernel_accepted. Repair kernel diagnostics and any rejected target correspondence. Once kernel_accepted is true and the user has authorized submission, call submit_lean_proof or submitLeanProof with that exact draft_run_id, even while correspondence is pending. This saves a submission request that continues automatically after correspondence approval. Private checks alone stay private. Poll the returned proof run and report target review, signed verification, and packet attachment separately. Withdraw a waiting request only when the user asks. Free-text discovery is a fallback for sessions without an exact reference.