安装
claude mcp add mathlas -- uvx mathlas-mcp适合谁
你在 Claude Code 或 Cursor 里推数学，希望模型少编造定理、常数和数列，并且不想再申请 API key。mathlas 自己不跑大模型、不要 key、免费；它提供候选、判定、清单和脚手架，推理仍由你的 AI 完成。
它适合两类具体任务：在约 368 万篇索引里用 search_existing_math 找回真实定理；或对认不出的常数做 identify_constant（PSLQ 加闭式匹配，50 位精度），对整数列做 identify_sequence（精确 OEIS 项匹配）。
官方仓库单独一行：
https://github.com/Archerkattri/mathlas
3 分钟完成第一次尝试
只走官方这一行接入，需要先有 uv。uv 文档单独一行：
https://docs.astral.sh/uv/
然后执行：
claude mcp add mathlas -- uvx mathlas-mcp
前置条件：已安装 uv。不需要 API key。官方说 nothing to install first，但仍依赖 uv。
配置位置：Claude Code 用上面这条 add；Cursor 或其他 MCP 客户端把 stdio 指到同一条 uvx mathlas-mcp。不要同时再开一条 python -m mathlas.server 作为主路径。服务优先官方 mcp SDK，若未安装则回退到无依赖的 stdio JSON-RPC，官方称它总会跑起来。
低风险第一步：调用 search_existing_math，在 3.68M 文档索引里查找已有定理。这是检索，返回数据给模型推理，不改你的仓库。成功信号是得到候选或检索结果，而不是一段新证明。一共十二个工具，本页只点名其中几个，不要编造其余名字。
不要把“无 LLM、无 API key”理解成无网络或无本地读取。uvx 会拉起本机进程，检索和验证会读本地可选数据。readOnlyHint 即使出现也不是零风险。
使用案例
案例一：先核对一条可能是幻觉的定理。调用 search_existing_math，从 3.68M 文档索引找真实定理。官方还提到 verify_numeric 与 verify_formal 用来检查断言，并称零幻觉风险；verify_formal 需要 Lean 工具链，没有时会明确返回 data/toolchain not available，不会假造答案。本页没有这些工具的参数表。
案例二：认出常数或整数列。调用 identify_constant，用 PSLQ 加闭式匹配，精度写明 50 位。或调用 identify_sequence，做精确 OEIS 项匹配。identify_sequence 需要本地 OEIS 副本，没有时同样诚实降级，返回不可用而不是假命中。官方未给出输入格式示例。
使用边界
不需要 API key，但需要 uv。十二个工具里本页只点名 search_existing_math、verify_numeric、verify_formal、identify_constant、identify_sequence。缺 Lean 或本地 OEIS 时工具会说不可用，不会编造。mathlas 只返回数据，证明仍由模型完成。可选本地数据未装时功能收缩。官方未写索引更新频率、资源占用和撤销。不要把“零幻觉风险”理解成验证工具从不访问本机。