# Archerkattri/mathlas [Health: Active]

**Category:** 🧮 Data Science Tools  
**Repository:** https://github.com/Archerkattri/mathlas  
**GitHub Stars:** 12  
**Views:** 3  
**Installs:** 0  
**Upvotes:** 0  
**Directory Page:** https://allmcps.com/mcp/archerkattri-mathlas

## Description
Airtight math for agents: 3.7M-theorem search, PSLQ constant ID, OEIS, real Lean kernel checks, applicability checklists. No LLM inside, no API key.

## Tools
Capabilities this server exposes over MCP:

- **identify_constant** — Identify a real number's closed form, airtight: PSLQ + closed-form search, every candidate independently re-evaluated to 50+ digits, honest UNIDENTIFIED otherwise. Use when you have a numeric constant and want to know what it IS. Args: value (decimal string — give MANY digits, >16), optional basis (constant names like ['pi','e']).
- **identify_sequence** — Match an integer sequence against a LOCAL OEIS copy by EXACT contiguous term-match (no fuzzy scoring; honest UNDETERMINED if the data files are absent). Use when you have >= 4 integer terms and want the named sequence. Args: terms (list of integers), max_results (default 5).
- **search_existing_math** — Find existing theorems/results for a problem from the mathlas 3.68M-doc index (dense + BM25 + RRF, fused with any live web_added findings). Use FIRST for any 'does known math solve this?' question; follow up with applicability_checklist on promising candidates. Args: query (problem/result description), k (default 10), optional corpus_dir (dataset parquets; omit to serve the prebuilt index or seed corpus), optional source_filter / source_weights to down-weight or exclude corpus sources, e.g. exclude web-mined docs when looking for canonical theorem statements.
- **search_formal_math** — Find mathlib DECLARATIONS (name + type) via the public Loogle (pattern/type queries like '?a * ?b = ?b * ?a') and LeanSearch (natural-language queries) services — the ONE tool that itself calls the web; honest 'service unavailable' if down (though a <=7-day-old cached response for the same query is then served, clearly labeled 'cached' with its age). Use when you need the formal Lean name/type of a result, e.g. before writing a verify_formal snippet. Args: query, k (default 10), backend ('auto'|'loogle'|'leansearch').
- **verify_numeric** — Airtight check that a closed-form expression equals a numeric value: independent sympy re-evaluation at higher precision, verified only on >= 20 agreeing digits. Use BEFORE asserting any numeric identity. Args: value (decimal string), closed_form (e.g. 'pi**2/6', 'zeta(3)').
- **verify_formal** — Run the REAL Lean 4 kernel (NO LLM). Two modes: (1) pass `lean` (a full snippet, e.g. 'example : 2 + 2 = 4 := rfl') to typecheck it as-is; (2) pass `proof` to PROOF-CHECK — `statement` must then be the Lean 4 proposition and `proof` YOUR proof (term or 'by ...' tactic block); mathlas builds `theorem _mathlas_check : <statement> := <proof>` and the kernel returns proof_status VERIFIED_PROOF / REFUTED (kernel_error carries the kernel's exact complaint — use it to repair the proof and re-call) / UNDETERMINED (no toolchain / timeout / unresolvable import — honest, never fake). sorry/admit are REJECTED. mathlas never writes proofs, only checks them. Find declaration names first with search_formal_math. Args: statement, lean?, proof?.
- **applicability_checklist** — Decompose a candidate theorem's statement into atomic preconditions + conclusion for YOU to verify one by one against your problem (catches misapplications like using a closed-interval theorem on an open interval). Use after search, before relying on any candidate. Args: candidate_statement (the result's statement text).
- **mapping_scaffold** — Build the needs<->guarantees scaffold (structured questions + fill-in template) between your problem and a candidate result. Use when applicability is non-obvious and you want structure for the judgment (the judging is yours). Args: problem, candidate_statement.
- **conjecture_relation** — Conjecture relations for a real constant — Ramanujan-Machine style: PSLQ over a rich basis + continued-fraction/recurrence search; every candidate numerically VERIFIED to >= 25 digits but NOT proved (provenance 'conjectured_relation'). Use when identify_constant returns UNIDENTIFIED. Args: value (decimal string, MANY digits), max_terms (default 16), cf_depth (default 200).
- **funsearch** — Sandboxed program-search harness (FunSearch): action='evaluate' scores YOUR Python program for problem_id ('cap_set' or 'online_bin_packing') in a no-network/timeout/rlimit sandbox; action='register' stores a scored program in the MAP-Elites DB; action='status' returns the best programs + few-shot context for writing the next variant. Use to iteratively evolve programs — YOU are the generator, mathlas is the deterministic scorer. Args: action, problem_id, then program_src (evaluate/register), score + behavior (register), timeout_s (evaluate), top_k (status).
- **search_directive** — Get a STRUCTURED web-search plan for a problem — arXiv query strings, sub-fields/categories, named results to look for, and which other mathlas tools to run; mathlas makes NO web call (YOU search, then feed results back via add_finding). Use when the local index missed. Args: problem (description).
- **add_finding** — Ingest a web-found result into the live mathlas corpus so search_existing_math returns it immediately (provenance 'web_added'; BM25 always — no model load; full dense retrieval too if you pass dense_vec embedded in the served index's space). Use after web-searching per search_directive. Args: statement, slogan, source, optional name, optional dense_vec.

## Claude Desktop Quick Installation
Install path detected from listing signals. Uses `uvx` (confidence: high):

```json
"mcpServers": {
  "mathlas": {
    "command": "uvx",
    "args": ["mathlas-mcp"]
  }
}
```

## Documentation

## What Archerkattri/mathlas MCP server does

Archerkattri/mathlas MCP server supplies MCP tools for checking and investigating mathematical claims without embedding an LLM in the server. It can search a 3.68M-document math index, identify constants with PSLQ and closed-form matching, match integer sequences against a local OEIS copy, and independently re-evaluate numerical identities at high precision.

The server also supports formal mathematics workflows. Agents can search public Loogle and LeanSearch services for mathlib declaration names and types, then submit Lean snippets or proofs to the real Lean 4 kernel. Separate tools break a candidate theorem into preconditions and conclusions or create a structured needs-versus-guarantees scaffold. These outputs support the agent's judgment; the server does not decide whether a theorem's assumptions actually hold in the user's problem.

## How it works

Most operations return candidates, verdicts, checklists, or scaffolds for the calling agent to interpret. `search_existing_math` uses dense retrieval, BM25, and reciprocal-rank fusion over the supplied corpus, while `add_finding` can add a result found through the agent's own web search. `search_directive` produces a web-search plan but does not perform the search itself.

`identify_constant` expects a decimal string with many digits and checks proposed forms through independent high-precision evaluation. `verify_numeric` only accepts an identity after at least 20 agreeing digits. `conjecture_relation` can look for unproved relations using PSLQ, continued fractions, and recurrence searches; its results are explicitly conjectural.

`verify_formal` either typechecks a complete Lean snippet or checks a supplied proposition and proof. It rejects `sorry` and `admit`, and reports verified, refuted, kernel-error, or undetermined outcomes according to the available toolchain and result.

## Setup and configuration

The Archerkattri/mathlas MCP server can run over stdio with `uvx mathlas-mcp`, or after installation with `python -m mathlas.server`. The documented Claude Code registration command is:

```bash
claude mcp add mathlas -- uvx mathlas-mcp
```

Optional package extras provide the official MCP SDK, retrieval support for reading index data, and embedding dependencies. The server can fall back to a dependency-free stdio JSON-RPC implementation if the official SDK is unavailable.

Some capabilities depend on local resources. Sequence identification needs a local OEIS copy, and formal verification needs a Lean toolchain. If those resources are missing, the relevant tools report that the data or toolchain is unavailable rather than fabricating a result. The retrieval tool can use its prebuilt index or a supplied corpus directory.

## Tools and capabilities

- Identify numerical constants and integer sequences.
- Verify closed-form numerical identities with independent re-evaluation.
- Search existing mathematical results and formal mathlib declarations.
- Check Lean 4 snippets and proofs with the kernel.
- Decompose theorem assumptions and build applicability scaffolds.
- Generate search plans, ingest web findings, and run the sandboxed FunSearch harness for the supported problem IDs.

Archerkattri/mathlas MCP server is best suited to agent workflows where every claim needs a provenance-aware search result, a deterministic calculation, or a formal verification status.

_Full upstream README: https://allmcps.com/mcp/archerkattri-mathlas/readme_