io.github.Archerkattri/mathlas
PYPI · MATHLAS-MCP · SCANNED SEP 20
Airtight math for AI agents: 3.68M-doc theorem search + numeric/Lean verification. No LLM, no key.
Available components
How this component scores in each security and reliability category. Every signal is checked automatically from public evidence about the published package, including repeated runs of it in an isolated sandbox, and we only credit what we can confirm. How we score → Why this is hard to score →
Supply Chain Security100
- No malware found by supply-chain analysis.Pass
- No known CVEs affecting this package version or its production dependencies.Pass
- Runs setuptools.build_meta at install time, a recognised native-build step with no shell scripting around it. View diagnostics → Pass
- 0 of 5 dependencies flagged as unhealthy. View diagnostics → Pass
Provenance & Transparency35
- Source repository is publicly reachable at the declared URL. View diagnostics → Pass
- Provenance check failed: no build-provenance attestation is published. See how to fix → View diagnostics → Fail
- License check failed: the license (Apache Software License) isn't a recognized OSI-approved license. See how to fix → Fail
- Actively maintained (last published 80 days ago).Pass
- Publishes a security disclosure policy (SECURITY.md).Pass
Schema Quality & AI Usability70
- AI-judged instruction clarity (excellent).Pass
- Context-footprint check failed: tool/resource definitions use about 2310 tokens (~192/item across 12 items; 12 tools + 0 resources), over budget; trim descriptions and params. See how to fix → Fail
- Usage-examples check failed: none of the tools include examples. See how to fix → Fail
Stability & Change Management87
- Stability observed for 26 of 30 days with no destabilising changes; credit accrues until the full window elapses.Partial
Tool Coverage100
- 100% of tools have a non-trivial description (not blank, and not just the tool's name).Pass
- 100% of tool parameters carry a description.Pass
- Structured output schemas are declared (100% of tools); any adoption earns full credit.Pass
Tool Safety100
- No prompt-injection markers were found in the server instructions, tool names or descriptions we captured.Pass
- We read all 12 captured tool definition(s), and no name or description among them implies an irreversible operation.Pass
- An AI judge read all 13 captured unit(s) of tool text and found none that tries to manipulate the model reading it.Pass
Capabilities60
- Spec-recency check failed: implements MCP spec 2025-06-18; the latest is 2026-07-28. See how to fix → Fail
How do I install the io.github.Archerkattri/mathlas MCP server?
io.github.Archerkattri/mathlas runs locally as a PyPI package, launched with uvx mathlas-mcp. Ready-made configuration for Claude, Cursor, VS Code, Codex and 5 more is on this page, copied from each client's own documentation.
pypi · mathlas-mcp
claude mcp add archerkattri-mathlas -- uvx mathlas-mcp
{
"mcpServers": {
"archerkattri-mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
} {
"servers": {
"archerkattri-mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
} codex mcp add archerkattri-mathlas -- uvx mathlas-mcp
{
"$schema": "https://opencode.ai/config.json",
"mcp": {
"archerkattri-mathlas": {
"type": "local",
"command": [
"uvx",
"mathlas-mcp"
],
"enabled": true
}
}
} openclaw mcp add archerkattri-mathlas --command uvx --arg mathlas-mcp
mcp_servers:
archerkattri-mathlas:
command: "uvx"
args: ["mathlas-mcp"] {
"McpServers": {
"archerkattri-mathlas": {
"Transport": "stdio",
"Command": "uvx",
"Arguments": [
"mathlas-mcp"
]
}
}
} assistant mcp add archerkattri-mathlas -t stdio -c uvx -a mathlas-mcp
{
"mcpServers": {
"archerkattri-mathlas": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
} Every change we have recorded for this component, newest first. Security-relevant changes are always shown. ▲ marks a change for the better, ▼ a change for the worse; unmarked changes are neutral.
- 19 Sept 26 +1
No change was recorded against any check on this day. Stability & Change Management went from 80 to 83. That category is still filling its 30-day observation window: 24 days of observed history at the previous scan, 25 at this one. The score rises as the window fills, whether or not the server changes.
- 18 Sept 26 −2
- Security disclosure: fail → pass ▲ functional
- Stability: pass → 0.80 functional
- 17 Sept 26 0
- Stability: 0.97 → pass security
- 16 Sept 26 +1
No change was recorded against any check on this day. Stability & Change Management went from 93 to 97. That category is still filling its 30-day observation window: 28 days of observed history at the previous scan, 29 at this one. The score rises as the window fills, whether or not the server changes.
- 15 Sept 26 +15
- Malware scan: unverified → pass ▲ security
- 14 Sept 26 −15
- Malware scan: pass → unverified ▼ security
- 13 Sept 26 +1
No change was recorded against any check on this day. Stability & Change Management went from 83 to 87. That category is still filling its 30-day observation window: 25 days of observed history at the previous scan, 26 at this one. The score rises as the window fills, whether or not the server changes.
- 11 Sept 26 −2
- Stability: pass → 0.80 functional
Diagnostic detail from the automated scan of this channel: what the scanner observed at each step, so you can see exactly where a check passed or failed. It is informational only and never changes the trust score.
Captured 20 Sept 2026 · Analysed pypi/mathlas-mcp@1.5.0
Provenance No attestation
The registry publishes no build provenance for this version, so there is nothing to verify.
| Result | No attestation |
|---|---|
| Ecosystem | pypi |
Background: How many MCP packages publish verified provenance →
Install scripts 1 script
| Hook | Tier | Command |
|---|---|---|
| build_backend | allowlisted | setuptools.build_meta |
Background: Why install scripts are a supply-chain risk →
Dependencies 5 packages
| Packages resolved | 5 |
|---|---|
| Tree resolution | Complete |
Background: SBOMs and build attestations, explained →
The tools this component advertises to a client, with an estimated token cost for each. Expand a tool to see its parameters and schema. The per-tool counts are indicative and are not scored directly; the schema's total context footprint is one signal in Schema Quality & AI Usability. A tool's description is untrusted text the model reads on every call, which is what makes this list a security surface and not just an inventory: how tool poisoning works →
add_finding Add web finding to live corpus ~230
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.
| Name | Type | Req | Description |
|---|---|---|---|
| dense_vec | array | – | OPTIONAL 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 (fou… |
| name | string | – | optional name/title of the result |
| slogan | string | yes | a short natural-language denotation of it (what it says) |
| source | string | yes | where it came from: a URL / arXiv id / citation |
| statement | string | yes | the web-found result's statement (the real text) |
| Name | Type | Req | Description |
|---|---|---|---|
| dense_added | boolean | – | – |
| n_findings | integer | – | – |
| name | string|null | – | – |
| note | string | yes | on failure (e.g. dense_vec dim mismatch) says exactly what to fix; the finding is NOT added |
| ok | boolean | yes | – |
| provenance | string|null | – | – |
| slogan | string|null | – | – |
| source | string|null | – | – |
| statement | string|null | – | – |
No examples provided.
applicability_checklist Applicability checklist ~83
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).
| Name | Type | Req | Description |
|---|---|---|---|
| candidate_statement | string | yes | the candidate result's statement |
| Name | Type | Req | Description |
|---|---|---|---|
| conclusion | string | yes | – |
| instructions | string | – | – |
| note | string | – | – |
| preconditions | array | yes | – |
| statement | string | – | – |
No examples provided.
conjecture_relation Conjecture relations (Ramanujan Machine) ~162
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).
| Name | Type | Req | Description |
|---|---|---|---|
| cf_depth | integer | – | continued-fraction evaluation depth (default 200) |
| max_terms | integer | – | max PSLQ basis vector length (default 16; cost grows fast) |
| value | string | yes | the real constant as a decimal string (give MANY digits; PSLQ/CF search needs >16) |
| Name | Type | Req | Description |
|---|---|---|---|
| continued_fractions | array | yes | – |
| found | boolean | yes | – |
| integer_relations | array | yes | – |
| note | string | – | – |
| query | string | – | – |
| simple_continued_fraction | object|null | – | – |
No examples provided.
funsearch FunSearch harness (evaluate/register/status) ~303
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).
| Name | Type | Req | Description |
|---|---|---|---|
| action | string | yes | 'evaluate' = sandbox-score program_src; 'register' = store a scored program; 'status' = best programs + few-shot context |
| behavior | array | – | (register) the behaviour descriptor from action='evaluate' (selects the MAP-Elites cell) |
| problem_id | string | yes | the problem: 'cap_set' or 'online_bin_packing' |
| program_src | string | – | (evaluate/register) the candidate Python program source — YOU write it; it must define the problem's entry point |
| score | number | – | (register) the score that action='evaluate' returned |
| timeout_s | number | – | (evaluate) hard wall-clock timeout seconds (default 10) |
| top_k | integer | – | (status) elite programs in the few-shot (default 3) |
| Name | Type | Req | Description |
|---|---|---|---|
| accepted | boolean | – | (register) |
| action | string | – | – |
| behavior | array | – | – |
| best_program | string|null | – | (status) |
| best_score | number|null | – | (status) |
| error | string|null | – | agent-actionable: what failed and which args to fix |
| few_shot_context | string|null | – | (status) DATA for you to write the next program |
| note | string | – | – |
| ok | boolean | – | (evaluate) program ran + scored |
| problem_id | string | yes | – |
| score | number|null | – | – |
No examples provided.
identify_constant Identify constant (closed form) ~128
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']).
| Name | Type | Req | Description |
|---|---|---|---|
| basis | array | – | optional constant basis, e.g. ["pi","e","catalan"] |
| value | string | yes | the real value as a decimal string (give many digits, >16) |
| Name | Type | Req | Description |
|---|---|---|---|
| basis | array | – | – |
| best | object|null | yes | best verified candidate {expr, display, digits_agreed, provenance}, or null if honest UNIDENTIFIED |
| candidates | array | yes | – |
| identified | boolean | yes | – |
| note | string | – | – |
| query | string | yes | – |
| unidentified_reason | string | – | – |
No examples provided.
identify_sequence Identify integer sequence (OEIS) ~128
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).
| Name | Type | Req | Description |
|---|---|---|---|
| max_results | integer | – | max OEIS matches to return (default 5) |
| terms | array | yes | the integer sequence to identify, e.g. [1,1,2,3,5,8,13,21] (give >= 4 terms) |
| Name | Type | Req | Description |
|---|---|---|---|
| data_dir | string|null | – | – |
| identified | boolean | yes | – |
| matches | array | yes | – |
| note | string | – | – |
| query | string | yes | – |
| remediation | string | – | present iff local OEIS data is missing — how to get it |
No examples provided.
mapping_scaffold Needs-guarantees mapping scaffold ~86
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.
| Name | Type | Req | Description |
|---|---|---|---|
| candidate_statement | string | yes | a candidate existing result's statement |
| problem | string | yes | the problem to solve |
| Name | Type | Req | Description |
|---|---|---|---|
| answer_template | string | yes | – |
| candidate_statement | string | – | – |
| checklist | object | – | – |
| note | string | – | – |
| problem | string | – | – |
| questions | array | yes | – |
| signature | object | – | – |
No examples provided.
search_directive Web-search directive (plan only) ~96
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).
| Name | Type | Req | Description |
|---|---|---|---|
| problem | string | yes | a problem / result description to build a web-search plan for |
| Name | Type | Req | Description |
|---|---|---|---|
| also_try_mathlas_tools | array | – | – |
| arxiv_categories | array | – | – |
| arxiv_queries | array | yes | – |
| instructions | string | yes | – |
| named_results | array | – | – |
| note | string | – | – |
| problem | string | – | – |
| signature | object | – | – |
| subfields | array | – | – |
No examples provided.
search_existing_math Search existing math (mathlas index) ~355
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.
| Name | Type | Req | Description |
|---|---|---|---|
| corpus_dir | string | – | optional dir of open theorem dataset parquets; omit to use the served index / built-in seed corpus |
| k | integer | – | number of candidates (default 10) |
| query | string | yes | a problem / result description |
| source_filter | object | – | 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 dra… |
| source_weights | object | – | 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 o… |
| Name | Type | Req | Description |
|---|---|---|---|
| candidates | array | yes | – |
| corpus | string | – | what was actually served |
| k | integer | – | – |
| live_findings_merged | integer | – | – |
| next | string | – | – |
| note | string | – | – |
| query | string | yes | – |
No examples provided.
search_formal_math Search formal math (Loogle/LeanSearch) ~205
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').
| Name | Type | Req | Description |
|---|---|---|---|
| backend | string | – | 'loogle' = pattern/type, 'leansearch' = natural language, 'auto' = both (default) |
| k | integer | – | max merged hits (default 10) |
| query | string | yes | natural language (leansearch) or a Loogle pattern/type query |
| Name | Type | Req | Description |
|---|---|---|---|
| backend | string | – | – |
| backends | object | – | 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) |
| hits | array | yes | – |
| note | string | – | – |
| query | string | yes | – |
No examples provided.
verify_formal Verify formal (real Lean kernel) ~379
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?.
| Name | Type | Req | Description |
|---|---|---|---|
| lean | string | – | 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) |
| proof | string | – | 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 reje… |
| statement | string | yes | the claim being checked; with `proof` it MUST be the Lean 4 proposition to prove, e.g. '∀ n : Nat, n + 0 = n' |
| Name | Type | Req | Description |
|---|---|---|---|
| applies | boolean|null | – | – |
| checked | boolean | yes | true iff the Lean kernel actually ran and gave a verdict |
| declaration | string | – | proof mode only — the exact declaration the kernel checked |
| detail | string | – | – |
| kernel_error | string|null | – | proof mode, REFUTED only — the kernel's error verbatim; the repair-loop payload |
| lean_available | boolean | yes | – |
| lean_provided | boolean | – | – |
| mode | string | – | 'proof_check' iff `proof` was supplied |
| note | string | – | – |
| proof_provided | boolean | – | – |
| proof_status | string | – | proof mode only — the kernel's verdict on YOUR proof |
| remediation | string | – | present iff not checked — exactly what unblocks a real kernel check |
| statement | string | – | – |
| tier | string | – | – |
| typechecks | boolean|null | yes | – |
No examples provided.
verify_numeric Verify numeric claim (airtight) ~116
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)').
| Name | Type | Req | Description |
|---|---|---|---|
| closed_form | string | yes | a closed-form expression, e.g. "pi**2/6" or "zeta(3)" |
| value | string | yes | the value as a decimal string |
| Name | Type | Req | Description |
|---|---|---|---|
| closed_form | string | – | – |
| digits_agreed | integer | yes | – |
| error | string|null | – | – |
| min_digits_required | integer | – | – |
| note | string | – | – |
| reeval | string|null | – | – |
| value | string | – | – |
| verified | boolean | yes | – |
No examples provided.
What is the io.github.Archerkattri/mathlas MCP server?
io.github.Archerkattri/mathlas is an MCP server listed in the public MCP registry as io.github.Archerkattri/mathlas. Airtight math for AI agents: 3.68M-doc theorem search + numeric/Lean verification. No LLM, no key. This page covers its PyPI package (mathlas-mcp).
Is the io.github.Archerkattri/mathlas MCP server safe to use?
io.github.Archerkattri/mathlas scores 78 out of 100 on VerifyMCP. We found no known CVEs affecting it as of 20 September 2026. That is a record of what we were able to check automatically, not an endorsement. The category breakdown on this page shows every signal behind the number, including the ones we could not confirm.
What tools does the io.github.Archerkattri/mathlas MCP server expose?
io.github.Archerkattri/mathlas exposes 12 tools: identify_constant, identify_sequence, search_existing_math, search_formal_math, verify_numeric, and 7 more. Their descriptions and schemas cost roughly 2,271 tokens of context every time the server is loaded.
Is the io.github.Archerkattri/mathlas MCP server still maintained?
io.github.Archerkattri/mathlas is still listed as active in the MCP registry. We last reached this channel on 20 September 2026. Those dates come from our own scans of the registry and the channel itself, not from anything the publisher announced.