LabscoMCP early access ↗
ArcherkattriMCP SERVER

mathlas

Twelve tools that check maths instead of generating it — a Lean kernel typecheck, PSLQ constant identification, OEIS matching, and a 3.68M-document theorem index.

by Archerkattri ↗Physical Sciences & Scientific ComputingCommunity

LABSCO 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

See installation options