Math-Graph ist ein Datensatz mathematischer Theorem-Abhängigkeitsgraphen, der 2026 vom Labor für Mathematische Künstliche Intelligenz der Universität Washington veröffentlicht wurde. Er erstellt einen detaillierten, auf Aussagenebene aufgelösten mathematischen Theorem-Abhängigkeitsgraphen. Zugehörige Veröffentlichungen umfassen… TheoremGraph: Die Brücke zwischen formaler und informeller Mathematik . Dieser Datensatz enthält 47.952 Paare informeller und formaler mathematischer Aussagen und integriert die beiden Arten mathematischen Wissens in einen kohärenten Abhängigkeitsgraphen, der sowohl informelle als auch formale Mathematik abdeckt. Er umfasst Metadaten von Publikationen, mathematische Aussagen (formal/informell), Abhängigkeitskanten und LLM-generierte natürlichsprachliche Beschreibungen.

Zusammensetzung des Datensatzes:

• Informeller Graph (arXiv): Enthält 11,7 Millionen Aussageknoten und 18,3 Millionen Abhängigkeitskanten und unterstützt verschiedene Methoden zur Extraktion von Abhängigkeiten: deterministische Regeln, Heuristiken, symbolisches Schließen und LLM usw.
• Formaler Graph (LeanGraph): Enthält 388.000 Lean 4-Deklarationsknoten und 11,3 Millionen typisierte Abhängigkeitskanten, die 25 Projekte einschließlich Mathlib abdecken.

Datenfelder:

• paper_arxiv.csv: arXiv-Paper-Metadaten, einschließlich ID, Titel, Autor, Kategorie, Lizenz, Link usw.
• paper_lean_community.csv / paper_lean_repo.csv: Metadaten des Lean-Projekts, einschließlich ID, Titel, Autor, Kategorie, Lizenz, Link usw.
• statement_informal.csv / statement_formal.csv: Felder für Inhalt, Typ, Ort, Kontext und Lizenzgateway der Anweisung/Deklaration.
• informal_dependency.csv / formal_dependency.csv: Gerichtete Abhängigkeiten zwischen Anweisungen, Extraktionsmethoden, Typen und Referenzorten.
• slogan.csv: Speichert den Slogan in natürlicher Sprache, die Prompt-Wort-Version, die Modellkonfiguration und den Tokenverbrauch für jede Anweisung.

Zitat

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