Econlib for agents
Formalize with a coding agent that knows the library.
Coding agents are strong Lean collaborators when they can search the library and check their work against the elaborator. Econlib ships an econlib-tools plugin that gives your agent both: a proving skill that encodes the right workflow, and an MCP server for searching Econlib and Mathlib. The plugin works with Claude Code and Codex, and the search server is available to any MCP-capable client directly.
What the plugin provides
econlib-proving — a search-first, fast-feedback workflow for stating theorems faithfully and building proofs against the Lean elaborator.
econlib-search MCP server with
loogle (type- and pattern-shaped) and search
(semantic) tools over both Econlib and Mathlib.
Setup
The plugin lives in the Econlib repository under
agent-plugin/. Clone the repo so you have the plugin directory
locally:
git clone https://github.com/danlyng/Econlib
# plugin directory: Econlib/agent-pluginClaude Code
Point Claude Code at the plugin directory with --plugin-dir. The
flag takes the plugin root — the folder containing
.claude-plugin/ — and applies for the session:
claude --plugin-dir ./Econlib/agent-plugin
This loads the econlib-tools plugin, which registers the
econlib-proving skill and the econlib-search MCP
server. If you edit the plugin mid-session, run
/reload-plugins to pick up the changes.
Codex
Register the plugin directory as a local source, then install
econlib-tools through the codex plugin interface:
codex plugin marketplace add ./Econlib/agent-plugin
codex plugin add econlib-tools
You can also run codex and open /plugins to browse the
source, install econlib-tools, and toggle it on. Installing enables
the bundled skill; the econlib-search MCP server is picked up from
the plugin's config.
MCP server directly
If you just want search — or you use another MCP-capable client — add the HTTP endpoint directly, no plugin required:
https://mcp.lean4.party/mcpWorking well with agents
Agents are most reliable when the ask is precise. Before you hand off a proof, say exactly what statement you want, and how it fits into your model. A vague request produces a theorem that looks right but proves something weaker; a sharp one produces a faithful formalization.
The habits below get the most out of the plugin:
- State the claim precisely. Spell out the exact hypotheses and conclusion — including whether you need both directions of an iff, uniqueness rather than mere existence, and the full statement of any named theorem. Most Lean errors are semantic: a statement that suggests one thing but proves something weaker. Pin down the shape up front.
- Explain how it fits your model. Tell the agent what role the result plays — which definitions it depends on, which downstream result it feeds. This lets it reuse your existing structures instead of reinventing them.
-
Ask it to search first. Econlib and Mathlib already contain
a great deal of infrastructure. The
econlib-searchtools (plusGLOSSARY.mdin the checkout) let the agent find existing lemmas before writing new ones — steer it to search before it formalizes. -
Work in small, checked steps. The proving skill favors fast
feedback: state a scaffold of
have … := by sorrysublemmas, confirm the decomposition composes, then discharge the riskiest leaves first — checking each against the elaborator withlake buildbefore moving on.
See also
The same retrieval the MCP server exposes, in your browser — over Econlib and its Mathlib dependency.
Type- and pattern-based search over Econlib, Mathlib, and Lean by shape, constant, or subexpression.
The full library source, the plugin, and the issue tracker.