Agent skills for CodingTheoryLib MCP.

These skills package the QA-tested MCP workflows into reusable instructions for Codex-style agents. They are separate from the MCP server: install the skills locally, then connect the MCP endpoint as codingTheoryLib.

Skill Pack

Textbook Formalization

codingtheory-textbook-formalization

Turn Pless or Huffman-Pless labels into exact Lean names, source modules, reusable APIs, and scoped formalization plans.

Trigger: Use when the user gives a book/chapter/theorem/exercise label or quoted textbook statement.

View skill

Proof Context

codingtheory-proof-context

Gather compact Lean context before writing, repairing, or reviewing coding-theory proof code.

Trigger: Use when the next step is a Lean edit and the agent needs imports, signatures, dependencies, or examples.

View skill

Research Problem

codingtheory-research-problem

Explore open problems safely by separating carriers, solved endpoints, obstruction theorems, and next subproblems.

Trigger: Use for hard research-problem scenarios like the MCP QA report.

View skill

Install

Install the public skills from the GitHub repository, then restart Codex so the skills are discovered.

git clone https://github.com/LeGenAI/CodingTheoryLib-MCP.git
mkdir -p ~/.codex/skills
cp -R CodingTheoryLib-MCP/skills/codingtheory-* ~/.codex/skills/

Use With MCP

  • Install the MCP server as codingTheoryLib.
  • Generate a GitHub API key at /access.
  • Use the skill that matches the task: textbook label, proof edit, or research problem.
  • Keep secrets out of prompts, repositories, screenshots, and logs.