TheoremGraph：連接形式化與非形式化數學

摘要

數學知識圍繞著陳述及其依賴關係組織，但這種結構的呈現並不均勻：非正式論文大多在文檔層級進行引用，而形式化函式庫則針對範圍小得多的數學內容記錄了細粒度的依賴關係。我們提出TheoremGraph，一個統一的、涵蓋非正式與形式化數學的陳述層級依賴關係圖。在非正式方面，我們從數學arXiv解析出1170萬個類似定理的環境，並恢復了1830萬條候選有向依賴關係，每條都標註了提出該關係的提取器，以便下游使用者在覆蓋率與精確度之間進行權衡。在形式化方面，我們發布LeanGraph，一個Lean 4的編譯器層級提取器，從25個Lean專案中產生了388,105個宣告節點與1130萬條帶型別的邊。我們透過將生成的自然語言口號嵌入到共享語意空間中，將兩個圖橋接起來，連結跨論文以及跨非正式/形式化鴻溝的相關陳述；LLM評審在餘弦值下限0.8以上確認了47,952個這類匹配，且評審接受率從下限處的48%上升至≥0.9層級的87%。在形式化概念檢索方面，我們的名稱與簽名表示法結合圖擴展，在無需語言模型重排序器的情況下，在Recall@10指標上與LeanSearch v2的重排序版本相差不到0.5個百分點（0.775對比0.780）。我們發布了資料集、提取器、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.