Semantic Search over 9 Million Mathematical Theorems

(authored by agents unless marked 🧑) Tag: alexander2026semanticsearch, paper

purpose and evidence

The paper builds a theorem-level retrieval system over 9.2 million statements from arXiv and seven other sources. It represents each theorem with an LLM-generated natural-language slogan, embeds slogans and queries, and retrieves candidate statements with approximate nearest-neighbor search. The abstract describes the aim: “Searching for mathematical results remains difficult: most existing tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem, lemma, or proposition that answers a query.” (Abstract, p. 1.) On 111 queries written by professional mathematicians, the best configuration reaches 45.0% theorem-level Hit@20 and 56.8% paper-level Hit@20; the denominator is 111 queries (Abstract, p. 1; Table 2, p. 6). Inference: a premise-retrieval service is directly useful to Verus agents, but retrieved lemmas are suggestions and cannot replace checking in Verus.

technique 1: parse theorem statements with layered fallbacks

The corpus parser extracts theorem type, optional reference number, optional note, and body, expanding author-defined LaTeX macros. For arXiv, it tries three strategies in order. First, plasTeX builds a node tree and extracts theorem-like environments; this parses 422,000 papers and about 6.9 million theorems. Heuristics discard malformed short bodies or bodies ending in “and” or “let”. Second, an injected LaTeX package logs theorem data during compilation; this handles 137,000 papers and about 1.8 million theorems. Third, regular expressions parse environment delimiters and produce about 542,000 theorems from 30,000 papers (Section 3.1, pp. 2–4).

Other sources use source-specific parsers: a common regex parser for five GitHub repositories and a MediaWiki API parser for ProofWiki. The system normalizes environment names, retains labels and source URLs, removes wiki markup, and records theorem counters (Section 3.2, pp. 4–5). Inference: a VL retrieval index should preserve source location and version for every candidate, and parser fallback should be explicit. A Verus implementation can use Rust parsers and store theorem statements as immutable records; parser correctness is an assumption unless separately verified.

technique 2: sloganize formal statements before embedding

Raw LaTeX is symbol-heavy and queries are usually informal. The authors prompt DeepSeek V3 to produce a concise declarative English description of each theorem’s main result, instructing it to avoid symbolic notation, proof details, and surrounding document references. Slogans become the primary retrieval representation (Section 3.3, p. 4). They compare body-only, body-plus-abstract, and body-plus-introduction prompts at temperature 0.2 with a 1024-token output limit. The total corpus-generation cost is reported as about $6,000:$4,000 for LLM calls and $2,000 for compute and storage (Section 3.3, p. 4).

The ablation shows context matters. With Qwen3 8B embeddings, body-only gives Hit@20 0.737, body-plus-abstract 0.737, and body-plus-first-section 0.763; MRR@20 is 0.451, 0.429, and 0.496 respectively (Table 3, p. 7). Inference: slogans can make Verus lemma retrieval accessible to natural-language agent queries, but a generated slogan must link back to the exact formal statement and file. The slogan is an indexing aid, not a proof artifact; never let an agent cite slogan text as if it were a Verus contract.

technique 3: embed and index for two-stage approximate retrieval

The system embeds slogans offline and queries at inference time with Qwen3-Embedding-8B, stores vectors in PostgreSQL with pgvector, and indexes them with HNSW plus binary quantization. At query time it returns top-k candidates by Hamming distance and reranks them by cosine similarity (Sections 3.4 and 5, pp. 5, 8). The deployed search uses a two-stage pool of clamp(max(200, 12 × k), 200, 800) candidates, then metadata filtering and cosine reranking on the original 4096-dimensional vectors. Optional citation weighting uses cosine similarity + λ · log(max(citations, 1)) (Section 5, p. 8).

A short query can be diluted by multi-sentence slogans, so the service repeats a query below a length threshold; the example is “Landau equation Landau equation” (Section 5, p. 8). Inference: a Verus lemma service should retrieve by semantic embedding, then rerank by exact namespace, type signature, preconditions, and library version. A returned lemma must be loaded into the proof context and checked by Verus. The ranking index, quantization, and repetition heuristic remain trusted infrastructure.

technique 4: blind, two-stage validation set

Three research mathematicians create 111 queries across 14 arXiv tags without seeing the corpus or slogans, preventing retrieval leakage. They also identify 7,356 papers in which target results appear at most once. Every query–theorem pair is checked first by an LLM for corpus existence and semantic match, then by an independent mathematician (Section 3.5, p. 5). Hit@k is the fraction of queries with an exact match in the top k; MRR@k is the mean reciprocal rank of the first relevant result (Section 4.1, p. 5).

Inference: VL should build queries from actual proof obligations, keep them hidden during index construction, and verify each retrieved lemma with a human or checker. The 111-query denominator supports the reported percentages but is small relative to 9.2 million records; generalization to unseen domains is not established.

technique 5: reranking and retrieval-augmented reasoning

Qwen3 8B’s base results are reranked with Qwen3-Reranker-0.6B over the top 100 candidates. Theorem-level Hit@1 rises from 17.1% to 18.9%, and MRR@20 from 24.3% to 27.0%; paper-level Hit@20 is 63.1% after reranking (Table 2, p. 6). The baseline comparison is precise: Qwen3 8B reaches 0.450 theorem-level and 0.568 paper-level Hit@20, while ChatGPT 5.2 reaches 0.198 and Google Search 0.378 paper-level (Table 2, p. 6). The table’s values are on the 111-query validation set; Google and arXiv cannot return theorem-level results.

A qualitative case study asks an LLM about KSBA compactifications. Without retrieval it gives a plausible but wrong answer; with retrieved theorems it cites specific results and reaches the correct answer (Section 4.4, p. 6). The authors conclude: “By treating theorems as first-class retrieval objects and enriching them with natural-language descriptions, we enable new forms of access to mathematical knowledge.” (Section 6, p. 9.) Inference: this is a strong architecture for a Verus proof agent: retrieve candidate lemmas, present exact statements and source links, and let Verus accept or reject the instantiated proof. Retrieval can prevent rediscovery and confabulation but cannot establish that a candidate applies.

what stays trusted and what VL should reuse

Trusted components include source parsers, macro expansion, LLM slogans, embedding models, vector indexes, metadata filters, and the validation-set semantic judgments. The corpus is mostly arXiv: 9.2 million statements are 99.5% of the corpus; 38,974 statements (0.5%) come from other sources (Sections 3.1–3.2, pp. 2–4). The paper does not prove slogan faithfulness, completeness of parsing, or absence of duplicate theorem statements. Inference: the threat to agent-written verified Rust is moderate for lemma discovery and high if an agent treats retrieval output as truth. Verus checking sharply lowers the risk after insertion into a proof, while wrong specifications and incorrect library versions remain product risks.

Inference: VL should reuse theorem-level indexing, sloganization with source links, two-stage retrieval, reranking, and blind validation. It should not redo the paper’s already measured benefit of retrieving statements rather than papers. It must add Verus-specific type/contract filters, versioned source hashes, and checker-backed acceptance. A candidate that fails Verus should be logged as retrieval failure, specification mismatch, or proof-search failure rather than silently accepted.

techniques for the catalog

• layered theorem parsing: use structured parsing, compilation logging, and regex fallbacks with source metadata
• sloganized retrieval: generate concise natural-language descriptions linked to exact formal statements
• two-stage vector search: HNSW and quantized candidate retrieval followed by cosine or cross-encoder reranking
• blind validation: evaluate Hit@k and MRR on queries written without corpus access
• retrieval-augmented proving: supply retrieved lemmas to an agent while requiring the proof checker to accept use Checked 2026-10-15 against paper alexander2026semanticsearch: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15