CodingTheoryLib / CodingTheoryLib-MCP
Formal coding-theory knowledge shaped into a reusable substrate for theorem-proving agents.
A formalized coding-theory substrate: Lean definitions, proof work, graph memory, and MCP-style access for agents.
problem
General theorem-proving models struggle when a research topic depends on local definitions, naming conventions, and domain-specific theorem structure.
why it matters
If a mathematical domain has no formal, searchable substrate, every agent must rediscover the vocabulary before it can reason productively.
maker note
The goal is not only to prove isolated theorems. I want a working memory for a mathematical domain, something a prover agent can actually search and reuse.
what I built
- • Lean/Mathlib formalization work around coding theory
- • A graph/MCP direction for exposing the library to agents
- • Project scaffolding for domain-specific formal memory
evidence
- • Core thesis project in the portfolio
- • Connected to the LLM-Lean award thread and building-up/self-dual-code work
current status
Active research substrate; public preview and documentation are being shaped around the long-term AI4Math direction.
next step
Make the agent-facing interface and example workflows clearer for external readers.
role
Lead builder/researcher for the agent-readable coding-theory substrate direction.
tags
artifact links
Coderelated publications
Proposal of an LLM-Lean Approach and Architecture for Automated Mathematical Problem SolvingA Lean-facing multi-agent math-solving architecture where a falsifier makes the solver loop more inspectable and efficient.SolEvolve: LLM-driven Evolutionary Discovery of AlgorithmsAn LLM-guided evolutionary search system for discovering and testing coding-theoretic constructions.