TheoremGraph: 形式的数学と非形式的数学の橋渡し

要旨

数学的知識は命題とその依存関係に基づいて整理されるが、この構造は非一様にしか表面化されていない。すなわち、非形式的な論文は主に文献レベルで引用を行う一方、形式的なライブラリははるかに小規模な数学体系に対して細粒度の依存関係を記録している。本稿では、非形式的数学と形式的数学の両方にまたがる統一的な文レベルの依存グラフであるTheoremGraphを導入する。非形式的側面として、数学arXivから1170万件の定理類似環境を解析し、1830万件の候補となる有向依存関係を抽出する。各関係はそれを提案した抽出器でラベル付けされ、下流の利用者がカバレッジと精度をトレードオフできるようになっている。形式的側面として、Lean 4のエラボレータレベルで抽出を行うLeanGraphを公開する。これは25件のLeanプロジェクトから38万8105個の宣言ノードと1130万本の型付きエッジを生成する。さらに、生成された自然言語によるスローガンを共有意味空間に埋め込むことで、両グラフを橋渡しし、論文をまたいだ関連記述や非形式的／形式的な区分を超えた関連記述をリンクする。LLM判定器により、コサイン類似度0.8以上の閾値において4万7952件のマッチが確認され、判定器の受入率は0.8台で48%から0.9以上で87%に上昇する。形式的な概念検索において、グラフ拡張を伴う名称とシグネチャ表現は、LM再ランカーを用いずにLeanSearch v2の再ランク後Recall@10と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.