Mathlas
About
Airtight math for AI agents: 3.7M-theorem search, PSLQ constant ID, OEIS, real Lean 4 kernel checks. No LLM inside, no API key.
Explore
Setting up with Highlight
This MCP is not yet compatible with Highlight’s one-click setup. However, you can still use it with Highlight by following these steps:
- Download and install Highlight from highlightai.com/download
- Navigate to the plugins tab and select "Add Custom Plugin"
-
Configure the plugin with the settings below
Plugin Name
MathlasCommand (node, npx, python, etc.)Please refer to the README for specific instructions on how to obtain API keys or other required environment variables.
- Enable "Start Automatically" if you want the plugin to start when Highlight launches
From the repository
One line, nothing to install first (needs](https://github.com/Archerkattri/mathlas/blob/HEAD/assets/gen/capture_outputs.py)uv):
claude mcp add mathlas -- uvx mathlas-mcp
uvx mathlas-mcpfetches + runs the server in an isolated env on first use. Prefer pip?
pip install mathlas-mcp # core: numeric + retrieval + verify + scaffolds pip install 'mathlas-mcp[mcp]' # + official MCP SDK pip install 'mathlas-mcp[retrieve]' # + pyarrow, to read the real index pip install 'mathlas-mcp[embed]' # + sentence-transformers/torch, for the Qwen3 embedder claude mcp add mathlas -- python -m mathlas.server
mathlas now appears astwelvetools the agent can call. The server prefers the officialmcpSDK andfalls back to a dependency-free stdio JSON-RPC serverifmcpisn't installed — it always runs. (Cursor / any MCP client: point it at the sameuvx mathlas-mcporpython -m mathlas.serverstdio command.)
Optional local data (degrades honestly):identify_sequencewants a local OEIS copy;verify_formalwants a Lean toolchain. Without them the tools return a clear "data/toolchain not available" — never a fake answer. See[docs/methods.mdfor the one-line setup of each.
User: "Does x = cos(x) have a unique solution I can reach by iterating?" AI → search_existing_math("contraction mapping unique fixed point complete metric space") ← ](https://github.com/Archerkattri/mathlas/blob/HEAD/docs/methods.md#data--toolchains-optional-gitignored-removable)[{name:"Banach Fixed-Point Theorem", statement:"Let (X,d) be a complete metric space and T a contraction. Then T has a unique fixed point ...", ...}, ...] AI → applicability_checklist(banach.statement) ← preconditions: ["(X,d) is a complete metric space", "T: X→X is a contraction"] conclusion: "T has a unique fixed point" AI (reasons): [0,1] is complete; cos is a contraction there (|cos'|=|sin|≤sin 1<1). Every precondition holds ⇒ Banach applies ⇒ unique fixed point, reachable by iteration. AI → verify_numeric("0.7390851332151607", "<the Dottie-number closed form, if claimed>")
mathlas supplied the search, the checklist, and the airtight numeric check. The AI did the judging.No LLM was called inside mathlas.
The discipline isairtight-or-nothing: a result is an independently-checkable fact or an honest "nothing." Thefalse-positive rate is 0 across every tier(full tables + commands inRESULTS.md):
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 given18 math tasksWITH the live mathlas MCP server as its only tool vs WITHOUT any tools scores18/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 goes8/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.
The 3.68M-doc index.search_existing_mathis served from a3,683,428-documentdense index (Qwen3-Embedding-8B, 4096-d): the1.34Mpermissive CC-BY/CC0 TheoremSearch subset +2.34Mslogan-embedded arXiv-math documents from Dolma, dense + Okapi-BM25 + RRF. Honest headline recall at full 3.68M scale:R@1 0.614 / R@10 0.832querying by a document's rawbodyagainst its slogan-embedded entry — the hardcross-representationself-recall regime. (At the earlier 1.635M build, the easier same-representation slogan→slogan self-recall was R@1 0.977 / R@10 0.998 on its 81,833-doc held-out split.)
Open corpus on Hugging Face.The text + metadata side of that index is published atkattri15/mathlas-corpus: 3,683,428 theorem-level documents plus the smallfindingsconfig, split intotheoremsearch,dolma, andfindingsconfigs. It includes slogans, LaTeX statements, source URLs, titles, labels, categories, citation counts where known, and provenance keys. It doesnotinclude the 30 GB embedding matrices or local benchmark slices. Licenses are per config: TheoremSearch subset CC BY-SA 4.0, Dolma statements ODC-BY 1.0 with our slogans CC BY 4.0, and findings CC BY 4.0. Full audit:docs/HF_DATASET_LICENSING.md.
from datasets import load_dataset ts = load_dataset("kattri15/mathlas-corpus", "theoremsearch", split="train") dolma = load_dataset("kattri15/mathlas-corpus", "dolma", split="train")
Quantized laptop tier (opt-in).The fp16 matrix is 30 GB on disk (~60 GB fp32 resident) — fine on the build box, not on a laptop.MATHLAS_QUANTIZED=binary(orquantized="binary"onHybridRetriever.from_index) serves the SAME index from memmapped quantized sidecars instead: sign-bit Hamming over1.9 GBshortlists 1000 candidates, exact rescore picks the top-k — measured on the full 3.68M index with the same n=3000 protocol as the headline, it isrecall-lossless(R@1 0.6143 vs 0.6140 fp16, R@10 equal at 0.8323; int8 mode: R@1 0.6147, 15 GB) at2.4 s/query on 4 CPU threads. Honest caveat: this shrinks thedocumentside only — queries must still be embedded by the same Qwen3-Embedding-8B(a small 0.6B encoder lives in a different vector space). The true end-to-end small-encoder tier is the 0.6B tier below. Numbers, build command, and the caveat in full:docs/QUANTIZED_TIER.md.
0.6B end-to-end laptop tier (opt-in).The SAME 3,683,428-doc corpus re-embedded once withQwen3-Embedding-0.6B(1024-d, row-aligned with the served meta), so the query encoder itself runs on a laptop CPU:MATHLAS_ENCODER=0.6b(composes withMATHLAS_QUANTIZED=binary). Measured with the identical n=3000 cross-representation protocol, queries re-encoded by the 0.6B model:R@1 0.545 / R@10 0.745(binary + int8 rescore; the 0.6B fp16 exact scan is 0.544 / 0.745, so quantization is again lossless within the tier). The honest price vs the 8B tier (0.614 / 0.832) is about 7-9pp recall; the dual-channel 8B configuration (0.965 / 0.999) stays the big-box quality ceiling. The laptop headline:end-to-end 0.67 s/query on 4 CPU threads (0.88 s on 2), query encoding included, over all 3.68M documents. Dense-channel footprint: binary sidecar0.47 GB+ 0.6B encoder~1.2 GB(~1.7 GB; int8 rescore source 3.77 GB recommended; full fp16 sibling index 7.54 GB). On the TheoremSearch-110 corpus-only probe the tier scores Hit@20 8.2% / 10.0% theorem/paper vs the 8B tier's 10.0% / 11.8% (both licensing-bounded floors). Full tables, footprints, and caveats:docs/QUANTIZED_TIER.md; build:scripts/build_06b_index.py; eval:scripts/eval_06b_tier.py.
Dual-channel retrieval (opt-in).The 0.614 headline is a cross-representation gap: LaTeX-statement-shaped queries searched against slogan-embedded docs. A second dense channel embeds the same 3,683,428 docs by their cleaned LaTeXstatement(Qwen3-Embedding-8B, row-aligned, built byscripts/build_statement_channel.py) and folds into the dense ranking by per-doc max-sim. Measured on the same n=3000 sample at full corpus scale:R@1 0.614 to 0.965, R@10 0.832 to 0.999. Honest caveats: that eval is a self-retrieval proxy in which the statement channel indexes the very text the queries are drawn from (an exact-text advantage, like BM25's); on the no-leak 110 human-query benchmark the lift is real but partial (paper Hit@20 11.8% to 12.7%). And the second matrix roughly doubles serving RAM (measured at full scale: 150 GB process peak for the dual server vs ~95 GB single-channel; ~2.75 s/query dual dense scan on 2 CPU threads), so it ships strictly opt-in (MATHLAS_STATEMENT_INDEX=/path/index_full_statement.npz, never auto-detected) and is not combinable with the quantized tier. Full numbers and the serving-tier table:docs/RETRIEVAL_UPGRADE_NOTES.md. The production hybrid defaultrrf_kis 10 (measured best at every k tested), plus an opt-in cross-encoder rerank blend (MATHLAS_RERANK=1, Qwen3-Reranker-0.6B, +1.7pp R@1 honest lift). The rerank backend is selectable withMATHLAS_RERANK_MODEL:qwen3(default, Qwen3-Reranker-0.6B, unchanged) orjina-v3(jinaai/jina-reranker-v3,[arXiv:2509.25085— a 0.6B "last but not late" reranker that leads BEIR at the 0.6B scale). Both lazy-load their weights on first use and fall back to the un-reranked fusion (honest stderr note) if torch/transformers or the weights are absent; a typo'd model name raises rather than silently serving the wrong reranker. We ship the wiring, not a jina benchmark number — bring your own weights.
Claude Desktop / Cursor
Paste into your MCP client config file to install this server.
{
"mcpServers": {
"mathlas": {
"mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
}
}McpServers
{
"mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}Available onmcp.so·Glama· listed inawesome-mcp-serversandbest-of-lean4.
An airtight-math tool an AIuses— no LLM, no API key, free.Plug it into Claude Code, Cursor, or any MCP client. TheAI is the brain; mathlas is thehands— it gives the AI the capabilities it lacks and returnsdata(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 byassets/gen/capture_outputs.py.
- You use Claude Code / Cursor and want your AI to stop hallucinating math—search_existing_mathfinds the real theorem from a 3.68M-doc index;verify_numericandverify_formalcheck claims with zero hallucination risk.
- You have a numeric constant or integer sequence you can't identify—identify_constantruns PSLQ + closed-form matching (50-digit precision);identify_sequencedoes an exact OEIS term-match.
- You need the formal (Lean/mathlib) name of a result—search_formal_mathproxies 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 (needsuv):
claude mcp add mathlas -- uvx mathlas-mcp
uvx mathlas-mcpfetches + runs the server in an isolated env on first use. Prefer pip?
pip install mathlas-mcp # core: numeric + retrieval + verify + scaffolds pip install 'mathlas-mcp[mcp]' # + official MCP SDK pip install 'mathlas-mcp[retrieve]' # + pyarrow, to read the real index pip install 'mathlas-mcp[embed]' # + sentence-transformers/torch, for the Qwen3 embedder claude mcp add mathlas -- python -m mathlas.server
mathlas now appears astwelvetools the agent can call. The server prefers the officialmcpSDK andfalls back to a dependency-free stdio JSON-RPC serverifmcpisn't installed — it always runs. (Cursor / any MCP client: point it at the sameuvx mathlas-mcporpython -m mathlas.serverstdio command.)
Optional local data (degrades honestly):identify_sequencewants a local OEIS copy;verify_formalwants a Lean toolchain. Without them the tools return a clear "data/toolchain not available" — never a fake answer. Seedocs/methods.mdfor the one-line setup of each.
A worked example — an AI using the tools
User: "Does x = cos(x) have a unique solution I can reach by iterating?" AI → search_existing_math("contraction mapping unique fixed point complete metric space") ← [{name:"Banach Fixed-Point Theorem", statement:"Let (X,d) be a complete metric space and T a contraction. Then T has a unique fixed point ...", ...}, ...] AI → applicability_checklist(banach.statement) ← preconditions: ["(X,d) is a complete metric space", "T: X→X is a contraction"] conclusion: "T has a unique fixed point" AI (reasons): [0,1] is complete; cos is a contraction there (|cos'|=|sin|≤sin 1<1). Every precondition holds ⇒ Banach applies ⇒ unique fixed point, reachable by iteration. AI → verify_numeric("0.7390851332151607", "<the Dottie-number closed form, if claimed>")
mathlas supplied the search, the checklist, and the airtight numeric check. The AI did the judging.No LLM was called inside mathlas.
The discipline isairtight-or-nothing: a result is an independently-checkable fact or an honest "nothing." Thefalse-positive rate is 0 across every tier(full tables + commands inRESULTS.md):
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 given18 math tasksWITH the live mathlas MCP server as its only tool vs WITHOUT any tools scores18/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 goes8/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.
The 3.68M-doc index.search_existing_mathis served from a3,683,428-documentdense index (Qwen3-Embedding-8B, 4096-d): the1.34Mpermissive CC-BY/CC0 TheoremSearch subset +2.34Mslogan-embedded arXiv-math documents from Dolma, dense + Okapi-BM25 + RRF. Honest headline recall at full 3.68M scale:R@1 0.614 / R@10 0.832querying by a document's rawbodyagainst its slogan-embedded entry — the hardcross-representationself-recall regime. (At the earlier 1.635M build, the easier same-representation slogan→slogan self-recall was R@1 0.977 / R@10 0.998 on its 81,833-doc held-out split.)
Open corpus on Hugging Face.The text + metadata side of that index is published atkattri15/mathlas-corpus: 3,683,428 theorem-level documents plus the smallfindingsconfig, split intotheoremsearch,dolma, andfindingsconfigs. It includes slogans, LaTeX statements, source URLs, titles, labels, categories, citation counts where known, and provenance keys. It doesnotinclude the 30 GB embedding matrices or local benchmark slices. Licenses are per config: TheoremSearch subset CC BY-SA 4.0, Dolma statements ODC-BY 1.0 with our slogans CC BY 4.0, and findings CC BY 4.0. Full audit:[docs/HF_DATASET_LICENSING.md.
from datasets import load_dataset ts = load_dataset("kattri15/mathlas-corpus", "theoremsearch", split="train") dolma = load_dataset("kattri15/mathlas-corpus", "dolma", split="train")
…
Sign in to leave a review
Use Google, GitHub, or an email account so ratings stay tied to real people.
No reviews posted yet.
