安裝
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 只回傳資料，證明仍由模型完成。可選本機資料未裝時功能收縮。官方未寫索引更新頻率、資源占用和撤銷。不要把「零幻覺風險」理解成驗證工具從不造訪本機。