Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@quarry-mcp search the corpus for Poisson"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
An MCP (Model Context Protocol) server for querying a Lean 4 proof corpus registry.
pip install -e .Related MCP server: Atlas
Run the MCP server over stdio:
quarry-mcp --db PATH/to/quarry-fixture.sqlite serveOr via Python module:
python -m quarry_mcp --db PATH/to/quarry-fixture.sqlite serveOne-shot tool invocation:
quarry-mcp --db PATH/to/quarry-fixture.sqlite call quarry.search '{"query": "Poisson"}'quarry.search — Full-text or hash search
quarry.get — Get declaration by ID
quarry.closure — Compute dependency/dependent closure
quarry.similar — Find similar declarations
quarry.stats — Get corpus statistics
MIT
The web workspace adds a browser UI over the same Quarry schema. It has no additional dependencies.
python3 -m quarry_mcp.web --db fixtures/quarry-fixture.sqlite --state ./quarry-workspace.sqlite --port 8791Open http://127.0.0.1:8791. To browse a remote registry, run the web app on
that machine and forward its loopback port over SSH:
ssh -N -L 8791:127.0.0.1:8791 user@remote-hostSearch real declarations by name or statement; filter by source package and declaration kind, with pagination.
Inspect full statements, source revision links, recorded axioms, module names, authorship, and direct dependencies/dependents (up to 100 in each direction). Missing external declarations are explicitly labelled.
Save declarations, maintain notes, and register local proofs with statement, source, module, and toolchain metadata.
Export a JSON selection manifest including pinned corpus IDs, source revisions encoded in IDs, toolchains, statement hashes, notes, and review blockers. This is not a Lake lockfile and does not install packages. Mixed Lean/Mathlib selections require porting and re-verification.
The corpus is opened with SQLite mode=ro; management data lives in the separate --state SQLite file. Back up that file to preserve registrations and notes. New registrations always remain unverified. “Recorded sorry-free” means only that the extractor recorded no sorryAx and no nonstandard axioms; the app does not run Lean, execute submitted source, audit transitive dependencies, or independently validate corpus-level verification claims. The importer currently attaches a Navier–Stokes comparator claim to Mathlib too, so the UI deliberately labels those as source-provided claims.
The server listens only on loopback and is intended for a private SSH workspace. It checks Host and requires a same-origin token on mutations. It is not a public multi-user service. Local drafts stay registered when removed from the selection; find them in Registrations and save them again at any time.
Run the integration tests (requires permission to bind a temporary localhost port):
python3 -m unittest tests.test_web -v
node --check quarry_mcp/static/app.jsThis server cannot be deployed
Ask a codebase what calls what: search, blast radius, paths between symbols, and diffs.
Ingest and search LogsLoom logs from coding agents.
Turn a GitHub repo or docs site into agent-ready context: pack it or search it, over MCP.
Resolve, search and verify legal citations against the official sources, with provenance.
