TheoremGraph : Un pont entre les mathématiques formelles et informelles

Résumé

Les connaissances mathématiques sont organisées autour d’énoncés et de leurs dépendances, mais cette structure est exposée de manière inégale : les articles informels citent principalement au niveau du document, tandis que les bibliothèques formelles enregistrent des dépendances à grain fin sur un corpus mathématique beaucoup plus restreint. Nous introduisons TheoremGraph, un graphe de dépendances unifié au niveau des énoncés couvrant à la fois les mathématiques informelles et formelles. Du côté informel, nous analysons 11,7 millions d’environnements de type théorème provenant d’arXiv mathématiques et récupérons 18,3 millions de dépendances candidates dirigées, chacune étiquetée par l’extracteur qui l’a proposée, afin que les utilisateurs avals puissent arbitrer entre couverture et précision. Du côté formel, nous publions LeanGraph, un extracteur au niveau de l’élaborateur Lean 4 produisant 388 105 nœuds de déclaration et 11,3 millions d’arêtes typées dans 25 projets Lean. Nous relions les deux graphes en plongeant des slogans en langage naturel générés dans un espace sémantique partagé, associant ainsi des énoncés apparentés à travers les articles et au-delà de la frontière informel/formel ; un juge LLM valide 47 952 de ces correspondances au-dessus d’un seuil cosinus de 0,8, le taux d’acceptation par le juge passant de 48 % à ce seuil à 87 % dans la tranche >=0,9. Pour la recherche de concepts formels, notre représentation par nom et signature avec expansion de graphe atteint un Recall@10 après reclassement à moins de 0,5 point près de LeanSearch v2 (0,775 contre 0,780), sans reclasseur LM. Nous publions l’ensemble de données, les extracteurs, l’API HTTP et l’interface MCP comme infrastructure pour la recherche mathématique, l’attribution et le raisonnement augmenté par recherche, disponibles sur theoremsearch.com et 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.