One-sentence Summary

TheoremGraph, a unified statement-level dependency graph introduced by the University of Washington Math AI Lab, parses $11.7\mathrm{M}$11.7M theorem-like environments from arXiv and extracts Lean-Graph’s $388,105$388,105 declaration nodes and $11.3\mathrm{M}$11.3M typed edges across $25$25 Lean projects, bridges them via embedded natural-language slogans and an LLM judge to produce $47,952$47,952 matches above $0.8$0.8 cosine similarity (with acceptance rising to $87\%$87% at the $\geq 0.9$≥0.9 tier), and achieves formal concept retrieval using name-and-signature representation and graph expansion within $0.5\mathrm{pp}$0.5pp of LeanSearch v2’s reranked $Recall@10$Recall@10 ($0.775$0.775 vs. $0.780$0.780) without an LM reranker, thereby enabling mathematical search and retrieval-augmented reasoning.

Key Contributions

• TheoremGraph combines 11.7 million theorem-like environments and 18.3 million candidate directed dependencies from mathematics arXiv with Lean-Graph, an extractor that captures 388,105 declaration nodes and 11.3 million typed edges across 25 Lean projects, forming a unified statement-level dependency graph spanning informal and formal mathematics.
• Embedding generated natural-language slogans into a shared semantic space bridges the informal and formal graphs, producing 47,952 matches affirmed by an LLM judge above a 0.8 cosine floor, with the judge acceptance rate rising from 48% at that floor to 87% for pairs with similarity ≥ 0.9.
• A name-and-signature representation with graph-based expansion achieves 0.775 Recall@10 on formal concept retrieval, within 0.5 percentage points of LeanSearch v2’s reranked 0.780, without a language-model reranker; the dataset, extractors, API, and MCP interface are released as open infrastructure.

Introduction

Mathematics is inherently a web of interdependent statements, but in practice researchers cite papers rather than the specific lemmas or theorems they use. This coarsening obscures attribution, hides duplication, and makes it hard to navigate the literature at the statement level. Formal proof assistants like Lean capture precise dependency structures, yet their libraries cover only a small fraction of existing mathematics, and no unified graph spans the informal and formal worlds.

Prior work addresses pieces of the puzzle: mathematical information retrieval handles symbolic formulas, bibliometrics models paper-level citations, and neural tooling targets theorem proving or autoformalization. However, these approaches do not connect fine-grained dependencies across informal research articles and formal verification libraries, limiting cross-formality search and large-scale dependency analysis.

The authors tackle this gap by constructing TheoremGraph, a statement-level dependency graph that links 11.7 million informal statements from arXiv (18.3 million edges) with 388,105 declarations from Lean and 25 formal projects (11.3 million typed edges). They align both corpora in a shared embedding space using sloganized statement representations, validated by an LLM judge to yield over 47,000 high-confidence cross-formality matches. This unified resource improves retrieval-augmented autoformalization and comes within 0.5 percentage points of a specialized reranker’s performance while requiring no reranker, and it is released as a public dataset, API, and MCP interface.

Dataset

The authors construct three interconnected datasets to link informal mathematical writing with formal proof assistants, providing a resource for neural theorem provers and auto-formalization systems.

• Informal Graph (arXiv mathematics papers) Source: arXiv Kaggle metadata snapshot, filtered to mathematics-tagged papers, with their LaTeX source. Scale: 11.7 million theorem-like statements and 18.3 million directed dependency edges (within and across papers). Extraction & filtering: A regex-based parser identifies theorem environments and records each statement’s type, reference number, \label key, body, proof, and local context. Statements are filtered out if they have empty bodies, unbalanced math delimiters, very short content, or end mid-clause. Edge types: Edges are tagged with the extractor(s) that proposed them: deterministic (\ref/\cite resolution via arXiv IDs or title matching, with citation-to-statement resolution), heuristic (backward document-order references, discourse cues, prose theorem names), and notation (LLM-identified notation definitions and uses, linked to the closest prior definition). Each edge retains its extractor label, letting users trade coverage for precision; deterministic edges reach 98.8% judge-verified precision.

• Formal Graph (Lean 4 projects) Source: Compiled Lean 4 projects, including Mathlib versions 4.27–4.29 and 24 other libraries. Scale: 388,105 declaration nodes and 11,335,708 total typed edges (9.3M within Mathlib alone). Extraction: LeanGraph runs as a Lean 4 elaborator over the kernel Environment API, extracting dependencies from elaborated, type-checked declarations. Nodes are included only if they satisfy a structural predicate that removes kernel-generated artifacts (auxiliary recursors, matcher declarations, etc.), keeping user-facing declarations. Anonymous instances and tactic objects are retained with metadata. Edge types: Six semantic categories: extends (inheritance), field (structure field dependencies), sig (signature constants), proof (proof-term constants), def (non-Prop definition bodies), and docref (docstring references). This taxonomy separates structural, type-level, value-level, and documentation dependencies.

• Bridge Graph (Universal Graph) Construction: Formal declaration slogans and informal statement slogans are embedded into a shared vector space. For each of 385,657 formal declarations, the single most similar informal slogan is retrieved by cosine similarity (ann_k=50). Author-written blueprint pairs serve as ground truth: the annotated informal partner ranks first 43.5% of the time and in the top ten 69.9% of the time, and among top candidates with similarity ≥0.85, a GPT-5.4 judge affirms 65% as valid matches (exact or inexact restatements). Curated matches: All candidates with cosine similarity ≥0.8 are judged by GPT-5.4. Out of 100,799 candidates, 47,952 (48%) are affirmed as matches; the affirmation rate climbs steeply with similarity (87% for the ≥0.9 tier). Each bridge edge stores the similarity score, the judge’s exact/inexact/wrong label, and the deterministic graph context, enabling high-precision cross-modal linking. Intended use: The bridged graphs provide a scaffold for neural theorem provers and auto-formalization systems, connecting what a formal declaration depends on with the informal mathematics that uses or describes those concepts.

Method

The authors construct a comprehensive mathematical knowledge graph by first building an Informal Graph from arXiv papers and then bridging it with a formal graph of Lean declarations to create a Universal Graph.

For the Informal Graph, the authors parse over 11.7 million theorem-like statements from mathematics arXiv papers. They employ a regex-based parser to identify theorem-like environments, capturing metadata, references, and LaTeX source. Dependency edges are extracted using three methods: a deterministic extractor resolving references and citations, a heuristic extractor adding edges from nearby references and discourse cues, and a notation extractor using an LLM to link notation usage to prior definitions.

To unify the informal and formal graphs, the authors map every statement into a shared semantic space. They generate a slogan for each statement, which is a concise natural-language summary produced by an LLM. For informal statements, an escalating prompt chain adds context until a sufficient summary is generated. These slogans are then embedded into $\mathbb{R}^{4096}$R4096 using Qwen3-Embedding-8B and $\ell_2$ℓ2​-normalized. The vectors are stored in an index with HNSW for efficient retrieval.

To bridge the formal and informal corpora, the authors implement a matching pipeline to find pairs of statements expressing the same mathematical result.

As shown in the figure below:

The pipeline begins by sloganizing both Lean declarations and LaTeX statements into plain-English descriptions. These slogans are embedded into a single shared index. For each formal declaration, the system retrieves the most similar informal slogan via rank-1 cosine similarity search, proposing a candidate match.

To validate these matches, an LLM-as-judge (GPT-5.4) evaluates each candidate with a cosine similarity of 0.8 or higher. The judge labels pairs as exact, inexact (generalizations or special cases), or wrong. The authors set the similarity floor at 0.8 to capture a broad band of inexact matches while maintaining precision, as the yield rate collapses below this threshold.

The distribution of verdicts across different similarity bins illustrates the effectiveness of this approach.

As shown in the figure below:

The chart demonstrates that as cosine similarity increases, the proportion of exact and inexact matches rises significantly, while wrong matches decrease. The stricter GPT-5.4 judge is adopted as the record to favor precision, though a more lenient judge is reported for high-recall comparison. This embedding-based matching allows formal statements to be paired with informal counterparts directly through similarity, without requiring shared vocabulary.

Experiment

Retrieval augmented formalization experiments show that adding slogan based retrieval improves an LLM's ability to restate informal math into Lean, raising evaluated correctness while using far fewer tokens and tool calls than full library grep, though typechecking alone is a misleading success signal. A comparison against the LeanSearch‑v2 retriever reveals that embedding only the slogan underperforms the baseline, but adding a name‑and‑signature representation, query rewriting, and a name‑matching index closes the gap, reaching higher recall and nDCG without a reranker. These interventions primarily boost retrieval for declaration types poorly served by slogans (structures, classes) at a slight cost to theorems, and the same tuned configuration does not transfer to chained‑premise retrieval, indicating task‑specific trade‑offs.

Switching from descriptive slogans to a name-and-signature representation substantially improves retrieval ranking, while keeping the slogan or expanding with a dependency graph yields small recall gains at a minor ranking cost. These changes primarily benefit categories where slogans were weakest, such as structures and definitions, with little effect on theorem and instance retrieval. Using name-and-signature embeddings (Configuration F) raises nDCG@10 from 0.494 to 0.558 and Recall@10 from 0.657 to 0.733 over the retriever-only baseline, surpassing it on every reported metric. The representation alone accounts for the ranking gain, since configurations B and F share identical search techniques and differ only in what is embedded. Mixing the slogan back in (Configuration D) and adding graph expansion (Configuration E) improves Recall@10 to 0.775 at the expense of nDCG@10 dropping to 0.548, approaching the reranked recall of 0.780 without a reranker. Graph expansion contributes the least among levers: it adds +0.8 pp Recall@10 and costs –0.2 pp nDCG@10 when moving from D to E. Per declaration type, structures, classes, definitions, and inductives benefit most from the interventions, while theorem and instance retrieval slightly declines because they already possess strong slogans.

Three extractors contributed overlapping sets of informal dependency edges, with the notation extractor producing the most edges overall, all within the same paper. The deterministic extractor identified the largest number of external edges, including a subset that link to specific named theorems. After deduplication, the combined set contains 18.32 million edges, predominantly within-paper. The notation extractor yields the most edges (7.88M) and all are within-paper. Deterministic extraction captures more external edges (1.92M) than heuristic (1.70M), including 79K that point to a specific theorem. After deduplication, within-paper edges (14.86M) outnumber external edges (3.46M) by over four to one.

An LLM-based judge evaluates dependency edges extracted from 500 arXiv papers. The deterministic extractor achieves near-perfect precision (98.8% verified), while the heuristic and notation extractors show progressively lower precision. The combined, deduplicated set yields 68.1% precision, but a large number of dependencies (6,372) are found solely by the judge, resulting in an overall F1 of 0.642. Deterministic extraction is the most reliable, with 98.8% of its edges confirmed by the judge, giving users a high-confidence label when precision matters. Extractors collectively miss 6,372 judge-identified edges, revealing a considerable gap in recall that leaves room for improvement.

The escalating prompt chain generated slogans for all 11.75 million informal statements, resolving the majority with minimal context. Only 1.9% of statements required the final forced fallback, and 70.3% succeeded with just the statement body. This incremental strategy adds context only when prior stages self-flag as insufficient, ensuring coverage without wasted computation. Using only the statement body, 70.3% of slogan generations were already sufficient. Slogan sufficiency reached 98.1% before the forced fallback, leaving just 1.9% that needed a best-guess completion.

When matching formal Lean declarations to informal statements by embedding similarity, only a small minority achieve high cosine similarity above 0.90. Most successful matches concentrate in a moderate band between 0.50 and 0.80, while over 44% of declarations find no neighbor at the default retrieval depth. Deeper search reveals that these missing matches generally reflect a genuine absence of close informal counterparts rather than a limitation of the retrieval scope. A tiny fraction of formal declarations obtain very high similarity informal matches, while the majority of matches fall into a moderate 0.50–0.80 range and a large share have no match at all. Probing deeper with larger shortlists recovers candidates for most previously unmatched declarations, but almost none exceed 0.85 similarity, confirming that missing matches indicate true gaps in informal coverage rather than shallow search.

The evaluation analyzes retrieval improvements from replacing slogans with name-and-signature embeddings, the effectiveness of an escalating prompt chain for generating slogans, and the extraction of dependency edges from informal mathematics. Name-and-signature representations yield the strongest ranking gains, particularly for categories where slogans were weak, while mixing slogans back or adding graph expansion provides modest recall benefits at a minor ranking cost. The prompt chain attains 98.1% slogan sufficiency before forced fallback, and deterministic edge extraction achieves near-perfect precision but misses many edges, indicating recall gaps. Matching formal declarations to informal statements reveals that over 44% lack close counterparts, confirming genuine coverage gaps rather than search limitations.