Mathlas

Overview

Mathlas is a Model Context Protocol (MCP) server: Airtight math for AI agents: 3.68M-doc theorem search + numeric/Lean verification. No LLM, no key. In practice that means any MCP-compatible AI assistant can call Mathlas's tools directly — the model decides when to use them in a conversation or agent run.

It runs locally: the Python package mathlas-mcp (via uvx) speaks MCP over stdio on your machine. No credentials are required — it works out of the box. The current release is v1.5.0, published under the Apache-2.0 license, with source at Archerkattri/mathlas on GitHub, where it has earned 12 stars.

Mathlas is listed under AI & Agents on mcp.site and works with any MCP client — Claude Desktop, Claude Code, Cursor, VS Code, Windsurf, Zed and the rest of the ecosystem — using the install snippets below. If you maintain Mathlas for Archerkattri, claim this listing to verify ownership, earn the Verified badge, and keep the details current.

Installation

// claude_desktop_config.json
{
  "mcpServers": {
    "mathlas": {
      "command": "uvx",
      "args": [
        "mathlas-mcp"
      ]
    }
  }
}