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.
Details
- Author
- Archerkattri
- Downloads
- 200
- Categories
- Search, Knowledge Base, Other, AI
Jump to
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
{
"mcpServers": {
"mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
}
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.
