TheoremGraph: Bridging Formal and Informal Mathematics
AuthorsSimon Kurgan, Evan Wang, Eric Leonen, Sophie Szeto, Luke Alexander, Artemii Remizov, Jarod Alper, Giovanni Inchiostro, Vasily Ilin
Resources
This work builds a massive bridge between informal math papers and formal proof libraries, making the structure of mathematics searchable across both worlds.
Key results
Statements parsed from mathematics arXiv.
Directed dependencies recovered across the informal corpus.
Formal declaration nodes extracted across 25 Lean projects.
GPT-5.4-accepted matches above cosine similarity 0.8.
Recall-optimized TheoremGraph configuration, compared with LeanSearch v2’s 0.780.
Correct targets out of 24 with retrieval-augmented generation, versus 5/24 without retrieval.
What the paper found
TheoremGraph, from the University of Washington Math AI Lab, introduces a statement-level dependency graph that connects informal mathematical literature with formal Lean proofs. Its informal pipeline parses 11.7M theorem-like statements from mathematics arXiv and recovers 18.3M directed dependencies, while LeanGraph extracts 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. To bridge the two ecosystems, the authors generate natural-language slogans with Qwen3-235B-A22B-Instruct-2507, embed them using Qwen3-Embedding-8B, and retrieve cross-formality nearest neighbors through an HNSW index. GPT-5.4 judges 47,952 candidate formal–informal matches above cosine similarity 0.8, with acceptance reaching 87% for candidates scoring at least 0.9; DeepSeek-V4-Pro is reported as a more permissive comparison. Graph expansion and name-and-signature representations improve MathlibQR fair-810 Recall@10 to 0.775, within 0.5 percentage points of LeanSearch v2’s 0.780 reranked score without an LM reranker. In retrieval-augmented autoformalization, Claude Sonnet 4-6 improves evaluated correctness from 5/24 without retrieval to 8/24 with retrieved premises, while using 14k output tokens and 68 tool calls. Additional experiments show citation-graph expansion raises Qwen3-8B premise-retrieval recall from 7.9% to 13.4%, though Gemini 3.1 Pro, GPT-5.5, ChatGPT 5.4, and Claude models remain important comparison points. The released dataset, extractors, HTTP API, and MCP interface target mathematical search, attribution, and retrieval-augmented theorem proving.
Original abstract
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.
Read the original paperMore in AI for Science
Browse all 43 papers →AI-guided high-throughput discovery of iridium- and ruthenium-free palladium-oxide catalysts for durable acidic oxygen evolution
Ken J. Jenewein, Faezeh Habib Zadeh, Xiaoxiao Wang, Gustavo Malkomes, Huafan Zhang, Natalie Page, Jae Jin Bang, Peter J. Santiago, Karla V. Contreras, Katherine K. Li, Allison Perna, Lorena M. Britton, Fahrettin Kilic, Kevin J. Cruse, Armin Taheri, Krishnanand Mallayya, Harley Quinn, Rebecca A. Durr, Peter A. Beaucage, John M. Gregoire, Rafael Gómez-Bombarelli
An AI-guided robotic lab discovered palladium-based catalysts that could make acidic water electrolysis more durable while reducing dependence on scarce iridium and ruthenium.
Discovery of radio emission from the exoplanet $β$ Pictoris b
Kevin N. Ortiz Ceballos, Edo Berger, Yvette Cendes
Astronomers have detected radio auroras from β Pictoris b, revealing that this distant giant planet has a magnetic field at least 1.25 kilogauss strong.
EurekaBench: Measuring Agentic Ability to Discover New Scientific Insights
Jiayi Geng, Zhengxuan Wu, Kevin S. Chen, Seungone Kim, Joseph Janssen, Zora Zhiruo Wang, Bhupalee Kalita, Runtian Gao, Aaron Ho, Andrew Oakleigh Nelson, Olexandr Isayev, Francisco Villaescusa-Navarro, Ching-Yao Lai, Howard Chen, Graham Neubig
EurekaBench tests whether AI agents can move beyond accurate prediction to uncover mechanisms and insights that genuinely advance scientific understanding.