Neo4j-backed Lean context for coding theory

Formalization context, shaped for proof agents.

CodingTheoryLib MCP turns a curated graph of Lean declarations, problem/example chunks, natural-language notes, dependencies, and Mathlib stubs into compact context packs for any MCP-aware proof agent.

Connect an MCP client Open API key console Preview the corpus

Agent Tool Surface

This page currently documents only the 6 implemented core tools for the active L3:v5 graph. Raw Cypher and graph mutation stay private; MCP tools return only proof_usable=true nodes as structured context that proof agents can paste into Lean-oriented workflows.

  • search_declarationscandidate search
  • search_examples_and_problemsexample/problem search
  • get_declaration_contextexact declaration details
  • get_dependency_contextrequired dependency context
  • get_dependency_summarycompact dependency counts
  • get_graph_snapshot_statuscoverage and ingest metadata

What a proof agent receives

Each tool returns bounded JSON aimed at a different stage of Lean formalization work. Move through the slides to see the shape of the payload a proof agent can rely on.

Tool 1 of 6

search_declarations

Find proof-usable declaration candidates from a topic query. Problem/example nodes are off by default for ordinary theorem proof work; opt in only for textbook exercises or examples.

{
  "result": [
    {
      "name": "HuffmanPless.duadicSquareRootBound_basicBound",
      "type": "theorem",
      "module": "CodingTheoryLib.HuffmanPless.Chapter6.Section_Weights",
      "type_signature": "theorem ... : C.minimumOddLikeWeight ^ 2 >= C.n",
      "score": 0.89,
      "confidence": "high",
      "proof_status": "proven",
      "dependency_health": "trusted",
      "warnings": []
    }
  ]
}
Tool 2 of 6

search_examples_and_problems

Search only proof-usable textbook examples and problems. It uses the same internal scoring/reranking as declaration search, returns a final score, and includes code by default.

{
  "query": "dual weight enumerator",
  "type": "problems",
  "mode": "textbook_alignment",
  "results": [
    {
      "name": "Problem18_dualWeightEnumerator",
      "node_type": "problem_theorem",
      "statement": "theorem Problem18_dualWeightEnumerator : ...",
      "code": "theorem Problem18_dualWeightEnumerator : ... := by ...",
      "score": 0.88,
      "confidence": "high"
    }
  ]
}
Tool 3 of 6

get_declaration_context

Expand one known proof-usable declaration into textbook links, docstring, stored Lean code, source, dependency count, helper names, and optional one-hop dependency summary.

{
  "declaration": {
    "name": "weightEnumerator_60_30_12",
    "statement": "theorem weightEnumerator_60_30_12 : ...",
    "docstring": "Weight enumerator theorem for a self-dual code.",
    "code": "theorem weightEnumerator_60_30_12 : ... := by ...",
    "source": "CodingTheoryLib/core/weight/Enumerator.lean:241-268"
  },
  "textbook_links": [],
  "helper_names": [],
  "dependency_count": 3,
  "lean_code": "theorem weightEnumerator_60_30_12 : ... := by ..."
}
Tool 4 of 6

get_dependency_context

Show proof-usable declarations needed to complete a known declaration. For ordinary theorem proof context, leave problem/example nodes off and omit PROBLEM_NEEDS/EXAMPLE_NEEDS; enable those only for exercise carriers.

{
  "name": "weightEnumerator_60_30_12",
  "direction": "out",
  "depth": 2,
  "include_problems": false,
  "include_examples": false,
  "edge_types": ["NEEDS_DEFINITION", "NEEDS_LEMMA", "NEEDS_THEOREM"],
  "node_types": ["theorem", "def"],
  "internal": [
    {
      "name": "selfDual_weightEnumerator_helper",
      "node_type": "theorem",
      "statement": "theorem selfDual_weightEnumerator_helper : ...",
      "docstring": "Helper theorem used by the weight enumerator theorem.",
      "depth": 1
    }
  ],
  "edges": [
    {
      "source": "weightEnumerator_60_30_12",
      "target": "selfDual_weightEnumerator_helper",
      "edge_type": "NEEDS_THEOREM"
    }
  ]
}
Tool 5 of 6

get_dependency_summary

Show only the proof-usable target and dependency node_type counts for one theorem, problem, or example. Use this for a quick view such as def/theorem/lemma/structure counts.

{
  "target": {
    "name": "weightEnumerator_60_30_12",
    "node_type": "problem_theorem"
  },
  "dependency_summary": {
    "total": 18,
    "node_type_counts": {
      "def": 7,
      "lemma": 2,
      "structure": 3,
      "theorem": 6
    }
  }
}
Tool 6 of 6

get_graph_snapshot_status

Active graph namespace, embedding model, CSV node_type labels, indexes, node counts, edge counts, coverage, and recommended retrieval workflows.

{
  "graph_namespace": "CodingLIB_LYJ:L3:v5",
  "embedding_model": "google/gemini-embedding-2",
  "node_labels": "csv_node_type",
  "proof_usable_filter": true,
  "node_counts": {"theorem": 6800, "def": 2618},
  "edge_counts": {"NEEDS_DEFINITION": 9183}
}
Topic search Use search_declarations to compare ordinary declaration candidates. Keep problem/example nodes off unless the task is explicitly textbook-oriented.
Examples/problems Use search_examples_and_problems only when the task is an exercise, example, or problem carrier.
Dependencies Use get_dependency_context with ordinary NEEDS_* edges by default; add PROBLEM_NEEDS or EXAMPLE_NEEDS only by explicit opt-in.
Known name Use get_declaration_context to inspect docs, Lean code, source, helpers, textbook links, and dependency count.

Generate Your API Key

Invite beta users can sign in with GitHub and generate a bearer token for MCP clients. The raw token is shown once; the server stores only its SHA-256 hash and provider identity metadata.

GitHub login

Use this when your coding-theory work already lives in GitHub. The OAuth flow requests basic profile and email access only.

Continue with GitHub

Public boundary

Public: service code, website, tests, docs, and agent skills in the GitHub repository. Private: Neo4j credentials, OpenRouter key, GitHub OAuth secret, bearer tokens, runtime SQLite logs, and admin graph tooling.

Open GitHub repo

After generation, copy the token into your local environment as CODINGTHEORY_MCP_TOKEN. Do not commit it to a repository or paste it into issue trackers.

Connect From Any MCP Client

The service is a remote Streamable HTTP MCP server. Ask for a bearer token, then point your MCP host or client at the Railway endpoint and enable only the read-only context tools you need.

Codex Claude Code Claude Desktop Claude custom connectors Cursor-style MCP clients VS Code MCP hosts Any Streamable HTTP client

Remote endpoint

Use these values in any MCP-compatible client that supports remote HTTP servers and bearer authentication.

Transportstreamable-http
URLhttps://codingtheorylib.com/mcp
AuthAuthorization: Bearer $CODINGTHEORY_MCP_TOKEN
HealthGET /healthz

Client checklist

Most MCP hosts use the same primitives even when their setup UI differs.

  • Register the server name as codingTheoryLib or another stable alias.
  • Set the remote URL to the full /mcp endpoint, not the website root.
  • Attach the bearer token through your client's secret or header mechanism.
  • After connecting, list tools and test get_graph_snapshot_status.
  • Grant only read-only context retrieval permissions; this server has no write or Lean execution path.

Codex

codex mcp add codingTheoryLib   --url https://codingtheorylib.com/mcp   --bearer-token-env-var CODINGTHEORY_MCP_TOKEN

Store CODINGTHEORY_MCP_TOKEN outside the repo and expose it through your Codex environment.

[mcp_servers.codingTheoryLib]
url = "https://codingtheorylib.com/mcp"
bearer_token_env_var = "CODINGTHEORY_MCP_TOKEN"

Claude Code

claude mcp add --transport http --scope user codingTheoryLib   https://codingtheorylib.com/mcp   --header "Authorization: Bearer $CODINGTHEORY_MCP_TOKEN"

The same endpoint also serves this operations page and /healthz for Railway checks.

Claude Desktop

Edit ~/Library/Application Support/Claude/claude_desktop_config.json on macOS, then restart Claude Desktop.

{
  "mcpServers": {
    "codingTheoryLib": {
      "command": "/bin/bash",
      "args": [
        "-lc",
        "npx -y mcp-remote https://codingtheorylib.com/mcp --header "Authorization: Bearer $CODINGTHEORY_MCP_TOKEN""
      ]
    }
  }
}

Because desktop apps may not inherit your shell environment, either launch Claude with CODINGTHEORY_MCP_TOKEN set or replace the command with a local wrapper script that reads a private env file outside the repository.

Claude Desktop skills

Register the agent skills separately from MCP. In Claude Desktop, open Customize → Skills → Personal Skills → +, then add each skill folder or a zip containing the folder and its SKILL.md.

cd CodingTheoryLib-MCP/skills
zip -qr codingtheory-proof-context.zip codingtheory-proof-context
zip -qr codingtheory-textbook-formalization.zip codingtheory-textbook-formalization
zip -qr codingtheory-research-problem.zip codingtheory-research-problem

Use codingtheory-proof-context for ordinary proof context. Problem/example nodes stay off by default; enable them only for textbook exercises or carriers.

JSON-based MCP clients

{
  "mcpServers": {
    "codingTheoryLib": {
      "type": "http",
      "url": "https://codingtheorylib.com/mcp",
      "headers": {
        "Authorization": "Bearer ${CODINGTHEORY_MCP_TOKEN}"
      }
    }
  }
}

Use this shape for clients that ask for a JSON MCP server map instead of a CLI command.

Environment setup

export CODINGTHEORY_MCP_TOKEN="..."

For macOS desktop apps launched outside your shell, set the same variable through your app launcher or OS environment before restarting the client.

MCP Ecosystem Readiness

MCP directories and marketplaces help users discover servers, compare risk, and copy install metadata. CodingTheoryLib MCP is designed to be easy to evaluate before it is broadly listed.

Protocol profile

  • Capabilities: tools only; no public resources or prompt templates yet.
  • Transport: remote Streamable HTTP at /mcp.
  • Security: invite bearer token, read-only graph access, no raw Cypher.
  • Runtime: Railway service with Neo4j graph retrieval and SQLite quota/debug logs.

Directory listing copy

CodingTheoryLib MCP is a read-only context server for coding theory formalization. It gives proof agents structured access to Lean declarations, Pless and Huffman-Pless problem/example chunks, natural-language proof notes, dependency neighborhoods, and suggested imports.

MCP server guide Remote MCP guide MCP Market

Operating Model

This MCP server is intentionally light. Neo4j stores the graph and vector indexes; OpenRouter embeds only the incoming query; Railway runs the HTTP process and a small SQLite cache on a mounted volume. There is no Lean verifier, no LLM proof generator, and no write path exposed to public MCP clients.