TheoremGraph: Bridging Formal and Informal Mathematics

Mathematical knowledge is fragmented: informal research papers cite documents rather than specific theorems, while formal proof assistants like Lean maintain precise, fine-grained dependency graphs. This paper addresses the lack of a unified structure, aiming to bridge these two worlds to improve mathematical search, attribution, and automated reasoning.

The authors construct TheoremGraph by extracting dependency data from two distinct sources. For informal mathematics, they parse 11.7 million theorem-like environments from arXiv, recovering 18.3 million directed dependency edges. For formal mathematics, they introduce LeanGraph, a tool that extracts 388,105 declaration nodes and 11.3 million typed edges from 25 Lean projects. To bridge these graphs, the authors generate natural-language "slogans" for every statement, embed them into a shared semantic space, and use an LLM judge to verify 47,952 matches between formal declarations and informal statements.

The study demonstrates that a shared embedding space can effectively align formal and informal mathematics. The matching pipeline achieves high precision, with an LLM judge affirming matches with an 87% acceptance rate for pairs with a cosine similarity of 0.9 or higher. Furthermore, the authors show that their name-and-signature representation for formal concept retrieval performs competitively with existing state-of-the-art tools like LeanSearch v2, achieving a Recall@10 of 0.775 without requiring an additional language model reranker.

By providing a unified, queryable interface for both formal and informal mathematics, TheoremGraph serves as critical infrastructure for the next generation of AI-assisted mathematical research. It allows researchers to trace the origins of mathematical results across different formats, helps identify duplicate work, and provides a scaffold for auto-formalization systems to translate informal research into machine-verified proofs.