Coding theory context for proof agents.

CodingTheoryLib serves a read-only MCP over a Neo4j graph of Lean declarations, Pless and Huffman-Pless textbook units, documentation fragments, and dependency neighborhoods. Agent skills package the best workflows so Codex and Claude Code know how to use it.

Explore the MCP server Install agent skills Generate GitHub API key
8MCP tools
3agent skills
2115textbook units
17019Lean declarations

Choose the surface

MCP Server

Remote Streamable HTTP endpoint for structured retrieval: declarations, textbook units, reusable APIs, dependencies, and proof context packs.

Open MCP guide

Agent Skills

Three installable skills teach agents when to call each MCP tool for textbook formalization, proof context, and open research problems.

Open skills guide

GitHub Access

The public repository hosts the service, website, tests, docs, and skills. GitHub OAuth issues beta bearer tokens for the MCP endpoint.

Open GitHub

Public Boundary

Safe to publish

  • Railway-ready MCP server source code.
  • Static website and install snippets.
  • Agent skill folders under skills/.
  • Tests, docs, and public graph schema descriptions.

Never publish

  • Neo4j URI credentials or admin tooling access.
  • OpenRouter key and GitHub OAuth client secret.
  • Raw bearer tokens or token hashes from production users.
  • Runtime SQLite logs, query logs, and private beta identity data.