Skip to content

v1.1.0 — formal search · reranker blend · dual-channel retrieval · 12-tool schema pass

Choose a tag to compare

View all tags
@Archerkattri Archerkattri released this 09 Jun 23:50
· 32 commits to main since this release
v1.1.0
1f15579

mathlas-mcp 1.1.0 — the verification-first release.

New

  • search_formal_math: Loogle + LeanSearch proxy returning mathlib declarations with provenance — live eval Hit@1/5/10 = 0.64/0.96/0.96 over 25 index-verified queries.
  • Qwen3-Reranker-0.6B blend (opt-in): dense R@1 0.731→0.748, R@5 0.933→0.974. (Honest finding: replacement reranking hurts — relevance ≠ row identity — so it ships as an RRF blend.)
  • Dual-channel retrieval (opt-in): per-doc max-sim over slogan + statement embeddings; 200k-slice validation R@1 0.833→0.981. Full-corpus statement channel building.
  • uvx mathlas-mcp one-liner; official-registry server.json; 12-tool surface with outputSchema/title (funsearch collapsed to one action-enum tool).

Changed

  • Index now 3,683,428 docs (1.34M + 2.34M slogan-embedded Dolma); honest cross-representation headline R@1 0.614 / R@10 0.832.
  • RRF k default 60→10 (evaluated); BM25 top-k via argpartition (9× sort speedup, deterministic ties).
  • README positioning rewritten: verification tiers + applicability checklist + the self-augmenting loop are the moat; comparison table vs TheoremSearch / LeanSearch / Wolfram MCP / sympy-mcp.

pip install -U mathlas-mcp · claude mcp add mathlas -- uvx mathlas-mcp

Assets 4
Loading