TheoremGraph: Puente entre las matemáticas formales e informales

Resumen

El conocimiento matemático se organiza en torno a enunciados y sus dependencias, pero esta estructura se expone de manera desigual: los artículos informales citan principalmente a nivel de documento, mientras que las bibliotecas formales registran dependencias detalladas sobre un cuerpo de matemáticas mucho más reducido. Introducimos TheoremGraph, un grafo de dependencias unificado a nivel de enunciado que abarca tanto las matemáticas informales como las formales. En el lado informal, analizamos 11,7 millones de entornos similares a teoremas del arXiv de matemáticas y recuperamos 18,3 millones de dependencias dirigidas candidatas, cada una etiquetada por el extractor que la propuso, para que los usuarios posteriores puedan intercambiar cobertura por precisión. En el lado formal, publicamos LeanGraph, un extractor a nivel de elaborador de Lean 4 que produce 388.105 nodos de declaración y 11,3 millones de aristas tipadas en 25 proyectos de Lean. Unimos ambos grafos incrustando eslóganes generados en lenguaje natural en un espacio semántico compartido, vinculando enunciados relacionados entre artículos y a través de la división informal/formal; un juez LLM afirma 47.952 coincidencias de este tipo por encima de un umbral de coseno de 0,8, con una tasa de aceptación del juez que aumenta del 48% en todo el umbral al 87% en el nivel >=0,9. En la recuperación de conceptos formales, nuestra representación de nombre y firma con expansión de grafo se sitúa a menos de 0,5 puntos porcentuales del Recall@10 reordenado de LeanSearch v2 (0,775 frente a 0,780) sin un reordenador de modelo de lenguaje. Publicamos el conjunto de datos, los extractores, la API HTTP y la interfaz MCP como infraestructura para búsqueda matemática, atribución y razonamiento aumentado por recuperación, disponibles en theoremsearch.com y 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.