Math-Graphは、ワシントン大学数理人工知能研究所が2026年に公開した、数学定理の依存関係グラフのデータセットです。これは、ステートメントレベルのきめ細かい数学定理の依存関係グラフを構築します。関連論文には、以下のようなものがあります。 TheoremGraph：形式数学と非形式数学の橋渡し 。 このデータセットには、非公式な数学的記述と公式な数学的記述のペアが47,952組含まれており、非公式な数学と公式な数学の両方を網羅する一貫性のある依存関係グラフに、2種類の数学的知識が統合されています。これには、論文のメタデータ、数学的記述（公式／非公式）、依存関係のエッジ、およびLLMによって生成された自然言語による説明が含まれます。

データセットの構成：

• 非公式グラフ（arXiv）：1170万個のステートメントノードと1830万個の依存関係エッジを含み、決定論的ルール、ヒューリスティクス、記号推論、LLMなど、さまざまな依存関係抽出方法をサポートします。
• 形式グラフ（LeanGraph）：388,000個の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: 各ステートメントについて、自然言語のスローガン、プロンプトワードのバージョン、モデル構成、およびトークン消費量を記録します。

引用

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