integrate theoremsearch

[jeremymanning]

for math papers: theoremsearch

[jeremymanning]

Research findings: TheoremSearch vs. the llmXive librarian

Investigated theoremsearch.com for integration into the librarian agent (spec 005, merged in #110). Summary: real working service, but the wrong granularity and out of scope for the librarian — close as out-of-scope.

What it is

TheoremSearch is a semantic search engine over mathematical theorem statements (not papers) — 9.2M theorem-level records LaTeX-extracted from arXiv + 7 other sources (ProofWiki, Stacks Project, etc.). It's an academic project from the UW Math AI Lab (companion paper arXiv:2602.05216; repo uw-math-ai/TheoremSearch — 8 stars, 0 forks, no license).

Does it have an API?

Yes — POST https://api.theoremsearch.com/search (no auth, no documented rate limits), plus an MCP server at https://api.theoremsearch.com/mcp. The API is real and in production.

But the response is theorem-centric, not paper-centric. /search returns slogan_id / theorem_id / name / body / slogan / link / similarity / score plus paper-adjacent source / title / primary_category / year / citations / journal_published. Missing from /search results: authors, abstract, DOI, arXiv ID — those require a separate GET /graph?external_id=... round-trip.

Why it's a poor fit for the librarian

Concern	Detail
Granularity mismatch	The librarian works at paper level (Candidate = {primary_pointer, claimed_title, claimed_authors, claimed_year, claimed_venue, claimed_abstract}). TheoremSearch returns theorem fragments — to map to a Candidate you need 2 HTTP calls per result (/search then /graph), and primary_pointer would be a theorem-level URL, not a verifiable DOI/arXiv ID.
Coverage redundancy	TheoremSearch's arXiv-math content is already fully indexed by Semantic Scholar (Allen Institute) and arXiv's own API — both already librarian backends. Its unique value is search granularity, not unique coverage.
Non-arXiv content fails the contract	The only non-redundant content (ProofWiki, Stacks Project) is reference/encyclopedia material, not peer-reviewed papers with DOIs — it can't satisfy the librarian's "verifiable primary-source pointer" requirement.
Verification chain needs the abstract	The librarian's title-token-overlap + summary-grounding checks require an abstract → the /graph round-trip is mandatory, not optional. High latency, leaky abstraction.
Stability risk	8-star academic repo, no license, no SLA, no versioned API. The librarian's design explicitly rejected Google Scholar / scholarly for "TOS fragility" — TheoremSearch carries the same risk profile, unlike institutionally-backed SS/arXiv.
Zero demand within llmXive	Across 555 project YAMLs: psychology 74, statistics 72, materials science 72, biology 72, CS 65, chemistry 65, physics 63, neuroscience 61, mathematics 0. Pure math is also absent from the librarian's 8 default fields. There is no math-paper demand to serve.

Verdict

OUT_OF_SCOPE — not a librarian enhancement, and not worth a separate agent right now. Recommend closing this issue.

Proposed plan

1. Close integrate theoremsearch #111 as out-of-scope, with this comment as the rationale.
2. If math projects ever materialize in llmXive (none today), the right move is not to wire TheoremSearch as a librarian backend — it's to either (a) bump the librarian's backend list in a future spec to add a math-specific paper-level index (e.g., zbMATH Open API or MathSciNet, which return proper DOIs/MR-numbers and conform to the Candidate contract), or (b) build a small standalone "theorem-finder" tool that uses TheoremSearch's MCP server for formal-math / proof-assistant workflows — a genuinely different use case from "find me citations for a research question."
3. No code change to the librarian. The Q1 clarification ("Semantic Scholar + arXiv only; future spec may expand if these prove insufficient") stands — and they have not proven insufficient for the 8 STEM fields llmXive actually works in.

Related

• spec 005 librarian agent (PR Spec 005: librarian agent + Phase 1 re-validation #110, merged)
• Diagnostic: notes/2026-05-07-spec-005-librarian-diagnostic.md
• Q1 backend-scope clarification: specs/005-librarian-agent/spec.md (Clarifications)

[jeremymanning]

Revised direction + proposed plan

Correction to my earlier comment: the maintainer's call is that math papers should be in scope for llmXive (the absence of mathematics from the 8 default fields and the 555-project corpus is a gap to close, not a reason to skip). So this is not "close as out-of-scope" — it's "plan the right integration." After probing TheoremSearch's live API, the picture is more favorable than my first pass suggested.

What the live API actually gives us (verified, not the earlier reconstruction)

• POST /search → {theorems: [{theorem_id, name, body, slogan, theorem_type, link, paper: {paper_id, source, title, authors, link, summary, journal_ref, primary_category, categories, citations, year, journal_published}, similarity, score, has_metadata}]}
• For arXiv-sourced theorems: paper.paper_id is the versioned arXiv ID (1306.5434v2), paper.link is http://arxiv.org/abs/<id>, paper.year is present. → A clean Candidate mapping: strip the version suffix, call the librarian's existing ArxivClient.get_by_id(arxiv_id) to fill claimed_title / claimed_authors / claimed_abstract, set backend="theoremsearch". No second TheoremSearch call needed — the librarian already knows how to talk to arXiv.
• For non-arXiv sources (ProofWiki, Stacks Project): no DOI / arXiv ID — paper.link is the reference-site URL. Skip these — they can't satisfy the librarian's "verifiable primary-source pointer" contract. (They'd be relevant for Spec B's theorem-statement artifacts, not Spec A's paper-level citations.)
• Full OpenAPI at https://api.theoremsearch.com/openapi.json — endpoints: POST /search, GET /paper/{paper_id}, GET /paper-search, POST /statements, GET /statement/{statement_id}, GET /graph/*, plus an MCP server at /mcp. No auth, no documented rate limits.
• Stability caveat stands: small-team academic project (uw-math-ai/TheoremSearch, 8 stars, no license), no SLA. Mitigation: treat it like any other backend — failures are TransientBackendError, the librarian falls through to SS+arXiv, and if it ever disappears we just drop the client. The librarian never depends on it being up.

Architecture decision

Two phased specs. TheoremSearch enters as a librarian backend now (Spec A); a theorem-statement artifact agent comes later only if math-theory projects show they need it (Spec B).

• Spec A keeps the librarian as the single entry point and single verifier — TheoremSearch is just another Candidate-producing client alongside SemanticScholarClient and ArxivClient. Its output flows through the existing verify chain (URL resolves → title-overlap ≥0.7 → summary-grounded ≥0.5 → LLM relevance judge), so the librarian's JSON contract is unchanged. The relevance judge filters any off-topic TheoremSearch hits, so false-positive triggers are cheap (a wasted API call, not bad output).
• Spec B is a genuinely new agent (theorem_searcher) with a new artifact: theorem statements (statement text + slogan + theorem type + source paper + source link + a "we fetched the LaTeX and confirmed the statement matches" verification flag), written to a ## Related theorems subsection of the math project's idea.md — parallel to the librarian's ## Search trail. Deferred until there's demand.

Trigger logic (Spec A)

In LibrarianAgent.invoke(), after the existing extracted-query searches:

if field == "mathematics":
    candidates += TheoremSearchClient().search(term)   # always
elif _is_math_theory_question(term, idea_body_excerpt):  # LLM classifier
    candidates += TheoremSearchClient().search(term)

• field == "mathematics" → always query TheoremSearch (deterministic, no classifier).
• field != "mathematics" → one LLM call: "Is this a pure-mathematics question about theorems, proofs, or formal mathematical structures? yes/no" — catches math-heavy questions in physics/CS/statistics. Costs +1 LLM call and introduces the same non-determinism class as Librarian relevance-judge is non-deterministic (LLM temperature noise) #112 (acceptable: a missed trigger just means TheoremSearch isn't consulted that run; SS+arXiv still cover it). Cache the classifier verdict in the librarian cache keyed by (question_hash, prompt_version) so re-runs are stable.

Spec A — concrete task list (small)

1. Add mathematics to the librarian's 8 default fields → 9. Touches: tests/phase2/test_librarian_cross_domain.py (DEFAULT_FIELDS), the brainstorm agent's field enum, and any field-list constant. Verify a math project exists in state/projects/ to cross-domain-test against; if not, brainstorm one (or accept the test skips mathematics until a math project is brainstormed — same pattern as the existing "no brainstormed projects found for field=X" skip).
2. New module src/llmxive/librarian/theoremsearch.py — TheoremSearchClient with search(term, *, limit=10) -> list[Candidate]:
   • POST https://api.theoremsearch.com/search with {query: term, limit: ...}
   • For each result where paper.source == "arXiv": extract paper.paper_id, strip v\d+ suffix, call ArxivClient.get_by_id(arxiv_id) for the full record, emit Candidate(backend="theoremsearch", primary_pointer=arxiv_id, claimed_title=..., claimed_authors=..., claimed_year=..., claimed_venue="arXiv", claimed_abstract=...).
   • Skip non-arXiv results.
   • De-dup against arXiv IDs already returned (the librarian's merge_candidates does this by primary_pointer, so just emit and let it dedup).
   • Token-bucket rate limiter (same pattern as ArxivClient — be conservative, ~1 req/2s).
   • Errors → TransientBackendError so the router falls through.
3. New module src/llmxive/librarian/math_classifier.py (or fold into query_extractor.py) — is_math_theory_question(term, idea_body_excerpt, *, model, ...) -> bool via a single LLM call; fail-open to False (don't block on a flaky classifier); cache the verdict.
4. Wire both into LibrarianAgent.invoke() per the trigger logic above; thread the new candidates into the existing merge → verify → judge chain (no chain changes — TheoremSearch Candidates carry arXiv IDs, which the verify chain already handles).
5. Bump librarian prompt_version (the classifier is a new LLM call) → cache-invalidating; re-run cross-domain + PROJ-261/262 re-validation.
6. Tests: tests/phase2/test_theoremsearch.py — parser tests on a recorded /search response (arXiv vs ProofWiki branching), real-API smoke test gated on network, the Candidate mapping, dedup; tests/phase2/test_math_classifier.py — parser + a real-LLM smoke (math question → True, non-math → False); add a mathematics parametrization to test_librarian_cross_domain.py.
7. Update agents/registry.yaml librarian entry comment (now 3 backends + a math classifier), the diagnostic, and specs/005-librarian-agent/spec.md Q1 clarification (it explicitly anticipated "future spec may expand the backend list" — this is that spec).
8. Decide: a new tiny spec doc (specs/006-theoremsearch-backend/ or fold into a spec-005 amendment)? Given the size, I lean spec-005 amendment — it's a backend addition the original spec anticipated, not a new feature.

Spec B — deferred (sketch only)

A theorem_searcher agent with a ## Related theorems artifact output, triggered by the librarian for field == "mathematics" theorem-shaped questions. Uses POST /statements + GET /statement/{id} to pull full statement bodies; verifies by fetching the source paper's LaTeX and confirming the statement text appears. New prompt, new output contract, new tests. Park until a math-theory project demonstrates it's needed.

Open questions for the maintainer

1. Spec A as a spec-005 amendment, or a fresh specs/006-theoremsearch-backend/? (I lean amendment — small, anticipated by Q1.)
2. The LLM math-classifier for non-math fields — keep it (catches cross-field math at +1 LLM call + non-determinism) or skip it (only trigger on field == "mathematics", simpler, but misses a physics project on topological invariants)? My lean: keep it but cache the verdict.
3. mathematics as a 9th default field — brainstorm a seed math project now, or let the cross-domain test skip mathematics until one appears organically? (The brainstorm agent would need to start producing math projects regardless, for this to matter.)
4. Non-arXiv TheoremSearch sources (ProofWiki, Stacks Project) — confirmed out of Spec A (no DOI/arXiv ID), but they're the natural input for Spec B's theorem-statement artifacts. Just flagging that the "skip non-arXiv" decision is Spec-A-scoped.

---

(Supersedes the "close as out-of-scope" verdict in my earlier comment — that was predicated on math being out of llmXive's scope, which the maintainer has corrected.)

[jeremymanning]

Quick answers:

1. Amendment seems like the right direction
2. Yes, keep LLM math-classifier for non-math fields and cache the verdict on a per-project basis
3. add math as the 9th default field and brainstorm 5 seed math projects
4. for spec A we can skip non-arxiv sources. keep non-arxiv sources (any source is worth exploring, with the caveat that quality needs checks in all cases!) for spec B.

[jeremymanning]

Spec issues opened

Per the maintainer's answers:

1. ✅ Spec A is a spec-005 amendment (not a new spec dir)
2. ✅ Keep the LLM math-classifier for non-math fields; cache the verdict per-project
3. ✅ Add mathematics as the 9th default field + brainstorm 5 seed math projects
4. ✅ Spec A skips non-arXiv TheoremSearch sources; Spec B keeps them, with quality checks on all sources

Tracking issues:

• Spec A: TheoremSearch backend for the librarian + mathematics as 9th default field #113 — Spec A: TheoremSearch backend for the librarian + mathematics as 9th default field (spec-005 amendment). Small. Starting /speckit-specify now.
• Spec B: theorem_searcher agent — theorem-statement artifacts for math-theory projects #114 — Spec B: theorem_searcher agent — theorem-statement artifacts (## Related theorems idea.md subsection). Deferred until a math-theory project shows it's needed; depends on Spec A: TheoremSearch backend for the librarian + mathematics as 9th default field #113.

This issue (#111) stays open as the umbrella; it'll close when both #113 and #114 are done (or when #114 is explicitly declined as unneeded).

[jeremymanning]

Spec A (#113) implemented: PR #117 — TheoremSearch as the librarian's 3rd backend + LLM math-classifier + mathematics as the 9th default field + 5 seed math projects + librarian prompt bump 1.5.0→1.6.0. 9-field cross-domain re-run 9/9 PASS (mathematics returned 6 TheoremSearch-sourced citations); PROJ-261/262 re-validate verified. Spec B (#114 — theorem-statement artifacts, non-arXiv sources, standalone theorem_searcher agent) remains the deferred follow-up.