TheoremGraph: Bridging Formal and Informal Mathematics

Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both: 11.7M theorem-like environments parsed from mathematics arXiv with 18.3M candidate directed dependencies, each labeled by the extractor that proposed it, and LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space; an LLM judge affirms 47,952 (informal, formal) matches among the candidates above a 0.8 cosine-similarity floor (48% of those judged), with the acceptance rate rising to 87% for scores ≥ 0.9. On the MathlibQR fair-810 retrieval benchmark, our name-and-signature retriever, reranked with the same Qwen3-Reranker-8B protocol as LeanSearch v2, reaches 0.883 Recall@10 / 0.739 nDCG@10, +10.3pp / +11.6pp over its reranked system, a comparison we verify by reproducing its reported numbers with our code. A recall-tuned variant of our retriever comes within 0.5pp of that reranked recall with no reranker at all. On 24 held-out Mathlib theorems, retrieval raises the number of correctly autoformalized statements from 5 to 8, using a quarter of the tokens of library search. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and agentic formalization.