Skip to main content
Glama
Archerkattri

mathlas

by Archerkattri
OverviewSchemaRelated ServersScoreDiscussions
Python
Local

mathlas

PyPI Downloads DOI mcp.so Glama score License Python HF dataset

Available on mcp.so · Glama · listed in awesome-mcp-servers and best-of-lean4.

An airtight-math tool an AI uses — no LLM, no API key, free. Plug it into Claude Code, Cursor, or any MCP client. The AI is the brain; mathlas is the hands — it gives the AI the capabilities it lacks and returns data (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).

Is this for you?

  • You use Claude Code / Cursor and want your AI to stop hallucinating math — search_existing_math finds the real theorem from a 3.68M-doc index; verify_numeric and verify_formal check claims with zero hallucination risk.

  • You have a numeric constant or integer sequence you can't identify — identify_constant runs PSLQ + closed-form matching (50-digit precision); identify_sequence does an exact OEIS term-match.

  • You need the formal (Lean/mathlib) name of a result — search_formal_math proxies 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.

Related MCP server: SymKit

Install & register with Claude Code (no API key)

One line, nothing to install first (needs uv):

claude mcp add mathlas -- uvx mathlas-mcp

uvx mathlas-mcp fetches + 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 as twelve tools the agent can call. The server prefers the official mcp SDK and falls back to a dependency-free stdio JSON-RPC server if mcp isn't installed — it always runs. (Cursor / any MCP client: point it at the same uvx mathlas-mcp or python -m mathlas.server stdio command.)

Optional local data (degrades honestly): identify_sequence wants a local OEIS copy; verify_formal wants a Lean toolchain. Without them the tools return a clear "data/toolchain not available" — never a fake answer. See docs/methods.md for 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.

Results

The discipline is airtight-or-nothing: a result is an independently-checkable fact or an honest "nothing." The false-positive rate is 0 across every tier (full tables + commands in RESULTS.md):

Tier

Recovery@known

False-positive

Why it's airtight

Benchmark

Numeric (identify_constant)

8/8

0/3

independent high-precision re-eval (50–51 digits)

benchmarks/numeric_bench.py

Sequence (identify_sequence)

8/8 (7 top-1)

0/3

exact term-match vs local OEIS (~400k seqs)

benchmarks/tier_bench.py

Formal (verify_formal)

7/7 verdicts

—

real Lean 4.31.0 kernel typecheck

benchmarks/tier_bench.py

Ramanujan (conjecture_relation)

6/6

0/2

PSLQ + CF, every hit re-verified ≥25 digits

benchmarks/tier_bench.py

Applicability moat

15/15 decomp + 6/6 catch

—

atomic preconditions, misapplication traps

benchmarks/moat_bench.py

FunSearch + web-aug

14/14

—

sandbox containment (network / timeout / memory)

benchmarks/tools_bench.py

Agent-in-the-loop, honestly reported (2026-06-10, Claude Fable 5): the same headless agent given 18 math tasks WITH the live mathlas MCP server as its only tool vs WITHOUT any tools scores 18/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 goes 8/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_math is served from a 3,683,428-document dense index (Qwen3-Embedding-8B, 4096-d): the 1.34M permissive CC-BY/CC0 TheoremSearch subset + 2.34M slogan-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.832 querying by a document's raw body against its slogan-embedded entry — the hard cross-representation self-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 at kattri15/mathlas-corpus: 3,683,428 theorem-level documents plus the small findings config, split into theoremsearch, dolma, and findings configs. It includes slogans, LaTeX statements, source URLs, titles, labels, categories, citation counts where known, and provenance keys. It does not include 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")

Quantized laptop tier (opt-in). The fp16 matrix is 30 GB on disk (~60 GB fp32 resident) — fine on the build box, not on a laptop. MATHLAS_QUANTIZED=binary (or quantized="binary" on HybridRetriever.from_index) serves the SAME index from memmapped quantized sidecars instead: sign-bit Hamming over 1.9 GB shortlists 1000 candidates, exact rescore picks the top-k — measured on the full 3.68M index with the same n=3000 protocol as the headline, it is recall-lossless (R@1 0.6143 vs 0.6140 fp16, R@10 equal at 0.8323; int8 mode: R@1 0.6147, 15 GB) at 2.4 s/query on 4 CPU threads. Honest caveat: this shrinks the document side only — queries must still be embedded by the same Qwen3-Embedding-8B (a small 0.6B encoder lives in a different vector space). The true end-to-end small-encoder tier is the 0.6B tier below. Numbers, build command, and the caveat in full: docs/QUANTIZED_TIER.md.

0.6B end-to-end laptop tier (opt-in). The SAME 3,683,428-doc corpus re-embedded once with Qwen3-Embedding-0.6B (1024-d, row-aligned with the served meta), so the query encoder itself runs on a laptop CPU: MATHLAS_ENCODER=0.6b (composes with MATHLAS_QUANTIZED=binary). Measured with the identical n=3000 cross-representation protocol, queries re-encoded by the 0.6B model: R@1 0.545 / R@10 0.745 (binary + int8 rescore; the 0.6B fp16 exact scan is 0.544 / 0.745, so quantization is again lossless within the tier). The honest price vs the 8B tier (0.614 / 0.832) is about 7-9pp recall; the dual-channel 8B configuration (0.965 / 0.999) stays the big-box quality ceiling. The laptop headline: end-to-end 0.67 s/query on 4 CPU threads (0.88 s on 2), query encoding included, over all 3.68M documents. Dense-channel footprint: binary sidecar 0.47 GB + 0.6B encoder ~1.2 GB (~1.7 GB; int8 rescore source 3.77 GB recommended; full fp16 sibling index 7.54 GB). On the TheoremSearch-110 corpus-only probe the tier scores Hit@20 8.2% / 10.0% theorem/paper vs the 8B tier's 10.0% / 11.8% (both licensing-bounded floors). Full tables, footprints, and caveats: docs/QUANTIZED_TIER.md; build: scripts/build_06b_index.py; eval: scripts/eval_06b_tier.py.

Dual-channel retrieval (opt-in). The 0.614 headline is a cross-representation gap: LaTeX-statement-shaped queries searched against slogan-embedded docs. A second dense channel embeds the same 3,683,428 docs by their cleaned LaTeX statement (Qwen3-Embedding-8B, row-aligned, built by scripts/build_statement_channel.py) and folds into the dense ranking by per-doc max-sim. Measured on the same n=3000 sample at full corpus scale: R@1 0.614 to 0.965, R@10 0.832 to 0.999. Honest caveats: that eval is a self-retrieval proxy in which the statement channel indexes the very text the queries are drawn from (an exact-text advantage, like BM25's); on the no-leak 110 human-query benchmark the lift is real but partial (paper Hit@20 11.8% to 12.7%). And the second matrix roughly doubles serving RAM (measured at full scale: 150 GB process peak for the dual server vs ~95 GB single-channel; ~2.75 s/query dual dense scan on 2 CPU threads), so it ships strictly opt-in (MATHLAS_STATEMENT_INDEX=/path/index_full_statement.npz, never auto-detected) and is not combinable with the quantized tier. Full numbers and the serving-tier table: docs/RETRIEVAL_UPGRADE_NOTES.md. The production hybrid default rrf_k is 10 (measured best at every k tested), plus an opt-in cross-encoder rerank blend (MATHLAS_RERANK=1, Qwen3-Reranker-0.6B, +1.7pp R@1 honest lift). The rerank backend is selectable with MATHLAS_RERANK_MODEL: qwen3 (default, Qwen3-Reranker-0.6B, unchanged) or jina-v3 (jinaai/jina-reranker-v3, arXiv:2509.25085 — a 0.6B "last but not late" reranker that leads BEIR at the 0.6B scale). Both lazy-load their weights on first use and fall back to the un-reranked fusion (honest stderr note) if torch/transformers or the weights are absent; a typo'd model name raises rather than silently serving the wrong reranker. We ship the wiring, not a jina benchmark number — bring your own weights.

The self-augmenting loop — beating TheoremSearch

On TheoremSearch's own 110 human-written queries, baseline mathlas hits a coverage floor — TheoremSearch withheld 85% of their private 9.2M corpus, so 95 target papers are unreachable for any open system. The AI then runs the loop: for each missing theorem it web-finds the real statement, embeds it with the same Qwen3-Embedding-8B, and add_finding(dense_vec=…) fuses it through the dense channel at runtime (re-measured 2026-06-10 on the served 3.68M index — the after-loop headline reproduced exactly; the corpus-only baseline dipped 13.6% → 11.8% paper-level from the added Dolma distractors, reported as is):

Method

theorem Hit@20

paper Hit@20

Google (site:arxiv.org)

—

37.8%

ChatGPT 5.2 w/ Search

19.8%

—

Gemini 3 Pro

27.0%

—

TheoremSearch (Qwen3-8B, full private 9.2M)

45.0%

56.8%

mathlas — baseline (corpus-only)

10.0%

11.8%

mathlas — after self-augmenting web loop

59.1% (65/110)

70.0% (77/110)

Reproduce with benchmarks/webaug_110_bench.py (use the full 82-finding worklist _findings_worklist_full.json).

Source-aware retrieval (opt-in). Growing the index 1.34M → 3.68M had a measured cost: the 2.34M web-mined Dolma docs crowd canonical papers out of the top-20 (corpus-only paper-level 13.6% → 11.8% on these same 110 queries). search_existing_math now takes optional source_filter / source_weights — e.g. source_filter={"exclude": ["dolma"]} when you want canonical theorem statements only — and excluding dolma fully recovers the pre-growth 13.6% paper-level (15/110; reachable-15 paper 15/15 = 100%) with theorem-level above the old index (11.8% vs 10.9%). The default ranking stays byte-identical (test-pinned). It is a per-query-intent knob, not a free win: on the n=3000 self-recall, 65% of whose targets ARE Dolma docs, down-weighting dolma is catastrophic for those queries (dolma-target R@10 0.999 → 0.884 at weight 0.5, → 0 when excluded) — exactly why it ships opt-in, default off. We also tested whether the dual channel fixes this regression structurally, without the knob: it recovers part of it (paper 11.8% to 12.7%, theorem 10.0% to 10.9% at default settings) but not the full 13.6%, so the knob remains the documented mitigation on this benchmark. Full matrix: docs/02_eval_vs_theoremsearch.md.

The 12 tools

search_existing_math ─▶ mapping_scaffold + applicability_checklist ─▶ (AI judges) ─▶ verify_numeric / verify_formal
   (own index)            (needs↔guarantees, no LLM)                                  (airtight)

Core four — what most agents use:

Tool

What it does

search_existing_math(query, k)

query → ranked results from the 3.68M-doc dense + BM25 + RRF index

identify_constant(value)

a real value → known closed form + provenance (50-digit re-eval)

verify_numeric(value, closed_form)

digit-agreement verdict — different engine, higher precision

verify_formal(statement, lean?, proof?)

runs the real Lean kernel — typecheck a snippet, or pass proof to kernel-check a full Lean 4 proof: VERIFIED_PROOF / REFUTED (the kernel's exact error, for the repair loop) / honest UNDETERMINED

Full toolkit:

Tool

What it does

search_formal_math(query, backend)

mathlib declaration names + types via the public Loogle (pattern/type) + LeanSearch (natural language) services, provenance-labeled; honest "service unavailable" — with a 7-day on-disk cache that serves the last good response when a service is down, clearly labeled (cached, <age> old)

identify_sequence(terms)

integer sequence → matching OEIS entries (exact term-match)

applicability_checklist(statement)

result's hypotheses as an atomic checklist for the AI to mark

mapping_scaffold(problem, statement)

needs↔guarantees questions + fill-in template

conjecture_relation(value)

Ramanujan Machine: PSLQ over rich basis + CF/recurrence conjectures

funsearch(action, problem_id, …)

FunSearch harness in one tool — action=evaluate (sandbox-score an AI-written program), register (MAP-Elites DB), status (best + few-shot)

search_directive(problem)

web-search plan: arXiv queries + sub-fields + which tools to run

add_finding(statement, slogan, source)

ingest a web-found result into the live corpus

All tools return data. No tool calls an LLM. search_formal_math is the one tool that itself makes a web call (to the public Loogle/LeanSearch services); everything else is fully local.

Proof checking — the repair loop

verify_formal doesn't just typecheck statements: give it a proposition and your Lean 4 proof, and the real kernel checks the full declaration. mathlas never writes a proof (the generator/verifier split is absolute) — but when your proof is wrong, the kernel tells you exactly why, verbatim, in kernel_error. That turns proof writing into a tight loop: the agent writes a proof → mathlas's kernel says exactly what's wrong → the agent repairs and re-calls.

verify_formal(statement="∀ n : Nat, n + 0 = n", proof="by\n  intro n\n  rfl")
// → {"proof_status": "VERIFIED_PROOF", "checked": true, ...}
verify_formal(statement="2 + 2 = 5", proof="rfl")
// → {"proof_status": "REFUTED", "kernel_error": "error: Not a definitional equality:
//     the left-hand side 2 + 2 is not definitionally equal to the right-hand side 5 ...", ...}

No fake passes, by construction: sorry/admit holes are REJECTED (Lean itself exits 0 on a sorried proof — mathlas scans the source and the kernel's sorryAx diagnostics); a missing toolchain, a timeout (60 s cap), or an import this bare toolchain can't resolve all return an honest UNDETERMINED, never a verdict. The whole contract is pinned by tests/test_proof_check.py (20 tests against the real Lean 4.31.0 kernel: correct term and tactic-block proofs verified, wrong proofs refuted with the kernel's message, sorried proofs rejected, toolchain-absent honest).

CLI / Python

mathlas 1.6449340668482264364724151666460251892   # -> pi**2/6  [verified 51 digits]
mathlas 1,1,2,3,5,8,13,21                          # -> A000045 Fibonacci  https://oeis.org/A000045
mathlas "a bounded sequence has a convergent subsequence" --k 5   # search + scaffold
mathlas mcp                                                        # run the MCP server
import mpmath
from mathlas import identify, identify_sequence, mapping_scaffold, applicability_checklist
print(identify(mpmath.zeta(2)))            # -> pi**2/6 [verified 51 digits]
print(identify_sequence([1,1,2,3,5,8,13,21]).matches[1].a_number)  # -> 'A000045'

Docs

Positioning — retrieval is table stakes; verification is the moat

Credit where due: the closest system, TheoremSearch (UW Math AI Lab), now ships a production REST API and its own MCP endpoint (api.theoremsearch.com/mcp) over a 9.2M-document corpus — on raw recall over math literature it is the system to beat, and "we're MCP-native, they're a lab tool" is no longer a differentiator. We reuse only their openly-licensed (CC-BY/CC0) dataset subset as raw data for our own index — not their API, MCP, index, or code.

The DeepMind signal, and why an open verifier still matters. DeepMind's AlphaProof Nexus (arXiv:2605.22763) validates precisely mathlas's architecture — an LLM agent orchestrating a Lean kernel and structured math resources like OEIS as the ground-truth oracle — but it is internal-only: the public artifact is a results dump (google-deepmind/alphaproof-nexus-results), not a runnable system, with no API and no MCP surface. Gemini Deep Think and its peers only sharpen the need: as agents reason harder, an agent-side local, deterministic verifier it can call cheaply and offline becomes the bottleneck, not the model. mathlas remains the only open, no-API-key, MCP-composable verification layer any agent can drop in today — and it now also ingests DeepMind's own openly-licensed formal-conjectures Lean corpus (arXiv:2605.13171) as an index source (scripts/fetch_formal_conjectures.py, 3,941 Lean conjecture statements, source tag formal_conjectures, including the frozen FC100SolvedSet1/FC100OpenSet1 eval subsets).

Naming note: mathlas is unrelated to Matlas (matlas.ai, Peking University theorem search, arXiv:2604.17484) — different project, different authors; the near-homophone is coincidental.

What no competitor has is everything that happens after retrieval:

  • Verification tiers — verify_numeric (independent 50-digit re-evaluation) and verify_formal (a real Lean kernel typecheck — including full proof checking with the kernel's error returned verbatim for agent repair loops — or an honest UNDETERMINED). Retrieval hands you a candidate; mathlas can also check the claim and check your proof of it.

  • applicability_checklist — decomposes a candidate theorem into atomic preconditions the AI verifies one by one, catching misapplications (open vs closed interval, infinite vs finite group). No competitor has one.

  • The self-augmenting add_finding loop — the AI web-finds a missing statement, embeds it, and fuses it into the live index at runtime: 59.1% vs TheoremSearch's 45.0% theorem Hit@20 on their own 110-query benchmark (see above). This is, to our knowledge, the first math-domain instantiation of a validated-writeback RAG loop — the family of bidirectional retrieval systems that write verified inference back into the retrievable store (Bidirectional RAG, arXiv:2512.22199), rather than treating retrieval as read-only (Self-RAG, arXiv:2310.11511; CRAG, arXiv:2401.15884). What makes the math domain the right place for it: the write-back candidate can be deterministically checked (verify_numeric / verify_formal) before it is trusted, so the loop grows the corpus without the hallucination-amplification risk a generic writeback loop carries.

  • Zero-false-positive discipline — every tier returns an independently-checkable fact or an honest "nothing"; measured false-positive rate is 0 across all tiers (RESULTS.md).

  • Free, no API key, provenance-labeled — every result carries where it came from (known_constant, conjectured_relation, web_added, external:loogle, …), and the index is built 100% from openly-licensed data.

mathlas

TheoremSearch

LeanSearch / Loogle

Wolfram MCP

sympy-mcp

Informal math retrieval

✅ 3.68M docs, open

✅ 9.2M docs (~85% private)

❌ (mathlib decls only)

❌

❌

Formal (mathlib) search

✅ proxies both → one MCP tool

❌

✅ (is exactly this)

❌

❌

Numeric verification

✅ airtight 50-digit re-eval

❌

❌

⚠️ CAS eval

⚠️ CAS (no claim-check framing)

Formal verification

✅ real Lean kernel (statements and full proofs, repair-loop errors)

❌

❌ (search, not check)

❌

❌

Applicability checklist

✅ unique

❌

❌

❌

❌

Self-augmenting corpus

✅ add_finding (59.1 vs 45.0 Hit@20)

❌

❌

❌

❌

Constant/sequence ID

✅ PSLQ + OEIS + Ramanujan-Machine

❌

❌

⚠️ some

❌

Provenance labels

✅ every result

❌

n/a

❌

n/a

Cost / key

free, no key

free endpoint

free

paid Wolfram API key

free

MCP

✅ stdio, uvx one-liner

✅ remote endpoint

❌ (mathlas proxies them)

✅

✅

(sympy-mcp is a fine CAS-manipulation server — its scope barely overlaps: it rewrites expressions you give it; mathlas finds, scopes, and verifies existing math.)

Official MCP registry

mathlas is published as io.github.Archerkattri/mathlas (see docs/REGISTRY_PUBLISH.md and server.json).

mcp-name: io.github.Archerkattri/mathlas

Available Tools

12 tools
add_findingAdd web finding to live corpusA

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.

ParametersJSON Schema
NameRequiredDescriptionDefault
nameNooptional name/title of the result
sloganYesa short natural-language denotation of it (what it says)
sourceYeswhere it came from: a URL / arXiv id / citation
dense_vecNoOPTIONAL dense embedding of the slogan, computed BY YOU (the AI) with the SAME model the served index uses, length == the served index dim. Storing it gives the finding full dense+BM25 retrieval (found even when wording differs from the query). NO model is loaded by mathlas. Omit for BM25-only.
statementYesthe web-found result's statement (the real text)

Output Schema

ParametersJSON Schema
NameRequiredDescription
okYes
nameNo
noteYeson failure (e.g. dense_vec dim mismatch) says exactly what to fix; the finding is NOT added
sloganNo
sourceNo
statementNo
n_findingsNo
provenanceNo
dense_addedNo

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

The description discloses important behavioral traits beyond annotations: it mentions provenance 'web_added', that BM25 is always used, that dense retrieval is optional if dense_vec is provided, and that no model is loaded by mathlas. This adds value beyond the annotations which only give readOnlyHint, destructiveHint, etc.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is relatively concise, fitting the purpose and usage into one sentence. It is front-loaded with the main purpose. However, the technical details about dense_vec and BM25 could be slightly more structured, but overall it is efficient.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's complexity (5 parameters, 3 required, optional dense_vec, and outcome of immediate searchability), the description covers all essential aspects: purpose, when to use, parameter meanings, and behavioral consequences. The output schema presumably documents the return value, so the description is complete.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters5/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%. The description adds meaning beyond the schema by clarifying each parameter: 'statement (the real text)', 'slogan (short natural-language denotation)', 'source (URL/arXiv/citation)', and explains dense_vec in detail (must match model, omit for BM25-only). This compensates fully for any ambiguity.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool's purpose: 'Ingest a web-found result into the live mathlas corpus so search_existing_math returns it immediately'. It specifies the verb (ingest), resource (live corpus), and the effect (immediate searchability). This makes it distinct from sibling tools, which focus on searching or other operations.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly guides usage: 'Use after web-searching per search_directive.' This provides clear context for when to invoke the tool. It doesn't explicitly list when not to use, but the context implies it is for web-found results, and sibling tools cover other scenarios.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

applicability_checklistApplicability checklistA
Read-onlyIdempotent

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).

ParametersJSON Schema
NameRequiredDescriptionDefault
candidate_statementYesthe candidate result's statement

Output Schema

ParametersJSON Schema
NameRequiredDescription
noteNo
statementNo
conclusionYes
instructionsNo
preconditionsYes

TDQS

A4.2/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint=true and idempotentHint=true, so the tool is safe and idempotent. The description adds that the tool decomposes statements into preconditions and conclusion for the agent to verify, disclosing that the tool outputs a checklist rather than performing verification itself.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two sentences with no extraneous information. The core action is front-loaded, followed by a concise usage instruction. Every sentence serves a clear purpose.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given that an output schema exists, the description does not need to explain return values. It covers purpose, usage context, and parameter semantics adequately for a simple tool with one parameter.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, and the description reiterates the parameter's meaning as 'the candidate result's statement text', adding no extra semantic context beyond what the schema already provides. Baseline of 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the verb 'Decompose' and the resource 'candidate theorem's statement into atomic preconditions + conclusion'. It distinguishes the tool from siblings by specifying its role in checking applicability after search, before relying on a candidate, which sets it apart from search and verification tools.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly says 'Use after search, before relying on any candidate,' providing clear when-to-use guidance. It does not explicitly mention alternatives or when not to use, but the context is sufficiently clear for an agent to select this tool appropriately.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

conjecture_relationConjecture relations (Ramanujan Machine)A
Read-onlyIdempotent

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).

ParametersJSON Schema
NameRequiredDescriptionDefault
valueYesthe real constant as a decimal string (give MANY digits; PSLQ/CF search needs >16)
cf_depthNocontinued-fraction evaluation depth (default 200)
max_termsNomax PSLQ basis vector length (default 16; cost grows fast)

Output Schema

ParametersJSON Schema
NameRequiredDescription
noteNo
foundYes
queryNo
integer_relationsYes
continued_fractionsYes
simple_continued_fractionNo

TDQS

A4.6/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations indicate readOnly and idempotent; description adds algorithms used (PSLQ, CF), verification threshold (>=25 digits), and provenance status (conjectured). No contradictions.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two efficient sentences, front-loaded with action and key information. Every sentence adds value without redundancy.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Covers purpose, usage condition, algorithm, verification state, and parameter hints. Could mention potential for no results or runtime cost, but overall sufficient given output schema exists.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100% but description adds useful context: 'MANY digits', 'cost grows fast' for max_terms, default values. Enhances understanding beyond schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Clearly states the tool's purpose: finding conjectured relations via PSLQ and continued-fraction methods, with numerical verification but not proof. Usage condition 'when identify_constant returns UNIDENTIFIED' distinguishes it from sibling identify_constant.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly states when to use: after identify_constant returns UNIDENTIFIED. Does not explicitly mention when not to use or alternatives, but context implies other sibling tools for different tasks.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

funsearchFunSearch harness (evaluate/register/status)A

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).

ParametersJSON Schema
NameRequiredDescriptionDefault
scoreNo(register) the score that action='evaluate' returned
top_kNo(status) elite programs in the few-shot (default 3)
actionYes'evaluate' = sandbox-score program_src; 'register' = store a scored program; 'status' = best programs + few-shot context
behaviorNo(register) the behaviour descriptor from action='evaluate' (selects the MAP-Elites cell)
timeout_sNo(evaluate) hard wall-clock timeout seconds (default 10)
problem_idYesthe problem: 'cap_set' or 'online_bin_packing'
program_srcNo(evaluate/register) the candidate Python program source — YOU write it; it must define the problem's entry point

Output Schema

ParametersJSON Schema
NameRequiredDescription
okNo(evaluate) program ran + scored
noteNo
errorNoagent-actionable: what failed and which args to fix
scoreNo
actionNo
acceptedNo(register)
behaviorNo
best_scoreNo(status)
problem_idYes
best_programNo(status)
few_shot_contextNo(status) DATA for you to write the next program

TDQS

A4.3/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations are neutral (no readOnly/destructive/idempotent hints). Description adds behavioral context: sandbox (no-network, timeout, rlimit), MAP-Elites DB storage, few-shot context retrieval. This goes beyond structured fields.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Description is 4 sentences, well-structured, front-loaded with purpose. Could be slightly more concise but effectively communicates key workflow.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given complexity (7 params, 3 actions) and presence of output schema (not shown), description covers core workflow and returns. Might miss edge cases (e.g., error handling on invalid program_src), but sufficient for iterative evolution use case.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, but description adds action-specific context (e.g., 'program_src — YOU write it', 'behavior — selects MAP-Elites cell'). Clarifies conditional parameters per action.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Description clearly states tool is a sandboxed program-search harness with three explicit actions (evaluate, register, status) and problem IDs. Distinct from sibling tools like verify_formal or search_directive.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Provides guidance 'Use to iteratively evolve programs — YOU are the generator, mathlas is the deterministic scorer.' Implicitly suggests when to use (evolution loop) and mentions sandbox constraints, but doesn't explicitly list when not to use or compare to siblings.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

identify_constantIdentify constant (closed form)A
Read-onlyIdempotent

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']).

ParametersJSON Schema
NameRequiredDescriptionDefault
basisNooptional constant basis, e.g. ["pi","e","catalan"]
valueYesthe real value as a decimal string (give many digits, >16)

Output Schema

ParametersJSON Schema
NameRequiredDescription
bestYesbest verified candidate {expr, display, digits_agreed, provenance}, or null if honest UNIDENTIFIED
noteNo
basisNo
queryYes
candidatesYes
identifiedYes
unidentified_reasonNo

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already indicate readOnly and idempotent. Description adds valuable behavioral details: PSLQ algorithm, 50+ digit reevaluation, honest UNIDENTIFIED output. No contradictions.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Single paragraph, front-loaded with purpose, then method, usage, and parameter hints. Every sentence adds value with no redundancy.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given 2 params, 100% schema coverage, and detailed annotation, the description fully covers inputs, process, and output behavior (closed form or UNIDENTIFIED).

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100% (baseline 3). Description adds extra guidance: 'give many digits, >16' for value, and example constant names for basis, enhancing usability beyond schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Explicitly states 'Identify a real number's closed form', with method details (PSLQ, closed-form search) and honesty condition. Clearly distinguishes from sibling 'identify_sequence' and other tools.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Provides explicit when-to-use: 'Use when you have a numeric constant and want to know what it IS.' Does not explicitly state when not to use or mention alternatives, but context is clear enough.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

identify_sequenceIdentify integer sequence (OEIS)A
Read-onlyIdempotent

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).

ParametersJSON Schema
NameRequiredDescriptionDefault
termsYesthe integer sequence to identify, e.g. [1,1,2,3,5,8,13,21] (give >= 4 terms)
max_resultsNomax OEIS matches to return (default 5)

Output Schema

ParametersJSON Schema
NameRequiredDescription
noteNo
queryYes
matchesYes
data_dirNo
identifiedYes
remediationNopresent iff local OEIS data is missing — how to get it

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Description adds behaviors beyond annotations: exact match, no fuzzy scoring, and honest UNDETERMINED if data absent. Annotations already indicate read-only and idempotent, which description aligns with.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two concise sentences: first states core behavior and constraints, second gives usage guidance and parameter summary. No redundant information.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the presence of an output schema, the description adequately covers purpose, usage, behavior, and parameter hints. It is complete for the tool's complexity.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, but description adds the key constraint that terms should have >=4 integers and mentions default for max_results, providing extra context beyond the schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool matches an integer sequence against a local OEIS copy using exact contiguous term-match. It distinguishes from sibling 'identify_constant' by focusing on sequences, and includes specific verbs and resources.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly states when to use: when having >=4 integer terms wanting the named sequence. The condition of data file absence leading to UNDETERMINED is mentioned. Does not explicitly exclude alternatives, but the context is clear.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

mapping_scaffoldNeeds-guarantees mapping scaffoldA
Read-onlyIdempotent

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.

ParametersJSON Schema
NameRequiredDescriptionDefault
problemYesthe problem to solve
candidate_statementYesa candidate existing result's statement

Output Schema

ParametersJSON Schema
NameRequiredDescription
noteNo
problemNo
checklistNo
questionsYes
signatureNo
answer_templateYes
candidate_statementNo

TDQS

A4.3/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations indicate readOnlyHint and idempotentHint, which the description does not contradict. The description adds context that the tool builds a scaffold and does not make judgments, complementing the annotations without repeating them.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two concise sentences with no wasted words. The first sentence states the purpose; the second gives usage guidance. Well-structured and front-loaded.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool has an output schema, the description appropriately explains the output as 'structured questions + fill-in template.' It covers usage context and parameter roles, providing sufficient completeness for a two-parameter tool.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100% with clear descriptions for both parameters. The description mentions the parameter names in context but adds minimal new meaning beyond what the schema already provides, so baseline 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool builds a 'needs<->guarantees scaffold' with structured questions and a fill-in template. The verb 'build' and specific resource distinguish it from siblings like applicability_checklist and search tools.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly says 'Use when applicability is non-obvious' and clarifies the judging is done by the user. It provides clear context but does not explicitly mention when not to use or suggest alternatives, though the sibling list helps differentiate.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

search_directiveWeb-search directive (plan only)A
Read-onlyIdempotent

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).

ParametersJSON Schema
NameRequiredDescriptionDefault
problemYesa problem / result description to build a web-search plan for

Output Schema

ParametersJSON Schema
NameRequiredDescription
noteNo
problemNo
signatureNo
subfieldsNo
instructionsYes
arxiv_queriesYes
named_resultsNo
arxiv_categoriesNo
also_try_mathlas_toolsNo

TDQS

A4.2/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint and idempotentHint. The description adds important behavioral traits: it produces a plan only, no web call is made, and the user must perform the search and feed results back via add_finding. This is valuable context beyond annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two sentences: first provides the core functionality and output structure; second gives usage guidance. No redundant words, front-loaded, every sentence earns its place.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the existence of an output schema (not shown but present), the description adequately covers the tool's process, constraints (no web call), and integration with other tools (add_finding). Complete for a planning tool, though some might want more detail on output interpretation.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Only one parameter 'problem' with schema description already present. The description adds minimal extra meaning ('Args: problem (description)'), which doesn't significantly enhance understanding beyond the schema. Schema coverage is 100%, so baseline 3 is appropriate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states it provides a structured web-search plan, listing specific components (arXiv query strings, sub-fields, named results, other tools). It distinguishes itself by noting mathlas makes no web call and directs the user to use add_finding, differentiating it from sibling tools.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

States 'Use when the local index missed' which is a clear context for use. Does not explicitly list when not to use or alternatives beyond that, but the context is clear enough. Could be more explicit about exclusions.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

search_existing_mathSearch existing math (mathlas index)A
Read-onlyIdempotent

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.

ParametersJSON Schema
NameRequiredDescriptionDefault
kNonumber of candidates (default 10)
queryYesa problem / result description
corpus_dirNooptional dir of open theorem dataset parquets; omit to use the served index / built-in seed corpus
source_filterNooptional hard include/exclude of corpus sources, e.g. {"exclude": ["dolma"]} to drop web-mined docs when looking for canonical theorem statements. Keys: 'include' and/or 'exclude', values = lists drawn from arxiv / dolma / stacks / proofwiki / other. Default off (no behaviour change).
source_weightsNooptional per-source score down-weighting, e.g. {"dolma": 0.5} to soft-demote web-mined docs (weight 0 = exclude). Source keys as in source_filter; weights >= 0 multiply the fused RRF score. Default off (no behaviour change). Note: down-weighting a source hurts queries whose true target IS that source — a per-query-intent knob, not a global default.

Output Schema

ParametersJSON Schema
NameRequiredDescription
kNo
nextNo
noteNo
queryYes
corpusNowhat was actually served
candidatesYes
live_findings_mergedNo

TDQS

A4.6/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations declare readOnlyHint and idempotentHint, which align with the description. The description adds value beyond annotations by detailing the index fusion method, optional corpus_dir behavior, and the effect of source_filter/source_weights (e.g., down-weighting hurts queries targeting that source). No contradictions.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is concise (5 sentences) and efficiently structured: core purpose first, then usage guidance, then parameter explanations with examples. No redundant or irrelevant information.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the complexity (5 parameters, nested objects, output schema exists), the description covers all necessary aspects: index composition, usage pattern, parameter nuances, and follow-up tool. Output schema is present so return values need not be described.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters5/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, and the description adds significant context: explains omit for corpus_dir uses prebuilt index, provides example for source_filter, and notes important behavior about source_weights. This adds meaningful meaning beyond the schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states it finds existing theorems/results from the mathlas index, specifying the index composition (dense + BM25 + RRF, fused with web_added findings). It distinguishes itself from the sibling applicability_checklist by advising to use this tool first for 'does known math solve this?' and then follow up with applicability_checklist.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly tells when to use: 'Use FIRST for any does known math solve this? question.' It also provides follow-up guidance (applicability_checklist). While it doesn't explicitly state when not to use, it implies the primary use case clearly.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

search_formal_mathSearch formal math (Loogle/LeanSearch)A
Read-onlyIdempotent

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').

ParametersJSON Schema
NameRequiredDescriptionDefault
kNomax merged hits (default 10)
queryYesnatural language (leansearch) or a Loogle pattern/type query
backendNo'loogle' = pattern/type, 'leansearch' = natural language, 'auto' = both (default)

Output Schema

ParametersJSON Schema
NameRequiredDescription
hitsYes
noteNo
queryYes
backendNo
backendsNoper-service block {available, hits, error, cached?, cache_age_seconds?} — cached=true means the live service failed and these hits are the last successful response (clearly labeled)

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint, idempotentHint, openWorldHint. Description adds honest 'service unavailable' behavior and cached response labeling with age, providing rich behavioral context beyond annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Compact description with no wasted words. Front-loads purpose, covers caching, usage context, and parameter details efficiently.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a tool with 3 parameters and an output schema, the description is comprehensive: explains caching, service availability, usage scenario, and all parameters. No gaps.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, baseline 3. Description adds value by giving example patterns for query, default for k, and explanations for backend options, exceeding schema info.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states it finds mathlib declarations via Loogle/LeanSearch, specifying query types and services. It distinguishes itself from siblings as the 'ONE tool that itself calls the web', setting it apart clearly.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly states when to use: 'when you need the formal Lean name/type of a result, e.g. before writing a verify_formal snippet'. Provides backend guidance but does not explicitly state when not to use it.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

verify_formalVerify formal (real Lean kernel)A
Read-onlyIdempotent

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?.

ParametersJSON Schema
NameRequiredDescriptionDefault
leanNoLean 4 snippet to kernel-check as-is, e.g. "example : 2 + 2 = 4 := rfl" (omit both this and `proof` and the verdict is an honest UNDETERMINED — statement text alone is not checkable)
proofNoYOUR Lean 4 proof of `statement` — a term ('rfl') or tactic block ('by\n intro n\n rfl'). Checked by the real kernel; on REFUTED, repair using `kernel_error` and re-call. sorry/admit holes are rejected.
statementYesthe claim being checked; with `proof` it MUST be the Lean 4 proposition to prove, e.g. '∀ n : Nat, n + 0 = n'

Output Schema

ParametersJSON Schema
NameRequiredDescription
modeNo'proof_check' iff `proof` was supplied
noteNo
tierNo
detailNo
appliesNo
checkedYestrue iff the Lean kernel actually ran and gave a verdict
statementNo
typechecksYes
declarationNoproof mode only — the exact declaration the kernel checked
remediationNopresent iff not checked — exactly what unblocks a real kernel check
kernel_errorNoproof mode, REFUTED only — the kernel's error verbatim; the repair-loop payload
proof_statusNoproof mode only — the kernel's verdict on YOUR proof
lean_providedNo
lean_availableYes
proof_providedNo

TDQS

A4.6/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Disclosures beyond annotations: states 'REAL Lean 4 kernel (NO LLM)', rejects 'sorry'/'admit', promises honest results (never fake), lists three outcome categories with meaning. Annotations (readOnlyHint, idempotentHint) are consistent and description adds significant behavioral context.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Description is front-loaded with 'Run the REAL Lean 4 kernel (NO LLM)', then clearly splits modes with examples and outcomes. Slightly long but every sentence serves a purpose; structured for quick parsing. Minor redundancy could be trimmed.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given tool complexity (two modes, multiple outcomes, constraints), description covers all aspects: parameter combinations, expected behavior, error handling, and guidance to use sibling tool. No gaps for agent invocation. Output schema presence implied but not needed due to description of outcomes.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100% with descriptions, but description adds value by explaining the two usage modes, clarifying that 'proof' must be a Lean 4 proof of 'statement', and noting that omitting both 'lean' and 'proof' results in UNDETERMINED. Adds context not in schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Description clearly states it runs the real Lean 4 kernel, distinguishes two modes (typecheck and proof-check), and emphasizes it never writes proofs. Specific verbs like 'typecheck', 'proof-check', and 'returns proof_status' make purpose unambiguous. Differentiates from sibling verify_numeric.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly describes when to use each mode: pass 'lean' for typechecking, pass 'proof' for proof-checking. Advises to find declaration names first with search_formal_math. Explains how to handle REFUTED outcome. Does not explicitly exclude cases like using for numeric verification, but context implies alternatives.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

verify_numericVerify numeric claim (airtight)A
Read-onlyIdempotent

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)').

ParametersJSON Schema
NameRequiredDescriptionDefault
valueYesthe value as a decimal string
closed_formYesa closed-form expression, e.g. "pi**2/6" or "zeta(3)"

Output Schema

ParametersJSON Schema
NameRequiredDescription
noteNo
errorNo
valueNo
reevalNo
verifiedYes
closed_formNo
digits_agreedYes
min_digits_requiredNo

TDQS

A4.7/5.0
Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already indicate readOnly and idempotent. The description adds key behavioral details: independent sympy re-evaluation, higher precision, 20-digit threshold, and 'airtight' nature. No contradiction.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two concise sentences plus an Args line, all front-loaded. No redundancy, every sentence adds value.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Output schema exists, so return values need no explanation. Description covers purpose, method, prerequisites, and usage context. Complete for a numeric verification tool.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100% with descriptions for both parameters. The description adds examples for closed_form and clarifies value as decimal string, enhancing understanding beyond schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the verb 'verify' and the resource 'numeric claim', with precise method (sympy re-evaluation, >=20 digits). It distinguishes from siblings like 'verify_formal' and 'identify_constant' by focusing on numeric identity.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly says 'Use BEFORE asserting any numeric identity', providing clear when-to-use guidance. However, no mention of when not to use or alternatives, but the context is sufficient.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections. Dates show when Glama detected each change.

  1. 3 tool updatesv1.2.0
    • Changedsearch_existing_math2 fields changed
      • addedInput schema / properties / source_filter
        Added value: +{
+  "description": "optional hard include/exclude of corpus sources, e.g. {\"exclude\": [\"dolma\"]} to drop web-mined docs when looking for canonical theorem statements. Keys: 'include' and/or 'exclude', values = lists drawn from arxiv / dolma / stacks / proofwiki / other. Default off (no behaviour change).",
+  "properties": {
+    "exclude": {
+      "items": {
+        "type": "string"
+      },
+      "type": "array"
+    },
+    "include": {
+      "items": {
+        "type": "string"
+      },
+      "type": "array"
+    }
+  },
+  "type": "object"
+}
      • addedInput schema / properties / source_weights
        Added value: +{
+  "additionalProperties": {
+    "type": "number"
+  },
+  "description": "optional per-source score down-weighting, e.g. {\"dolma\": 0.5} to soft-demote web-mined docs (weight 0 = exclude). Source keys as in source_filter; weights >= 0 multiply the fused RRF score. Default off (no behaviour change). Note: down-weighting a source hurts queries whose true target IS that source — a per-query-intent knob, not a global default.",
+  "type": "object"
+}
    • Changedsearch_formal_math1 field changed
      • changedOutput schema / properties / backends / description
        Previous value: -"per-service block {available, hits, error}"New value: +"per-service block {available, hits, error, cached?, cache_age_seconds?} — cached=true means the live service failed and these hits are the last successful response (clearly labeled)"
    • Changedverify_formal8 fields changed
      • changedInput schema / properties / lean / description
        Previous value: -"Lean 4 snippet to kernel-check, e.g. \"example : 2 + 2 = 4 := rfl\" (omit it and the verdict is an honest UNDETERMINED — statement text alone is not checkable)"New value: +"Lean 4 snippet to kernel-check as-is, e.g. \"example : 2 + 2 = 4 := rfl\" (omit both this and `proof` and the verdict is an honest UNDETERMINED — statement text alone is not checkable)"
      • addedInput schema / properties / proof
        Added value: +{
+  "description": "YOUR Lean 4 proof of `statement` — a term ('rfl') or tactic block ('by\\n  intro n\\n  rfl'). Checked by the real kernel; on REFUTED, repair using `kernel_error` and re-call. sorry/admit holes are rejected.",
+  "type": "string"
+}
      • changedInput schema / properties / statement / description
        Previous value: -"the claim being checked"New value: +"the claim being checked; with `proof` it MUST be the Lean 4 proposition to prove, e.g. '∀ n : Nat, n + 0 = n'"
      • addedOutput schema / properties / declaration
        Added value: +{
+  "description": "proof mode only — the exact declaration the kernel checked",
+  "type": "string"
+}
      • addedOutput schema / properties / kernel_error
        Added value: +{
+  "description": "proof mode, REFUTED only — the kernel's error verbatim; the repair-loop payload",
+  "type": [
+    "string",
+    "null"
+  ]
+}
      • addedOutput schema / properties / mode
        Added value: +{
+  "description": "'proof_check' iff `proof` was supplied",
+  "type": "string"
+}
      • addedOutput schema / properties / proof_provided
        Added value: +{
+  "type": "boolean"
+}
      • addedOutput schema / properties / proof_status
        Added value: +{
+  "description": "proof mode only — the kernel's verdict on YOUR proof",
+  "enum": [
+    "VERIFIED_PROOF",
+    "REFUTED",
+    "UNDETERMINED"
+  ],
+  "type": "string"
+}
  2. 12 tool updatesv0.1.0
    • First observedadd_finding
    • First observedapplicability_checklist
    • First observedconjecture_relation
    • First observedfunsearch
    • First observedidentify_constant
    • First observedidentify_sequence
    • First observedmapping_scaffold
    • First observedsearch_directive
    • First observedsearch_existing_math
    • First observedsearch_formal_math
    • First observedverify_formal
    • First observedverify_numeric
Install Server
RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A4.5/5.0
Disambiguation5/5

Each tool has a distinct purpose: different types of search (existing math, formal math, web directive), identification (constants, sequences, conjectured relations), verification (formal and numeric), and support (add finding, checklist, scaffold, program search). No two tools appear to do the same thing; descriptions clarify boundaries.

Naming Consistency4/5

Most tool names follow a verb_noun pattern (e.g., add_finding, identify_constant, search_existing_math). A few deviate: applicability_checklist (adjective_noun), conjecture_relation (noun_noun), funsearch (blend), and mapping_scaffold (gerund_noun). This is mostly consistent with minor exceptions that do not hinder understanding.

Tool Count5/5

With 12 tools, the server is well-scoped for a mathematical assistant. Each tool covers a necessary operation (search, identification, verification, support) without being excessive or sparse. The count feels appropriate for the domain.

Completeness5/5

The tool set covers the full workflow: searching for existing results (both natural language and formal), identifying unknowns (constants, sequences), conjecturing relations, verifying claims (formally and numerically), and applying results (checklist, scaffold). There are no obvious gaps; it provides a comprehensive surface for mathematical problem-solving.

Maintenance

ActivitySlowing
ResponsivenessSyncing

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

Related MCP Servers

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/Archerkattri/mathlas'

If you have feedback or need assistance with the MCP directory API, please join our Discord server