mathlas 是一套专为 AI 设计的数学工具集，通过 MCP（Model Context Protocol）协议供 AI 调用。其核心理念是“AI 是大脑，mathlas 是双手”：mathlas 本身不包含任何 LLM，也不需要 API 密钥，而是为 AI 提供其自身缺乏的数学能力，并返回候选、判定、清单和脚手架等数据，供 AI 进行推理。
用途
mathlas 旨在解决 AI 在数学任务中容易产生幻觉的问题。它提供可独立验证的事实或诚实的“无结果”，而非编造答案。适用于以下场景：
- 使用 Claude Code 或 Cursor，希望 AI 停止在数学上产生幻觉；
- 拥有无法识别的数值常数或整数序列；
- 需要某个结果的正式（Lean/mathlib）名称；
- 构建需要在循环中嵌入可靠数学能力的智能体流水线。
主要能力
mathlas 提供 12 个纯数据返回的 MCP 工具，核心包括：
- search_existing_math：从 3,683,428 篇文档的密集索引中检索真实定理，索引由 Qwen3-Embedding-8B（4096 维）构建，包含 134 万条宽松许可的 CC-BY/CC0 TheoremSearch 子集和 234 万条来自 Dolma 的 arXiv 数学文档，采用密集检索、Okapi-BM25 和 RRF 融合。
- identify_constant：运行 PSLQ 加闭式匹配（50 位精度）识别数值常数。
- identify_sequence：进行精确的 OEIS 项匹配。
- verify_numeric 和 verify_formal：以零幻觉风险检查声明；verify_formal 使用真实的 Lean 4.31.0 内核检查完整声明，拒绝 sorry/admit 空洞，工具链缺失、超时或无法解析的导入均返回诚实的 UNDETERMINED。
- search_formal_math：代理公共 Loogle 和 LeanSearch 服务，返回声明名称和类型，并标注来源。
- add_finding：支持自增强循环，将网络找到的真实定理语句嵌入后通过密集通道在运行时融合。
所有工具均返回数据，不调用 LLM。search_formal_math 是唯一自身发起网络调用的工具（调用公共 Loogle/LeanSearch 服务），其余完全本地运行。
使用方式
安装与注册到 Claude Code（无需 API 密钥）：
uvx mathlas-mcp
首次使用时，uvx 会在隔离环境中获取并运行服务器（需要 uv）。也可使用 pip 安装。注册后，mathlas 会作为 12 个工具出现在智能体可调用的列表中。服务器优先使用官方 mcp SDK，若未安装则回退到无依赖的 stdio JSON-RPC 服务器，确保始终可运行。Cursor 或任何 MCP 客户端可指向相同的 uvx mathlas-mcp 或 python -m mathlas.server stdio 命令。
可选本地数据（诚实降级）：identify_sequence 需要本地 OEIS 副本；verify_formal 需要 Lean 工具链。缺少时工具返回明确的“数据/工具链不可用”，绝不返回虚假答案。
适用场景
- 智能体流水线中需要可靠数学能力；
- 数学定理检索与形式化验证；
- 数值常数与整数序列识别；
- 证明检查与修复循环：智能体编写证明，mathlas 内核指出具体错误，智能体修复后重新调用。
限制
- 内部不含 LLM，不生成证明（生成器/验证器分离是绝对的）；
- 部分工具依赖可选本地数据或工具链，缺失时返回 UNDETERMINED 而非判定；
- 检索索引存在跨表示召回差距，诚实头条召回率在完整 3.68M 规模下 R@1 为 0.614、R@10 为 0.832；
- 量化笔记本层级和 0.6B 端到端层级为可选功能，存在召回率损失；
- 双通道检索会显著增加服务内存，严格可选；
- 源感知检索的 source_filter/source_weights 为按查询意图调节的旋钮，默认关闭。
项目采用 Apache-2.0 许可，代码可免费用于任何用途；发布的语料库和索引产物遵循各自的来源条款（CC-BY/CC0）。
