CodingTheoryLib serves a read-only MCP over a Neo4j graph of Lean declarations, Pless and Huffman-Pless problem/example chunks, documentation fragments, and dependency neighborhoods. Agent skills package the best workflows so Codex and Claude Code know how to use it.
The graph is organized around two coding theory tracks. Book-linked chunks include Lean declarations, problem/example carriers, helper names, code, and dependency neighborhoods.
Vera Pless's compact text emphasizes the algebraic and combinatorial foundations of linear block codes. The MCP graph tracks the Pless formalization as Lean chunks with problem/example carriers and dependency context.
Good for agent context around parity-check matrices, Hamming codes, cyclic codes, weight enumerators, perfect codes, and classical algebraic constructions.
Huffman and Pless provide a broad graduate-level route through coding theory from mathematical and engineering viewpoints, including classical topics and later techniques that are useful for research formalization.
The graph includes theorem statements, exercises, definitions, and research-problem context for navigating deeper chapters without flooding the model context window.
Remote Streamable HTTP endpoint for structured retrieval: declarations, problem/example nodes, reusable APIs, dependencies, and proof context packs.
Open MCP guideFour installable skills teach agents when to call each MCP tool for textbook formalization, proof context, proof strategy, and open research problems.
Open skills guideThe public repository hosts the service, website, tests, docs, and skills. GitHub OAuth issues beta bearer tokens for the MCP endpoint.
Open GitHubskills/.