Math-Graph 是由华盛顿大学数学人工智能实验室于 2026 年发布的数学定理依赖图数据集，构建了一个语句级粒度的数学定理依赖图，相关论文成果为 TheoremGraph: Bridging Formal and Informal Mathematics 。 该数据集包含 47,952 条非形式化与形式化数学的语句匹配对，将两类数学知识整合为一张连贯的依赖图，覆盖非形式化（informal）与形式化（formal）数学，涵盖论文元数据、数学语句（形式/非形式）、依赖关系边以及 LLM 生成的自然语言描述数据。

数据集构成:

• 非形式化图（arXiv）：包含 1,170 万个语句节点与 1,830 万条依赖边，支持多种依赖提取方法：确定性规则、启发式、符号推理及 LLM 等
• 形式化图（LeanGraph）：包含 38.8 万个 Lean 4 声明节点与 1,130 万条类型化依赖边，覆盖 Mathlib 等 25 个项目

数据字段:

• paper_arxiv.csv ：arXiv 论文元数据，包括 ID 、标题、作者、类别、许可证、链接等
• paper_lean_community.csv / paper_lean_repo.csv：Lean 项目元数据，包括 ID 、标题、作者、类别、许可证、链接等
• statement_informal.csv / statement_formal.csv：语句/声明内容、类型、位置、上下文及许可证门控字段
• informal_dependency.csv / formal_dependency.csv：语句间的有向依赖关系、提取方法、类型及引用位置
• slogan.csv：记录每条语句对应的自然语言标语、提示词版本、模型配置及 Token 消耗情况

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}
}