mathlas — Claude Code MCP server: what it does, how to install
Adds 12 rigorous tools to your AI agent for searching theorems, identifying numeric constants, and checking formal proofs in Lean 4.
claude mcp add --env MATHLAS_SEED=<MATHLAS_SEED> --env MATHLAS_INDEX=<MATHLAS_INDEX> --transport stdio mathlas -- uvx mathlas-mcpWhat mathlas does
The server shifts mathematical tasks from AI guessing to deterministic algorithms. Under the hood, it inspects an index of 3.68M mathematical documents, generates precondition checklists, and discovers closed-form constants to 50 digits using PSLQ. No language model runs inside the package; it passes structured candidates and exact verification verdicts back to the client.
Everything operates over stdio using the MCP SDK or a lightweight JSON-RPC fallback. Detailed checks via verify_formal depend on a local Lean toolchain, while sequence searches query a local OEIS snapshot. Without Lean installed, verify_formal reports the missing toolchain instead of producing a speculative pass.
What it helps with
- retrieve theorem statements and applicability conditions across 3.68M indexed documents
- recover closed-form constants from 50-digit floating-point values via PSLQ
- typecheck mathematical proofs against the Lean 4 kernel
- match integer sequences against the local OEIS database
Example prompts for the agent
- Search for the Banach fixed-point theorem and extract its required conditions
- Identify the closed-form expression for 0.7390851332151607 using PSLQ
- Run
verify_formalon this Lean lemma to verify there are no unproven steps
How to install mathlas
Platform CLI
claude mcp add --env MATHLAS_SEED=<MATHLAS_SEED> --env MATHLAS_INDEX=<MATHLAS_INDEX> --transport stdio mathlas -- uvx mathlas-mcpReplace <…> with your own values. uvx runs the command named after the package; if the README names another one, use uvx --from mathlas-mcp <command>
Platform CLI
codex mcp add mathlas --env MATHLAS_SEED=<MATHLAS_SEED> --env MATHLAS_INDEX=<MATHLAS_INDEX> -- uvx mathlas-mcpReplace <…> with your own values. uvx runs the command named after the package; if the README names another one, use uvx --from mathlas-mcp <command>
Config file
{
"mcpServers": {
"mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
],
"env": {
"MATHLAS_SEED": "<MATHLAS_SEED>",
"MATHLAS_INDEX": "<MATHLAS_INDEX>"
}
}
}
}Replace <…> with your own values. uvx runs the command named after the package; if the README names another one, use uvx --from mathlas-mcp <command>
Config file
{
"servers": {
"mathlas": {
"type": "stdio",
"command": "uvx",
"args": [
"mathlas-mcp"
],
"env": {
"MATHLAS_SEED": "<MATHLAS_SEED>",
"MATHLAS_INDEX": "<MATHLAS_INDEX>"
}
}
}
}Replace <…> with your own values. uvx runs the command named after the package; if the README names another one, use uvx --from mathlas-mcp <command>
Platform CLI
gemini mcp add -e MATHLAS_SEED=<MATHLAS_SEED> -e MATHLAS_INDEX=<MATHLAS_INDEX> mathlas uvx mathlas-mcpReplace <…> with your own values. uvx runs the command named after the package; if the README names another one, use uvx --from mathlas-mcp <command>
Step by step, with commands for each platform: How to add an MCP server to Claude Code, Codex, Cursor, VS Code, Gemini CLI and more
Questions about mathlas
How to install mathlas in Claude Code?
Run claude mcp add mathlas -- uvx mathlas-mcp in your console. The runner uses uv to manage the environment automatically.
What does mathlas do?
It gives your agent twelve deterministic tools for theorem retrieval, constant discovery, and formal proof verification in Lean.
Does mathlas require an external API key?
No API key is required because all calculations run locally without relying on external language model APIs.
