Neo4j-backed Lean context for coding theory

Formalization context, shaped for proof agents.

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

Connect an MCP client Generate API key Preview the corpus

Agent Tool Surface

The public server exposes a bounded read-only API. Raw Cypher and graph mutation stay private; the MCP tools return structured context that proof agents can paste into Lean-oriented workflows.

  • search_declarationshybrid declaration search
  • get_declaration_contextsignature, docs, textbook links
  • find_textbook_unitstheorem / lemma / exercise lookup
  • build_proof_contextcompact agent context pack
  • explore_dependency_graphbounded internal and external neighbors
  • find_reusable_apicore helpers and stable APIs
  • find_research_problem_contextopen-problem adjacent context
  • 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 8

search_declarations

Ranked Lean declarations with signatures, modules, docstrings, L3 flags, text/vector scores, and source locations.

{
  "result": [
    {
      "name": "HuffmanPless.duadicSquareRootBound_basicBound",
      "kind": "theorem",
      "module": "CodingTheoryLib.HuffmanPless.Chapter6.Section_Weights",
      "type_signature": "theorem ... : C.minimumOddLikeWeight ^ 2 >= C.n",
      "text_score": 25.74,
      "vector_score": 0.89,
      "is_l3_endpoint": true
    }
  ]
}
Tool 2 of 8

get_declaration_context

One declaration expanded into Lean type, textbook units, natural-language notes, dependencies, and verification metadata.

{
  "declaration": {
    "name": "HuffmanPless.chapter6_problem_6_5_3",
    "source_file": "CodingTheoryLib/HuffmanPless/Chapter6/Section_Weights.lean",
    "line_start": 453,
    "verification_level": "L3_local_lean_verified"
  },
  "textbook_units": [{"book": "HuffmanPless", "label": "6.5.3"}],
  "dependencies": {"internal": ["HuffmanPless.SquareRootBoundImprovementResearchProblem"]}
}
Tool 3 of 8

find_textbook_units

Exact or semantic textbook units with book, chapter, section, label, source pages, status, and linked Lean names.

{
  "result": [
    {
      "unit": {
        "book": "HuffmanPless",
        "chapter": 8,
        "section": "8.6",
        "kind": "ResearchProblem",
        "label": "8.6.10"
      },
      "declarations": ["HuffmanPless.chapter8_problem_8_6_10"]
    }
  ]
}
Tool 4 of 8

build_proof_context

A budgeted proof pack containing seed declarations, suggested imports, nearby dependencies, docs, and notes.

{
  "seed_names": [
    "HuffmanPless.chapter7_problem_7_10_14",
    "HuffmanPless.chapter7_problem_433"
  ],
  "suggested_imports": [
    "CodingTheoryLib.HuffmanPless.Chapter7.Section5"
  ],
  "chars": 4690,
  "context": "name: ... signature: ... notes: ..."
}
Tool 5 of 8

explore_dependency_graph

Graph neighbors split into internal CodingTheoryLib declarations and external Mathlib or field stubs.

{
  "name": "HuffmanPless.chapter8_problem_8_6_10",
  "internal": [
    {"name": "HuffmanPless.NonPrimePowerProjectivePlaneResearchProblem", "depth": 1}
  ],
  "external": [
    {"name": "P.bruckRyserChowlaObstructionStatement", "depth": 1}
  ]
}
Tool 6 of 8

find_reusable_api

Reusable structures, definitions, lemmas, theorem wrappers, and helper APIs suitable for new Lean work.

{
  "result": [
    {
      "name": "HuffmanPless.SimplexHammingWeightHierarchyCertificate",
      "kind": "structure",
      "module": "CodingTheoryLib.HuffmanPless.Chapter7.Section5"
    },
    {
      "name": "HuffmanPless.qaryHammingHierarchy_formula",
      "kind": "theorem"
    }
  ]
}
Tool 7 of 8

find_research_problem_context

ResearchProblem units with carrier declarations, formalization notes, related endpoints, and candidate dependencies.

{
  "result": [
    {
      "unit": {"label": "7.10.14", "kind": "ResearchProblem"},
      "declarations": [
        {"name": "HuffmanPless.chapter7_problem_7_10_14"}
      ],
      "docs": [{"heading": "Natural-language proof sketch"}]
    }
  ]
}
Tool 8 of 8

get_graph_snapshot_status

Graph namespace, embedding model, node counts, textbook coverage, ingest metadata, and recommended workflows.

{
  "graph_namespace": "CodingTheoryLib:L3:v1",
  "embedding_model": "google/gemini-embedding-2",
  "node_counts": {"Declaration": 17019, "TextbookUnit": 2115},
  "coverage": [{"book": "HuffmanPless", "implemented": 1454, "units": 1472}]
}
Exact label Use find_textbook_units, then open each Lean name with get_declaration_context.
Theorem topic Use find_textbook_units or search_declarations; then fetch declaration context.
Proof drafting Use build_proof_context once the goal is concrete, with an explicit budget.
Open problem Use find_research_problem_context only for research-target discovery, not ordinary theorem lookup.

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 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.

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 textbook units, 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.