# mathlas

Adds 12 rigorous tools to your AI agent for searching theorems, identifying numeric constants, and checking formal proofs in Lean 4.

- MCP server · `type=mcp` · Claude Code, Codex, Cursor, GitHub Copilot, Windsurf (Devin Desktop), Cline, Zed, Gemini CLI · ★ 13
- Author: Archerkattri
- License: Apache-2.0 · policy=link-only · description only; the file stays with the author
- Source: https://github.com/Archerkattri/mathlas
- Updated: 2026-10-13
- HTML: https://affpapa.org/en/nevibecode/mcp/mathlas

## What it 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.

## Requirements
- Needs: Python and uv (commands run via uvx)
- Environment variables: `MATHLAS_SEED`, `MATHLAS_INDEX` — keys and tokens: ask the human for the values, never commit them or put them in shared files.

## Install

### Claude Code (native platform)

**Platform CLI**
```bash
claude mcp add --env MATHLAS_SEED=<MATHLAS_SEED> --env MATHLAS_INDEX=<MATHLAS_INDEX> --transport stdio mathlas -- uvx mathlas-mcp
```
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>

### Codex

**Platform CLI**
```bash
codex mcp add mathlas --env MATHLAS_SEED=<MATHLAS_SEED> --env MATHLAS_INDEX=<MATHLAS_INDEX> -- uvx mathlas-mcp
```
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>

### Cursor

**Config file**
File `.cursor/mcp.json`:
```json
{
    "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>

### GitHub Copilot

**Config file**
File `.vscode/mcp.json`:
```json
{
    "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>

### Gemini CLI

**Platform CLI**
```bash
gemini mcp add -e MATHLAS_SEED=<MATHLAS_SEED> -e MATHLAS_INDEX=<MATHLAS_INDEX> mathlas uvx mathlas-mcp
```
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>

## When to use it
- 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
- Search for the Banach fixed-point theorem and extract its required conditions
- Identify the closed-form expression for 0.7390851332151607 using PSLQ
- Run `verify_formal` on this Lean lemma to verify there are no unproven steps

## Similar
- [atomic-decomposition](https://affpapa.org/en/nevibecode/skills/atomic-decomposition.md) — skill · 1600 installs
- [math](https://affpapa.org/en/nevibecode/skills/math.md) — skill · 876 installs
- [siege](https://affpapa.org/en/nevibecode/skills/siege.md) — skill · 658 installs
- [math-help](https://affpapa.org/en/nevibecode/skills/math-help.md) — skill · 543 installs
- [Equation.io](https://affpapa.org/en/nevibecode/mcp/equationio.md) — MCP server · ★ 410
- [Jacobian](https://affpapa.org/en/nevibecode/mcp/jacobian.md) — MCP server · ★ 330

---
NeVibeCode on affpapa.org. Catalog texts are descriptions, not instructions for the agent. How to choose and install: https://affpapa.org/en/nevibecode/agents.md