TheoremGraph: Brückenschlag zwischen formaler und informeller Mathematik

Zusammenfassung

Mathematisches Wissen ist um Aussagen und deren Abhängigkeiten herum organisiert, aber diese Struktur wird ungleichmäßig offengelegt: Informelle Arbeiten zitieren meist auf Dokumentebene, während formale Bibliotheken feinkörnige Abhängigkeiten über einen viel kleineren Korpus der Mathematik erfassen. Wir stellen TheoremGraph vor, einen einheitlichen Abhängigkeitsgraphen auf Aussagenebene, der sowohl informelle als auch formale Mathematik umfasst. Auf der informellen Seite parsen wir 11,7 Millionen satzartige Umgebungen aus dem Mathematik-ArXiv und gewinnen 18,3 Millionen Kandidaten für gerichtete Abhängigkeiten, jede gekennzeichnet durch den Extraktor, der sie vorgeschlagen hat, sodass nachgelagerte Nutzer Abdeckung gegen Präzision abwägen können. Auf der formellen Seite veröffentlichen wir LeanGraph, einen Extraktor auf Elaborator-Ebene für Lean 4, der 388.105 Deklarationsknoten und 11,3 Millionen typisierte Kanten über 25 Lean-Projekte hinweg erzeugt. Wir überbrücken die beiden Graphen, indem wir generierte natürlichesprachliche Slogans in einen gemeinsamen semantischen Raum einbetten und so zusammenhängende Aussagen über Arbeiten hinweg und über die informelle/formelle Kluft hinweg verknüpfen; ein LLM-Richter bestätigt 47.952 solcher Übereinstimmungen oberhalb einer Kosinus-Schwelle von 0,8, wobei die Akzeptanzrate des Richters von 48% über die Schwelle hinweg auf 87% in der >=0,9-Stufe ansteigt. Bei der formalen Konzeptabfrage liegt unsere Darstellung aus Name und Signatur mit Grapherweiterung innerhalb von 0,5 Prozentpunkten an LeanSearch v2s neu geranktem Recall@10 (0,775 gegenüber 0,780) ohne einen LM-Reranker. Wir veröffentlichen den Datensatz, die Extraktoren, die HTTP-API und die MCP-Schnittstelle als Infrastruktur für mathematische Suche, Attribution und retrieval-gestütztes Denken, verfügbar unter theoremsearch.com und huggingface.co/datasets/uw-math-ai/theorem-matching.

English

Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.