TheoremGraph links 11.7M informal theorems to formal proofs
A unified graph connecting 18.3M dependencies across informal and formal math
Mathematical knowledge is fragmented: informal papers cite at the document level, while formal libraries (like Lean) record fine-grained statement dependencies but cover far less content. TheoremGraph bridges this gap by constructing a unified, statement-level dependency graph across both worlds. The informal side parses 11.7M theorem-like environments from arXiv papers, extracting 18.3M candidate directed dependencies with labeled extractors for precision trade-offs. The formal side introduces LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects.
To link the two graphs, the team generates natural-language slogans for each statement and embeds them into a shared semantic space. An LLM judge validates 47,952 matches above a cosine threshold of 0.8, with acceptance rates climbing from 48% at the floor to 87% for matches >=0.9. In formal concept retrieval, a simple name-and-signature representation with graph expansion achieves a Recall@10 of 0.775, within 0.5pp of LeanSearch v2’s reranked result (0.780) — without any language model reranker. The full dataset, extractors, HTTP API, and MCP interface are released as open-source infrastructure for mathematical search, attribution, and retrieval-augmented reasoning.
- Parsed 11.7M theorem environments from arXiv, yielding 18.3M labeled informal dependencies
- LeanGraph provides 388K Lean 4 declaration nodes and 11.3M typed edges across 25 projects
- LLM-validated cross-domain matches (47,952) reach 87% acceptance at cosine >=0.9
Why It Matters
Unifies mathematical reasoning across informal papers and formal proofs, enabling better AI for theorem proving and search.