Summary

The failure modes are designed, which is rarer than the features.

A `sorry` hole is REJECTED even though Lean itself exits 0 on a sorried proof; a missing toolchain, a timeout or an unresolvable import returns UNDETERMINED rather than a verdict; a downed upstream service returns a labelled cached response rather than silence. That discipline is what makes the output usable as evidence. The README is equally frank about retrieval limits — it publishes the honest cross-representation recall rather than the flattering same-representation number.

What it is

An MCP server for airtight mathematics, with no LLM inside any tool. Every call returns data — candidates, verdicts, checklists, scaffolds — for the model to reason over: the AI is the brain, this is the hands. Retrieval runs against its own index; verification runs against a real Lean kernel and independent high-precision re-evaluation, so a wrong claim comes back refuted rather than plausible.

What you get

A query ranked against a 3,683,428-document index combining dense embeddings, BM25 and RRF, with optional source filtering — `search_existing_math`
A numeric value resolved to a known closed form with provenance, at 50-digit precision via PSLQ — `identify_constant`
A claimed closed form checked by a different engine at higher precision, returning a digit-agreement verdict — `verify_numeric`
A Lean statement typechecked, or a full Lean 4 proof kernel-checked, returning `VERIFIED_PROOF`, `REFUTED` with the kernel's exact error for the repair loop, or an honest UNDETERMINED — `verify_formal`
Mathlib declaration names and types via the public Loogle and LeanSearch services, provenance-labelled, with a 7-day on-disk cache that serves the last good response when a service is down — `search_formal_math`
An integer sequence matched exactly against OEIS entries — `identify_sequence`
A result's hypotheses broken into an atomic checklist, and a needs-versus-guarantees template for mapping a theorem onto your problem — `applicability_checklist`, `mapping_scaffold`
PSLQ over a rich basis plus continued-fraction and recurrence conjectures — `conjecture_relation`
A FunSearch harness for sandbox-scoring, registering and inspecting AI-written programs — `funsearch`
A web-search plan naming arXiv queries, sub-fields and which tools to run next — `search_directive`
A web-found result embedded and folded into the live corpus at runtime — `add_finding`

Requirements

No API key and no account: `claude mcp add mathlas -- uvx mathlas-mcp` is the whole install, and `uvx` fetches and runs it in an isolated environment on first use. Or `pip install mathlas-mcp` with optional extras — `[mcp]` for the official SDK, `[retrieve]` for pyarrow to read the real index, `[embed]` for the sentence-transformers embedder. If the `mcp` SDK is absent it falls back to a dependency-free stdio JSON-RPC server, so it always starts. Two tools want local data: sequence identification wants a local OEIS copy, and formal verification wants a Lean toolchain. Without them those tools return a clear "data/toolchain not available" rather than a fabricated answer.

Setup effort

One command — claude mcp add mathlas -- uvx mathlas-mcp