PaperlayerView exact revision on arXiv

Source-linked AI summary

TheoremGraph: Bridging Formal and Informal Mathematics

Simon Kurgan, Evan Wang, Eric Leonen, Sophie Szeto, Luke Alexander, Artemii Remizov, Jarod Alper, Giovanni Inchiostro, Vasily Ilin

arXiv:2606.25363v1cs.IRcs.AImath.HO

TL;DR

Informal mathematics exposes dependencies coarsely, while formal libraries cover a smaller body with finer structure. TheoremGraph unifies statement-level graphs across both settings and links them through slogan embeddings, with retrieval approaching LeanSearch v2 and 47,952 LLM-affirmed matches.

  • Problem

    Informal papers usually cite documents rather than exact mathematical statements, making fine-grained dependencies and attribution difficult to track.

  • Method

    TheoremGraph combines informal theorem-dependency extraction, LeanGraph’s typed declaration graphs, and slogan-embedding links between related statements.

  • Results

    The unified representation yields 47,952 LLM-affirmed cross-formality matches and Recall@10 of 0.775 versus LeanSearch v2’s 0.780 without an LM reranker.

  • Takeaways & Limitations

    The released graphs, extractors, API, and MCP interface provide infrastructure for mathematical search, attribution, and retrieval-augmented reasoning.

  • Takeaways & Limitations

    Cross-formality matching relies on lossy, limited-context slogans, and expert calibration covers only ten pairs, so some affirmed matches may not be ground truth.

Abstract

from arXiv · show

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.

1 Introduction

TheoremGraph addresses the difficulty of tracking fine-grained mathematical dependencies across a vast informal literature and a smaller formalized body. It contributes informal and formal dependency graphs, systematic analyses, a cross-formality bridge, and public programmatic access for search, navigation, and reasoning.

  • Motivation: Contemporary mathematical research typically cites papers rather than the exact lemmas, definitions, or theorems required for proofs.The literature’s scale and specialization make dependency structures difficult to track.
  • Motivation: Formalized mathematics remains much smaller and less comprehensive than informal mathematical knowledge, despite Lean’s rapidly growing library.Lean’s coverage is strongest in foundational and standard undergraduate- and graduate-level mathematics.
  • Contributions: 18.3 million dependencies connect over 11.7 million statements in the informal dependency graph extracted from arXiv and Lean Community.This graph captures dependency structure from informal mathematical sources.
  • Contributions: The formal dependency graph extracts typed declaration-level dependencies from Mathlib4 and several open-source formalization projects.The work collects and analyzes dependency graphs for formalized and informal mathematics.
  • Contributions: 47,952 LLM-affirmed informal–formal matches come from a shared slogan-embedding space, while graph-expanded retrieval comes within 0.5pp of LeanSearch v2’s reranked Recall@10 without a reranker.The project also releases the dependency data publicly and provides API and MCP access for direct querying.

2 Related Work

Related work spans formula-aware mathematical information retrieval, bibliometric graph analysis, neural theorem proving and autoformalization, and dependency extraction for formal libraries. These lines of research motivate representations and tools that capture mathematical structure, retrieval, proof generation, and declaration-level dependencies.

  • Mathematical information retrieval: Early mathematical information retrieval combined formulas with surrounding text, using benchmarks such as NTCIR-11 Math-2, NTCIR-12 MathIR, and ARQMath.This work motivated formula-specific representations and indexing because mathematical meaning depends on symbolic structure and visual layout.
  • Mathematical information retrieval: Learned mathematical retrieval representations include zbMath-BERT, NaturalProofs, and TheoremSearch.These systems extend earlier formula-aware retrieval toward neural representations and retrieval.
  • Bibliometric graph analysis: Bibliometric methods use citation graphs and influence measures to model scholarly relatedness, influence, and field structure.Measures range from citation counts such as the h-index and journal impact factor to recursive prestige models that weight graph structure, recency, or linking behavior.
  • Formal dependency extraction: Formal-library dependency extraction includes raw constant-reference graphs, typed and value-level edges, confidence scores, metadata, visualization, and author-annotated informal-to-formal links.Examples include Jixia, Lean Atlas, and leanblueprint, alongside earlier work on formal dependency extraction.

3 Informal Graph

The informal graph parses 11.7 million theorem-like statements from mathematics arXiv and recovers 18.3 million directed dependency edges within and across papers. Its extraction pipeline combines deterministic, heuristic, and notation-based methods, while retaining extractor labels to support coverage–precision tradeoffs.

  • Corpus and statement extraction: 11.7 million theorem-like statements are parsed from mathematics arXiv papers.The corpus uses mathematics-tagged arXiv papers and stores metadata, resolved references, and LaTeX sources.
  • Dependency extraction: 18.3 million directed dependency edges are recovered within and across papers.The reported edge count covers dependencies extracted from the parsed theorem-like statements.
  • Corpus and statement extraction: The parser identifies theorem-like environments and records statement types, reference numbers, label keys, and bodies.Malformed or implausible statements, including empty bodies, unbalanced math delimiters, very short statements, and statements ending mid-clause, are discarded.
  • Dependency extraction: The pipeline tags each edge by proposing extractor, combining deterministic resolution, backward-constrained heuristics, and notation-based links.The deterministic extractor resolves references within papers and bibliographic keys, while heuristic methods use nearby references, discourse cues, and prose references; the notation extractor links uses to definitions identified by Qwen3-235B-A22B-Instruct-2507.
  • Validation: 98.8% judge-verified precision is achieved by deterministic edges in validation on 500 sampled papers.An independent LLM judge, Kimi K2.5, proposes within-paper dependencies and verifies extractor-proposed edges it initially missed; released edges retain extractor labels.

4 Formal Graph

LeanGraph is a Lean 4 elaborator-level extractor that builds typed declaration-dependency graphs from compiled projects, using post-elaboration constants and proof terms. Across 25 projects it extracts 388,105 declaration nodes and 11,335,708 typed edges, organized into six semantic categories.

  • Scope and scale: 388,105 declaration nodes and 11,335,708 typed edges are extracted across 25 Lean projects, including cross-library dependencies.The Mathlib v4.27–v4.29 graph contributes 351K nodes and 9.3M within-library edges.
  • Scope and granularity: LeanGraph extracts dependencies inside Lean 4 over the kernel Environment API from elaborated, type-checked declarations rather than source text.This exposes post-elaboration constants and proof terms that source-level parsers cannot reliably recover.
  • Edge types: Six edge categories separate structural, type-level, value-level, and documentation-level dependencies: extends, field, sig, proof, def, and docref.They cover inheritance, structure field types, declaration signatures, theorem proof terms, non-Prop definition bodies, and valid docstring references.
  • Node inclusion: User-facing declarations become graph nodes, while kernel-generated artifacts are removed and anonymous instances and tactic objects are retained with metadata.Inclusion follows a structural predicate based on Lean classification APIs and doc-gen4 renderability criteria.

5 Universal Graph

The Universal Graph bridges sparse informal and dense formal dependency graphs by embedding every statement’s slogan in a shared semantic space. Approximate nearest-neighbor retrieval followed by full-precision cosine reranking surfaces cross-graph matches above a fixed threshold.

  • Graph alignment: The informal graph has an edge-to-statement ratio of ∼1.56, versus ∼29.2 for the formal graph, with no initial edges connecting them.The two graphs also differ in representation and density.
  • Slogans: Every statement receives a concise natural-language slogan generated by Qwen3-235B-A22B-Instruct-2507.Informal slogans use an escalating prompt chain that adds context when an earlier attempt is self-flagged as insufficient.
  • Slogans: 11.75M statements achieve full slogan coverage, with 70.3% resolved at the minimal stage and 98.1% before final fallback.The escalation adds statement body, proof and local context, neighboring statements and outgoing dependencies, then a forced best guess.
  • Embeddings: Slogans are embedded in R4096, ℓ2-normalized for cosine similarity, and indexed in pgvector with HNSW plus binary-quantized candidate generation.The embedding model is Qwen3-Embedding-8B with a retrieval instruction.
  • Semantic representation: Retrieval uses binary HNSW for an approximate shortlist, reranks candidates by full-precision cosine similarity, and retains matches above a fixed threshold.Self-retrieval can surface duplicates, while formal-to-informal retrieval can identify semantic restatement edges.

6 Bridging The Corpora

The matching pipeline embeds formal and informal slogans into a shared index, retrieves cross-modal nearest neighbors, and validates candidate counterparts against blueprint annotations. GPT-5.4 then curates high-similarity candidates into a precision-oriented bridge between the two mathematical corpora.

  • Setup: 385,657 formal declarations are searched against informal slogans in a shared index, with ann_k=50 yielding candidates for 55.3% of declarations.Each formal declaration retrieves its single most similar informal slogan by cosine similarity as a candidate match.
  • Setup: 84% and 88% of otherwise-unmatched declarations receive candidates at ann_k=500 and 1000, but only one of 400 deeper probes exceeds 0.85 and none reaches 0.90.The results indicate that missing candidates at ann_k=50 usually reflect the absence of a close informal counterpart rather than limited search depth.
  • Validation: Blueprint partners rank first 43.5% of the time and within the top ten 69.9%, while 65% of high-similarity mismatches are judged matches.Blueprints provide human-written informal statements linked to the Lean declarations they formalize.
  • Judged matches: 47,952 of 100,799 candidates at cosine similarity ≥0.8 are affirmed by GPT-5.4, including 6,353 matches in the ≥0.9 tier, where 87% of candidates are affirmed.The stricter GPT-5.4 set is retained as the curated match collection, while DeepSeek-V4-Pro affirms 61,234 candidates as a higher-recall comparison.
  • Looking to the future: Embedding both graphs into one space turns cosine similarity into a signal for curating links across large, largely disconnected bodies of mathematical writing.The resulting links are intended to provide concrete context for automated formalization systems.

7 Retrieval-Augmented Formalization

This section evaluates retrieval-augmented Lean autoformalization on 24 unseen Mathlib theorems, comparing retrieval, library search, and ungrounded generation. Retrieval raises evaluated correctness while reducing output tokens and tool calls, whereas typechecking alone poorly predicts correctness.

  • Evaluation setup: 24 Mathlib v4.30 theorems are evaluated using retrieval only from the v4.29 corpus to reduce memorization.Queries are name-free qwen3-8b back-translations of gold Lean signatures, and generation allows up to three compiler typecheck calls per target.
  • Evaluation setup: Four conditions compare no retrieval, retrieved premises, full-library grep, and their combination.A hand-checked claude-opus-4-7 judge labels outputs strict when they state the same proposition and evaluated when they are high-confidence equivalent restatements.
  • Results: 5/24 to 8/24: retrieval improves evaluated correctness while using fewer output tokens and tool calls than library search.RAG matches RAG+Library on evaluated correctness while using 14k output tokens and 68 tool calls, versus 37k tokens and 188 calls.
  • Results: 22/24 outputs typecheck without grounding, but only 5/24 are evaluated correct, showing that typechecking alone is not a reliable success signal.About 10/24 targets fail in every condition.

8 Comparison Against Existing Retrieval

Against LeanSearch v2 on MathlibQR, the slogan-only baseline trails because it lacks name and signature information, while adding these representations closes the recall gap without reranking. The improvements are task-specific: they help concept retrieval but hurt chained-premise retrieval on MathlibMPR.

  • Baseline gap: 0.586 Recall@10 / 0.380 nDCG@10 is 7.1pp / 11.4pp behind LeanSearch v2’s retriever-only baseline for the slogan-only system.Both systems use the same frozen Qwen3-Embedding-8B embedder, so the comparison primarily reflects representation and informal-text differences.
  • Representation effects: 0.222 and 0.253 nDCG@10 for Lattice and Functor are the baseline’s weakest categories, compared with 0.477 for theorems.Name-and-signature and related interventions primarily improve structures, classes, definitions, and inductives, while theorem and instance performance declines slightly.
  • Closing the gap: 0.775 Recall@10 versus 0.780 for LeanSearch v2’s reranked system brings the recall-optimized configuration within 0.5pp without a reranker.Configuration E combines slogan and name-and-signature representations with graph expansion, while its nDCG@10 is 0.548 versus 0.623 for the reranked system.
  • Closing the gap: +18.9pp Recall@10 and +16.8pp nDCG@10 are gained over the baseline across the same 810 MathlibQR queries.Graph expansion adds only +0.8pp Recall and −0.2pp nDCG after the name-and-signature representation is present.
  • Transfer limitation: 0.224 to 0.165 group Recall@10 on MathlibMPR shows that the QR-tuned configuration harms chained-premise retrieval relative to the untuned baseline.The paper attributes this limitation to premise lemmas sharing potentially no vocabulary with the theorem, unlike single-declaration concept retrieval.

9 Conclusion

TheoremGraph unifies statement-level dependencies between 11.7M informal arXiv statements and Lean declarations through shared slogan embeddings. The representation supports cross-formality matching and reaches near-parity with LeanSearch v2 on formal concept retrieval without reranking.

  • Contributions: TheoremGraph links 11.7M informal arXiv statements to LeanGraph’s 388,105 declarations across 25 projects through shared slogan embeddings.The Lean graph contains 11.3M typed edges, while the informal graph contains 18.3M edges.
  • Formal concept retrieval: +18.9pp Recall@10 and +16.8pp nDCG@10 improvements were measured over baseline.The bootstrap 95% CIs were [+15.1, +22.7] for Recall@10 and [+13.3, +20.2] for nDCG@10.
  • Formal concept retrieval: 0.775 Recall@10 came within 0.5pp of LeanSearch v2’s reranked 0.780 without an LM reranker.The 0.775 estimate has a bootstrap 95% CI of [0.746, 0.802], containing 0.780.
  • Cross-formality matching: 47,952 cross-formality matches were affirmed above the 0.8 cosine floor, with 87% judge acceptance among candidates at ≥0.9 similarity.Embedding both corpora into one index makes matching a nearest-neighbor query.

10 Limitations … E.3 Related work

TheoremGraph’s evaluations show both promise and important limits: semantic embeddings recover many formal–informal partners, while judge reliability, corpus coverage, and task transfer remain constrained. The paper also extends ingestion beyond arXiv and frames dependency retrieval as a sequential, reinforcement-learned search problem.

  • 10 Limitations: Informal extraction is approximate and arXiv-only, while slogan-based cross-formality matching loses hypotheses, definitions, and unmatched counterparts.The released graph preserves per-extractor labels, but nearest-candidate matching cannot recover results absent from the arXiv corpus.
  • 10 Limitations: 0.224 to 0.165: QR-tuned settings lower MathlibMPR group Recall@10, indicating that concept retrieval and chained-premise retrieval require different signals.Downstream evaluations focus on blueprint pairs, 24 autoformalization targets, and the MathlibQR fair-810 subset.
  • 10 Limitations / Data availability: 23,399 judged candidates are publicly released under open-license restrictions, with non-commercial research gating and CC-BY-NC-SA-4.0 licensing for the project’s contributions.TheoremGraph, LeanGraph, the extractors, HTTP API, MCP interface, and judged matches are released through the stated web and Hugging Face locations.
  • B.3 Open-pool retrieval: 61.2% [58.9, 63.6] of blueprint pairs are recovered by at least one retrieval direction, while 22.3% [20.2, 24.4] are mutual rank-1.Formal-to-informal search covers the full 11.7M-statement informal corpus, whereas informal-to-formal search is restricted to 36,708 project declarations; embeddings outperform BM25 at every cutoff.
  • B.1 Choosing the judge / B.2 Calibrating the judge of record / B.6 Judging breakdown: 8/10 GPT-5.4 verdicts strictly agree with the expert, rising to 9/10 when exact and inexact are collapsed into match versus non-match.The calibration documents scope-direction disagreements and motivates retaining GPT-5.4 as judge of record, while the judging breakdown shows match rates vary by cosine band and judge.
  • B.4 Match types / B.5 Candidate cross-project twins (f →f): 446 [253, 682] cross-project twin pairs sit at cosine ≥0.85, but these candidates are not judge-confirmed; the embedding also surfaces formal–informal and cross-paper match types.Only 14 candidate twins reach cosine ≥0.95 after excluding same-paper matches and parallel-formalization repository pairs.
  • D Extending the Corpus Beyond arXiv: PDF Ingestion: 406 statements are recovered from Artin’s Algebra, including 242 (59.6%) with extracted proofs, but PDF ingestion lacks machine-readable references for deterministic dependency extraction.PDF extraction is source-dependent: it recovers marked numbered environments, while prose definitions and cross-reference structure are incompletely exposed.
  • E.1 Introduction / E.2 Methodology / E.3 Related work: RL training improves the base Qwen3-8B policy but plateaus below Gemini 3.1 Pro and GPT-5.5, despite using six-query dependency-recall evaluation and SDPO-based self-distillation.The related-work framing distinguishes retrieval of dependency edges from proof generation, connects the setup to RL-based agentic search, and motivates graph augmentation through explicit structure.

E.4 Results … F.1 Setup

SDPO improves Qwen3-8B dependency recall but saturates, while cross-paper citation-graph expansion raises recall substantially by recovering dependencies missed by embedding search. The subsequent node-distance analysis samples exact-depth dependency pairs and compares normalized slogan-embedding cosine similarity against random-pair baselines.

  • E.4 Results: 4% to 7.9%: SDPO raises Qwen3-8B dependency recall at k=10 under a six-query budget, then saturates across learning rates and training-set scales.A learning rate of 10−6 reaches 7.9%, while 5×10−6 reaches 7.7%; increasing targets from 1,000 to 5,060 lowers recall to 5.8%.
  • E.4 Results: 7.9% to 13.4%: Cross-paper citation-graph expansion recovers dependencies that embedding search misses by following useful nearby statements.One graph hop can turn a semantic near miss into a true dependency, closing most of the gap to Gemini-3.1-Pro.
  • E.6 Conclusion: The trained policy’s main failure is query precision: it issues plausible topic queries but rarely identifies the exact earlier theorem cited by the proof.GPT-5.5 and Gemini-3.1-Pro retrieve more true dependencies using the same embedding index and comparable query budget.
  • E.5 Discussion: 22.7%: Same-paper expansion reaches higher recall, but cross-paper expansion is more informative because retrieved statements can expose overlapping dependencies.The gain is largest for low-degree targets, where a few good seeds cover much of the dependency set.
  • E.5 Discussion: 5.5 points: Cross-paper graph expansion adds a larger gain than differences within the 6–8% validation band, whose trained-policy validation set has n=150.Expansion also increases the candidate set from roughly 60 to roughly 115 statements, motivating re-ranking.
  • F Node Distance and Embedding Distance: The study tests whether dependency-graph proximity corresponds to greater slogan-embedding similarity by measuring cosine similarity across directed graph distances.Figure 10 reports results for parent-only trajectories.
  • F.1 Setup: 1,000 accepted statement pairs were collected for each formality and depth d using random parent walks whose directed shortest-path distance was exactly d.Each depth was sampled independently, rather than as continuations of the same trajectories.
  • F.1 Setup: Qwen3-8B slogan embeddings were ℓ2-normalized, with cosine similarity computed as their dot product and compared against separate formal and informal random-pair baselines.Error bars are pointwise 95% normal-approximation confidence intervals for mean cosine similarity; each baseline averages 1,000 randomly paired distinct statements.

F.2 Results … G.1 Methodology

The analysis finds that informal statements retain embedding similarity over longer dependency paths than formal statements, while noting sampling and uncertainty limitations. The subsequent literature-search study redacts theorem citations and compares web, dense database, and graph-based retrieval settings.

  • F.2 Results: Cosine similarity declines with directed parent-only distance in both graphs, but the formal graph drops from approximately 0.54 at depth one to the random-pair baseline by depth six.Informal pairs decline from approximately 0.61 at depth one to about 0.51 at depth six, remaining above the corresponding random baseline.
  • F.2 Results: Informal statements retain greater embedding similarity over longer parent-only dependency paths than formal statements.The formal graph’s faster decline may reflect higher local connectivity from fine-grained dependencies on reusable mathematical infrastructure.
  • F.3 Limitations: Depth-specific samples may overrepresent seed statements with rich neighborhoods, longer dependency chains, and reachable embedding-eligible endpoints.The analysis conditions on successful trajectories with usable slogan embeddings and exact directed shortest-path distance d, so samples may not represent all statements at that distance.
  • F.3 Limitations: Pointwise confidence intervals may understate uncertainty because independently sampled depths can reuse seed statements, nodes, and local neighborhoods.The intervals treat observations as independent despite overlap among sampled walks.
  • G In-Context Literature Search: The literature-search task asks models to recover a cited theorem from a local mathematical passage after its citation is removed.This reflects researchers’ need to identify known results from partial descriptions embedded in proofs or exposition.
  • G.1 Methodology: The evaluation sampled 149 redacted passages from mathematics arXiv papers released after February 2026.Recent papers were selected to reduce the likelihood that passages appeared in models’ pretraining data.
  • G.1 Methodology: Each passage replaced a citation to a named result with [Citation Needed], removed its bibliography entry, and preserved the remaining complete bibliography across conditions.Citations referred to theorems, lemmas, propositions, or analogous statements in another arXiv paper.
  • G.1 Methodology: The study compares unrestricted web search, dense retrieval returning the top 10 database candidates per query, and repeated search with dependency-graph navigation.An exact match requires both the correct theorem identifier and the cited paper’s arXiv identifier.

G.2 Results · G.3 Limitations

G.2 finds that graph-based retrieval improves exact-match citation recovery over dense retrieval, but unrestricted web search remains stronger. G.3 qualifies this comparison through uncontrolled search access, unequal interaction budgets, and a narrow 149-example evaluation set.

  • G.2 Results: The evaluation uses 149 redacted arXiv passages, with exact match requiring both the theorem identifier and cited paper arXiv identifier.Paper-level match requires only the correct cited paper.
  • G.2 Results: Graph-based retrieval improves exact-match performance over dense retrieval for all models and improves paper-level retrieval for ChatGPT 5.4 and Gemini 3.1 Pro.Neither database-backed method outperforms unrestricted web search.
  • G.2 Results: Graph navigation provides useful structure beyond dense statement retrieval, but the current interface and agent behavior do not match unrestricted web search.This conclusion follows from the retrieval results despite graph-based gains over dense retrieval.
  • G.2 Results: 0.570 exact-match rate is achieved by Gemini 3.1 Pro with web search, compared with 0.289 under graph-based retrieval.The largest gap between web search and graph-based retrieval occurs for Gemini 3.1 Pro.
  • G.3 Limitations: Web search is not a controlled retrieval comparison because exact-quotation searches may recover the original source paper and directly reveal the redacted citation.Its performance therefore partly reflects access to the original evaluation instance rather than citation inference alone.
  • G.3 Limitations: Repeated retrieval and navigation actions are allowed without matched search budgets, so results combine retrieval quality, agent strategy, stopping behavior, and interface affordances.Dense retrieval returns a fixed top-10 set, whereas graph-based retrieval permits open-ended local navigation.
  • G.3 Limitations: The 149-example evaluation covers only citations explicitly naming theorem-like results in arXiv papers, excluding broader scholarly citation types such as background, methods, attribution, and research lines.The set therefore does not represent the broader range of scholarly citations.
  • G.3 Limitations: Ground-truth citations may not be uniquely mathematically appropriate, since related theorems or alternative supporting sources can be identified while still receiving an incorrect score.This limitation affects interpretation of citation-recovery accuracy.
Loading 2606.25363v1…