TheoremGraph: Ponte entre Matemática Formal e Informal

Resumo

O conhecimento matemático está organizado em torno de afirmações e suas dependências, mas essa estrutura é exposta de maneira desigual: artigos informais citam principalmente ao nível do documento, enquanto bibliotecas formais registram dependências refinadas sobre um corpo de matemática muito menor. Apresentamos o TheoremGraph, um grafo de dependências unificado a nível de afirmações que abrange tanto a matemática informal quanto a formal. No lado informal, analisamos 11,7 milhões de ambientes semelhantes a teoremas do arXiv de matemática e recuperamos 18,3 milhões de dependências direcionadas candidatas, cada uma rotulada pelo extrator que a propôs, para que usuários downstream possam equilibrar cobertura e precisão. No lado formal, disponibilizamos o LeanGraph, um extrator a nível de elaborador do Lean 4 que produz 388.105 nós de declaração e 11,3 milhões de arestas tipadas em 25 projetos Lean. Estabelecemos uma ponte entre os dois grafos ao incorporar slogans em linguagem natural gerados em um espaço semântico compartilhado, vinculando afirmações relacionadas entre artigos e através da divisão informal/formal; um juiz LLM confirma 47.952 dessas correspondências acima de um limiar de cosseno de 0,8, com a taxa de aceitação do juiz subindo de 48% nesse limiar para 87% no nível >=0,9. Na recuperação de conceitos formais, nossa representação por nome e assinatura com expansão de grafo fica a 0,5 pp do Recall@10 reordenado do LeanSearch v2 (0,775 vs. 0,780) sem um reordenador LM. Disponibilizamos o conjunto de dados, os extratores, a API HTTP e a interface MCP como infraestrutura para busca matemática, atribuição e raciocínio aumentado por recuperação, em theoremsearch.com e 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.