Math-Graph is a dataset of mathematical theorem dependency graphs released in 2026 by the Mathematical Artificial Intelligence Laboratory at the University of Washington. It constructs a statement-level granular mathematical theorem dependency graph. Related papers include... TheoremGraph: Bridging Formal and Informal Mathematics . This dataset contains 47,952 pairs of informal and formal mathematical statements, integrating the two types of mathematical knowledge into a coherent dependency graph that covers both informal and formal mathematics. It includes paper metadata, mathematical statements (formal/informal), dependency edges, and LLM-generated natural language descriptions.

Dataset composition:

• Informal graph (arXiv): Contains 11.7 million statement nodes and 18.3 million dependency edges, supporting various dependency extraction methods: deterministic rules, heuristics, symbolic reasoning, and LLM, etc.
• Formal Graph (LeanGraph): Contains 388,000 Lean 4 declaration nodes and 11.3 million typed dependency edges, covering 25 projects including Mathlib.

Data fields:

• paper_arxiv.csv: arXiv paper metadata, including ID, title, author, category, license, link, etc.
• paper_lean_community.csv / paper_lean_repo.csv: Lean project metadata, including ID, title, author, category, license, link, etc.
• statement_informal.csv / statement_formal.csv: Statement/declaration content, type, location, context, and license gate fields.
• informal_dependency.csv / formal_dependency.csv: Directed dependencies between statements, extraction methods, types, and reference locations.
• slogan.csv: Records the natural language slogan, prompt word version, model configuration, and token consumption for each statement.

Citation

@misc{kurgan2026theoremgraph,
title         = {TheoremGraph: Bridging Formal and Informal Mathematics},
author        = {Kurgan, Simon and Wang, Evan and Leonen, Eric and Szeto, Sophie and
Alexander, Luke and Remizov, Artemii and Alper, Jarod and
Inchiostro, Giovanni and Ilin, Vasily},
year          = {2026},
eprint        = {2606.25363},
archivePrefix = {arXiv},
primaryClass  = {cs.IR},
url           = {https://arxiv.org/abs/2606.25363}
}