# TheoremGraph: Bridging Formal and Informal Mathematics

arXiv: https://arxiv.org/abs/2606.25363 · HTML: https://mlsanity.com/paper/2606.25363/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 47 references that are in the map.
- First posted on arXiv 24 Jun 2026.

## Builds on (most cited first, 21 of 21)

- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models](https://mlsanity.com/paper/2506.05176/) (2025)
- [Efficient and robust approximate nearest neighbor search using Hierarchical Navigable Small World graphs](https://mlsanity.com/paper/1603.09320/) (2016)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Nougat: Neural Optical Understanding for Academic Documents](https://mlsanity.com/paper/2308.13418/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [A Comprehensive Survey on Reinforcement Learning-based Agentic Search: Foundations, Roles, Optimizations, Evaluations, and Applications](https://mlsanity.com/paper/2510.16724/) (2025)
- [miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward](https://mlsanity.com/paper/2511.03108/) (2025)
- [MLFMF: Data Sets for Machine Learning for Mathematical Formalization](https://mlsanity.com/paper/2310.16005/) (2023)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [WithdrarXiv: A Large-Scale Dataset for Retraction Study](https://mlsanity.com/paper/2412.03775/) (2024)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database](https://mlsanity.com/paper/2505.13406/) (2025)
- [The Tangent Search Engine: Improved Similarity Metrics and Scalability for Math Formula Search](https://mlsanity.com/paper/1507.06235/) (2015)
- [Generalizable LLM Learning of Graph Synthetic Data with Post-training Alignment](https://mlsanity.com/paper/2506.00845/) (2025)
- [Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization](https://mlsanity.com/paper/2604.16347/) (2026)

## Built on by (most cited first, 5 of 5)

- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs](https://mlsanity.com/paper/2607.16997/) (2026)
- [Beyond Correctness: Toward Automated Novelty Verification with Lean 4](https://mlsanity.com/paper/2608.14669/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)

## Abstract (arXiv)

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 informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release 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, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.