TheoremGraph: Brug tussen formele en informele wiskunde

Samenvatting

Wiskundige kennis is georganiseerd rondom beweringen en hun afhankelijkheden, maar deze structuur wordt ongelijkmatig blootgelegd: informele artikelen citeren meestal op documentniveau, terwijl formele bibliotheken fijnmazige afhankelijkheden vastleggen over een veel kleiner deel van de wiskunde. We introduceren TheoremGraph, een uniforme afhankelijkheidsgraaf op beweringniveau die zowel informele als formele wiskunde omvat. Aan de informele kant parsen we 11,7M stellingachtige omgevingen uit wiskunde arXiv en herstellen we 18,3M kandidaat-gerichte afhankelijkheden, elk gelabeld door de extractor die het voorstelde, zodat downstream-gebruikers dekking kunnen inruilen voor precisie. Aan de formele kant brengen we LeanGraph uit, een extractor op elaborator-niveau voor Lean 4 die 388.105 declaratieknooppunten en 11,3M getypte randen produceert in 25 Lean-projecten. We overbruggen de twee grafieken door gegenereerde natuurlijke-taal-slogans in een gedeelde semantische ruimte in te bedden, waardoor gerelateerde beweringen over papers en over de informele/formele kloof heen worden gekoppeld; een LLM-rechter bevestigt 47.952 van dergelijke matches boven een cosinusdrempel van 0,8, waarbij het acceptatiepercentage van de rechter stijgt van 48% over de drempel tot 87% in de >=0,9-categorie. Bij het ophalen van formele concepten blijft onze naam-en-handtekeningrepresentatie met graafuitbreiding binnen 0,5 procentpunt van LeanSearch v2's herschikte Recall@10 (0,775 vs. 0,780) zonder een LM-herschikker. We geven de dataset, extractors, HTTP-API en MCP-interface vrij als infrastructuur voor wiskundig zoeken, bronvermelding en retrieval-augmented reasoning, beschikbaar op theoremsearch.com en 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.