TheoremGraph：连接形式化与非形式化数学

摘要

数学知识围绕陈述及其依赖关系组织，但这种结构的呈现并不均匀：非正式论文大多在文档层面进行引用，而形式化库则记录更小数学领域的细粒度依赖关系。我们引入TheoremGraph，这是一种统一的陈述级依赖关系图，涵盖非正式和形式化数学。在非正式方面，我们解析了来自数学arXiv的1170万个类定理环境，恢复了1830万个候选有向依赖关系，每个依赖关系由提出它的提取器标记，以便下游用户可以根据需要权衡覆盖率和精确度。在形式化方面，我们发布了LeanGraph，这是一个Lean 4细化器级别提取器，在25个Lean项目中生成了388,105个声明节点和1130万个类型化边。我们通过将生成的自然语言标语嵌入到共享语义空间中，将这两个图桥接起来，连接论文之间以及非正式/形式化边界上的相关陈述；一个LLM评估器确认了47,952个这样的匹配，其余弦下限为0.8，评估器接受率从0.8下限处的48%上升到>=0.9级别的87%。在形式化概念检索方面，我们的名称-签名表示结合图展开，在没有LM重新排序器的情况下，其Recall@10（0.775 vs 0.780）与LeanSearch v2的重新排序结果相差不到0.5个百分点。我们将数据集、提取器、HTTP API和MCP接口作为数学搜索、归因和检索增强推理的基础设施发布，可在theoremsearch.com和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.