lambdapi-agents

AI-agent tooling for the Lambdapi proof assistant — an MCP server, an agent skill, an edit-time check hook, and a benchmarking arena, in one repo.

The goal: let an LLM agent write, check, and repair Lambdapi (.lp) proofs, and measure how well it does under different tool configurations.

Components

Dir	What
mcp/	Standalone MCP server exposing lambdapi lsp to any client — check, goals, query, try, symbols, axioms
skills/	Agent skill (skills/lambdapi/) teaching Lambdapi syntax, tactics, and the tool surface
hooks/	PostToolUse hook that type-checks .lp files on edit and feeds diagnostics + proof state back to the agent
arena/	Benchmarking harness + proof corpora for evaluating agents across configurations

The MCP and the skill are the two ends of the "MCP vs skill" question the project explores: the MCP gives the agent a rigid, structured tool interface; the skill gives it prose guidance and lets it drive the lambdapi CLI itself. The arena measures which wins, and where.

Quickstart

As a Claude Code plugin (skill + server + hook)

/plugin marketplace add Deducteam/lambdapi-agents
/plugin install lambdapi-agents@deducteam

Installs the skill, wires up the MCP server, and enables the edit-time type-check hook — in one step. The pieces also work on their own:

MCP server (any MCP client)

cd mcp
pip install -e ".[dev]"
pytest                    # Stdlib-dependent tests skip if the Stdlib is absent
lambdapi-mcp --help       # the server

Point a client at uv run --directory mcp lambdapi-mcp from a checkout (or uvx lambdapi-mcp once published). See mcp/README.md for per-client config.

Skill (standalone)

cp -r skills/lambdapi ~/.claude/skills/lambdapi

It drives the lambdapi CLI directly. See skills/README.md.

Edit-time check hook (standalone)

Register hooks/lp_check.py as a PostToolUse hook in your project's .claude/settings.json to type-check every .lp edit and feed the diagnostics and proof state back to the agent. See hooks/README.md.

Arena

Proof corpora live in arena/corpora/; the evaluation harness is under construction. See arena/README.md.

Requirements

• A lambdapi binary on PATH (opam install lambdapi)
• Python 3.10+ for the MCP server
• The Lambdapi Stdlib for proof-exercising tools (the opam install already provides it under lambdapi's lib_root)

Layout

mcp/              standalone Python MCP server (PyPI-publishable)
skills/lambdapi/  the agent skill (SKILL.md + references/)
hooks/            edit-time .lp type-check hook (bundled in the plugin)
arena/            benchmarking harness + proof corpora
.claude-plugin/   Claude Code plugin + marketplace manifests (thin glue)
.mcp.json         dev: auto-wire the server when using Claude Code in this repo

Provenance

Folded together from two prototypes — lambdapi-mcp (server + skill) and lambdapi-skill (CLI skill + mirrored upstream docs) — into a single repo. History restarts here; the originals keep theirs.

License

Apache-2.0.