Math-Graph est un ensemble de données de graphes de dépendance de théorèmes mathématiques, publié en 2026 par le Laboratoire d'intelligence artificielle mathématique de l'Université de Washington. Il construit un graphe de dépendance de théorèmes mathématiques granulaire au niveau des énoncés. Parmi les articles connexes, on peut citer… TheoremGraph : Un pont entre les mathématiques formelles et informelles . Cet ensemble de données contient 47 952 paires d'énoncés mathématiques formels et informels, intégrant les deux types de connaissances mathématiques dans un graphe de dépendances cohérent qui couvre à la fois les mathématiques formelles et informelles. Il comprend les métadonnées des articles, les énoncés mathématiques (formels/informels), les arêtes de dépendance et les descriptions en langage naturel générées par LLM.

Composition de l'ensemble de données :

• Graphe informel (arXiv) : Contient 11,7 millions de nœuds d’instructions et 18,3 millions d’arêtes de dépendance, prenant en charge diverses méthodes d’extraction de dépendances : règles déterministes, heuristiques, raisonnement symbolique et LLM, etc.
• Graphe formel (LeanGraph) : Contient 388 000 nœuds de déclaration Lean 4 et 11,3 millions d’arêtes de dépendance typées, couvrant 25 projets, dont Mathlib.

Champs de données :

• paper_arxiv.csv : métadonnées des articles arXiv, y compris l’identifiant, le titre, l’auteur, la catégorie, la licence, le lien, etc.
• paper_lean_community.csv / paper_lean_repo.csv : Métadonnées du projet Lean, y compris l’identifiant, le titre, l’auteur, la catégorie, la licence, le lien, etc.
• statement_informal.csv / statement_formal.csv : Contenu, type, emplacement, contexte et champs de licence des déclarations.
• informal_dependency.csv / formal_dependency.csv : Dépendances dirigées entre les instructions, les méthodes d’extraction, les types et les emplacements de référence.
• slogan.csv : Enregistre le slogan en langage naturel, la version du mot d’invite, la configuration du modèle et la consommation de jetons pour chaque énoncé.

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