Archerkattri/mathlas

**Available on** mcp.so · Glama · listed in awesome-mcp-servers and best-of-lean4.
> **An airtight-math tool an AI *uses* — no LLM, no API key, free.** Plug it into
> Claude Code, Cursor, or any MCP client. The **AI is the brain**; mathlas is the
> **hands** — it gives the AI the capabilities it lacks and returns *data*
> (candidates, verdicts, checklists, scaffolds) for the AI to reason over.
> Apache-2.0. The code is free for any use; published corpus/index artifacts carry their own per-source terms (CC-BY/CC0).
Every verdict from the real Lean 4.31.0 kernel / PSLQ + an independent re-eval — no LLM inside. Real in-process tool outputs, captured by assets/gen/capture_outputs.py .
---
Is this for you?
- **You use Claude Code / Cursor and want your AI to stop hallucinating math** — search_existing_math finds the real theorem from a 3.68M-doc index; verify_numeric and verify_formal check claims with zero hallucination risk.
- **You have a numeric constant or integer sequence you can't identify** — identify_constant runs PSLQ + closed-form matching (50-digit precision); identify_sequence does an exact OEIS term-match.
- **You need the formal (Lean/mathlib) name of a result** — search_formal_math proxies the public Loogle + LeanSearch services and returns declaration names + types, provenance-labeled.
- **You're building an agent pipeline that needs airtight math in the loop** — all 12 tools are pure data-returning MCP tools, no LLM inside, composable with any framework.
---
Install & register with Claude Code (no API key)
One line, nothing to install first (needs uv):
uvx mathlas-mcp fetches + runs the server in an isolated env on first use. Prefer pip?
mathlas now appears as **twelve** tools the agent can call. The server prefers the official mcp SDK and **falls back to a dependency-free stdio JSON-RPC server** if mcp isn't installed — it always runs. (Cursor / any MCP client: point it at the same uvx mathlas-mcp or python -m mathlas.server stdio command.)
> **Optional local data (degrades honestly):** identify_sequence wants a local OEIS copy; verify_formal wants a Lean toolchain. Without them the tools return a clear "data/toolchain not available" — never a fake answer. See docs/methods.md for the one-line setup of each.
---
A worked example — an AI using the tools
mathlas supplied the search, the checklist, and the airtight numeric check. The AI did the judging. **No LLM was called inside mathlas.**
---
Results
The discipline is **airtight-or-nothing**: a result is an independently-checkable fact or an honest "nothing." The **false-positive rate is 0 across every tier** (full tables + commands in RESULTS.md):
| Tier | Recovery@known | False-positive | Why it's airtight | Benchmark |
|---|---|---|---|---|
| Numeric (identify_constant) | 8/8 | 0/3 | independent high-precision re-eval (50–51 digits) | benchmarks/numeric_bench.py |
| Sequence (identify_sequence) | 8/8 (7 top-1) | 0/3 | exact term-match vs local OEIS (~400k seqs) | benchmarks/tier_bench.py |
| Formal (verify_formal) | 7/7 verdicts | — | real Lean 4.31.0 kernel typecheck | benchmarks/tier_bench.py |
| Ramanujan (conjecture_relation) | 6/6 | 0/2 | PSLQ + CF, every hit re-verified ≥25 digits | benchmarks/tier_bench.py |
| Applicability moat | 15/15 decomp + 6/6 catch | — | atomic preconditions, misapplication traps | benchmarks/moat_bench.py |
| FunSearch + web-aug | 14/14 | — | sandbox containment (network / timeout / memory) | benchmarks/tools_bench.py |
The table above, at a glance — 0 false positives across every tier (0/8 structureless inputs produced a false hit), 100% recovery on knowns. Numbers: RESULTS.md §1–2b.
**Agent-in-the-loop, honestly reported (2026-06-10, Claude Fable 5):** the same headless agent given **18 math tasks** WITH the live mathlas MCP server as its only tool vs WITHOUT any tools scores **18/18 vs 15/18**. The original 10-task set is saturated (10/10 both ways: a frontier model passes it from parametric knowledge alone, and we say so plainly), so an 8-task hard set was added where verification, not recall, is the bottleneck: that set goes **8/8 WITH vs 5/8 WITHOUT**. The bare model times out on 50-digit integer-relation detection (PSLQ) and cannot name obscure OEIS sequences that shadow Catalan/Fibonacci prefixes and only diverge at depth. The bare passes it does earn are remarkable and we report them: it evaluated a 6-term constant relation to 45 digits by hand (residual 1.475e-27, correct), simulated IEEE-754 rounding bit-for-bit in its head (with one wrong exponent in prose), and proved a Machin-like formula exactly via Gaussian integers, all in-context at 3-9x the latency of a tool call. Every ground truth is a deterministic computation recorded in the bench; full table and provenance: RESULTS.md §2c. Run: benchmarks/agent_bench.py.