Lean Mathlib 搜索服务

lean-mathlib-mcp

A machine-first MCP server for structured, low-ambiguity search over the Lean Mathlib 4 knowledge base (definitions, theorems, lemmas, notations, modules, instances, typeclasses, axioms).

It is a ground-up rewrite of the reference implementation CriticalLine/lean-mathlib-docs-mcp, re-targeted from "string search for humans" to "structured semantic retrieval for LLM agents".

Design principles

• Machine-first. Every tool returns a single JSON string with a stable schema — directly parseable, no prose dumps.
• Precision over fuzzy semantics. Exact qualified name > short name + namespace > signature/conclusion structure > domain + intent.
• Complete metadata. A unified entity model covers definitions / theorems / lemmas / notations / modules / instances / typeclasses / axioms, with source, dependencies, status, and a stable id.
• Controllable granularity. Per-call terse | summary | complete | expanded, plus max_results, cursor pagination, and a soft token_budget.
• Read-only, structured errors. No write/exec path. Failures return an error code + corrective suggestions + negative-result feedback.

Architecture

docgen master index declaration-data.bmp  ──►  MasterIndexSource.load()
                                                │  (neutral SourceBundle)
                                                ▼
                                      MathlibIndex  (compact secondary index + lazy entity materialization)
                                                │
        ┌───────────────┬───────────────┬───────┴────┬──────────────────┐
        ▼               ▼               ▼            ▼                  ▼
   search/identity  search/semantic  search/context  search/scoring   sources/
   (exact identity) (semantic feats) (graph context) (relevance rank) docgen_detail
        │               │               │                              (optional enrichment)
        └───────────────┴───────────────┴──────────────────────────────┘
                                                ▼
                                      output.assemble()  → SearchResult (JSON)
                                                ▼
                                      MCPServer (stdio)  → 15 @server.tool

• sources/ — SourceBundle is a neutral data contract. MasterIndexSource parses the official master index; DocgenDetailProvider optionally supplies type signatures / docs / true dependency graphs (graceful degradation if absent).
• index.py — the production master index has 425k+ declarations. To avoid hundreds of MB of startup cost, a compact DeclMeta is kept per declaration for filtering, and the rich entity object is materialized lazily, only for returned results.
• search/ — identity (exact identity) / semantic (semantic features) / context (graph context) + scoring (weighted ranking).
• output.py — granularity projection + cursor pagination + token-budget truncation + reuse params + negative feedback.
• server.py — MCPServer("lean-mathlib-mcp") registers 15 tools via @server.tool; _dispatch routes all calls (sync request/response; the batch tool shares the same path).

Data sources & enrichment

The master index declaration-data.bmp (official docgen export) contains the declarations / modules / instances / instancesFor sections, but not type signatures, docs, or true dependency graphs. Those rich features come from an optional docgen4 JSON export:

• Without docgen_detail_path, search_by_signature / search_by_conclusion / search_hypothesis / search_proof_complexity and the "true dependencies" of expand_dependencies return an enrichment_unavailable error code with a fix suggestion instead of garbage.
• search_by_domain_use / search_declaration / search_by_notation / module_snapshot and the topology fallback (module import graph) are always available.

Installation

Requires Python 3.11+ (mcp>=2, pydantic>=2, pydantic-settings).

# from a clone of this repo
python -m pip install -e .          # installs the `lean-mathlib-mcp` console script
python -m pip install -r requirements.txt   # or pin manually

An offline sample index (data/sample_index.json, ~3.4k declarations / 115 modules) ships with the repo so the tests and a quick smoke run work without downloading anything.

Running (stdio)

# via the installed console script
lean-mathlib-mcp

# or, without installing, via the module
LEAN_MATHLIB_DATA_SOURCE=sample python -m lean_mathlib_mcp

# or via the bundled launcher (adds src/ to sys.path automatically)
LEAN_MATHLIB_DATA_SOURCE=sample python run_server.py

• LEAN_MATHLIB_DATA_SOURCE=auto (default): use the local sample/cache if present, otherwise download the production index.
• LEAN_MATHLIB_DATA_SOURCE=remote: force-download the full production index (network required).
• LEAN_MATHLIB_DATA_SOURCE=sample: force the committed offline fixture (deterministic).

Connecting from an MCP client (e.g. WorkBuddy)

Copy mcp.example.json to mcp.json, set command to your Python interpreter, and trust the server in your connector manager. Example:

{
  "servers": {
    "lean_mathlib_mcp": {
      "command": "python",
      "args": ["run_server.py"],
      "env": { "LEAN_MATHLIB_DATA_SOURCE": "auto" }
    }
  }
}

If the package is published to PyPI, uvx lean-mathlib-mcp works as the command.

Configuration

All knobs are environment-overridable (prefix LEAN_MATHLIB_), so the server deploys read-only with zero code changes.

Tools (15, all read-only)

Tools marked ⚡ enrichment return enrichment_unavailable when LEAN_MATHLIB_DOCGEN_DETAIL_PATH is unset. Shared output controls (most tools): granularity ∈ {terse,summary,complete,expanded}, max_results, min_score, token_budget, scope_modules, exclude_modules, mathlib_only, exclude_deprecated, only_stable, cursor.

3.1 Exact-identity search

3.2 Semantic-feature search

3.3 Association & context search

3.4 Service & batch

Output schema

SearchResult

{
  "query": { /* echoed query params */ },
  "total_matches": 326,
  "returned": 5,
  "next_cursor": "5",            // pagination cursor; null when exhausted
  "truncated_low_relevance": false,
  "hits": [ /* SearchHit[] */ ],
  "reuse_params": { "full_name": "...", "id": "decl:..." },
  "negative_feedback": {         // present only when hits is empty
    "reason": "no matching entity for the given query",
    "relax_suggestions": [ "..." ]
  }
}

SearchHit

{
  "entity": { /* MathlibEntity projection (per granularity) */ },
  "score": 0.95,                 // 0..1 relevance
  "tier": "exact",               // exact | structural | semantic | domain | usage
  "match_dimensions": [ { "dimension": "exact_name", "score": 1.0, "tier": "exact" } ],
  "truncated": false,
  "reuse_params": { "full_name": "...", "id": "decl:..." }
}

MathlibEntity (field names are stable across Mathlib versions)

id · entity_type · raw_kind · full_name · short_name · namespace · module · type_signature · statement · doc · domain · subdomain · use_tags · doc_link · relations (dependencies/dependents/equivalents/ generalizes/specializes/related) · status (deprecated/maintenance/ cache_key) · is_core · usage_frequency · enrichment_source.

granularity projection:

• terse: id / full_name / entity_type / module / domain
• summary: + short_name / doc_link / use_tags / is_core / usage_frequency
• complete: + type_signature / statement / subdomain / relations (light)
• expanded: + doc / full relations / status

Structured error

{
  "code": "enrichment_unavailable",   // see table below
  "message": "this search needs the docgen detail export",
  "fixable": true,
  "suggested_params": { "docgen_detail_path": "<path to docgen JSON>" },
  "disambiguation": [ /* on ambiguous_match */ ],
  "negative_feedback": { /* on no_match */ }
}

Relevance ranking

score = 0.45·name + 0.20·structure + 0.15·domain + 0.10·usage + 0.10·stability; tier order exact > structural > semantic > domain > usage. Collisions and ambiguity are surfaced explicitly via ambiguous_match rather than guessed.

Extending

• New data source: implement the DataSource / DetailProvider protocols in sources/__init__.py, produce a SourceBundle, and wire it into server.build_index().
• New detail provider: subclass DocgenDetailProvider and feed an external export (signatures / proof terms) into bundle.enriched[name].
• New tool: add an @server.tool function in server.py (prefix the function name with tool_ to avoid clashing with same-named search.* helpers), add a branch in _dispatch, and reuse assemble / make_error.

Testing

# unit tests (20): index, search, server wiring
python -m pytest tests/ -q

# real MCP stdio end-to-end (spawns the server subprocess over the protocol)
python tests/e2e_stdio.py

Build / rebuild fixtures and cache:

python -m lean_mathlib_mcp.builder sample   # slice multi-domain sample from the real master index
python -m lean_mathlib_mcp.builder build    # build the index cache
python -m lean_mathlib_mcp.builder info     # index statistics

Known limitations

• Rich features (signatures / conclusions / true dependencies / proof structure) depend on the optional docgen4 export; without it the relevant tools return enrichment_unavailable and degrade gracefully.
• In the master index, declaration names have no Mathlib. prefix (e.g. Add, Nat.add); mathlib_only is decided by whether the owning module is under Mathlib.* (default false, i.e. core library is not filtered out).
• The production index has 425k+ declarations; the first build downloads and parses declaration-data.bmp (~67 MB), then reuses data/cache afterward.

Credits

Refactored from CriticalLine/lean-mathlib-docs-mcp. Data is sourced from the Lean community's Mathlib 4 docgen.

License

MIT — see LICENSE.