TheoremGraph: 형식 수학과 비형식 수학의 연결

초록

수학적 지식은 명제들과 그 의존성들을 중심으로 조직되지만, 이러한 구조는 고르게 드러나지 않는다. 비형식 논문은 대개 문서 수준에서 인용하는 반면, 형식 라이브러리는 훨씬 적은 양의 수학에 대해 세분화된 의존성을 기록한다. 우리는 비형식 수학과 형식 수학을 모두 아우르는 통합된 명제 수준 의존성 그래프인 TheoremGraph를 소개한다. 비형식 측면에서는 수학 arXiv에서 1170만 개의 정리류 환경을 구문 분석하고 1830만 개의 후보 방향성 의존성을 복원하며, 각 의존성은 이를 제안한 추출기로 레이블링되어 하위 사용자가 범위와 정밀도를 절충할 수 있게 한다. 형식 측면에서는 Lean 4 정교화기 수준 추출기인 LeanGraph를 공개하며, 25개의 Lean 프로젝트에 걸쳐 388,105개의 선언 노드와 1130만 개의 타입 엣지를 생성한다. 우리는 생성된 자연어 슬로건을 공유된 의미 공간에 임베딩하여 두 그래프를 연결하며, 이는 논문 간 및 비형식/형식 경계를 넘어 관련 명제들을 연결한다. LLM 판정기는 코사인 하한 0.8 이상에서 47,952개의 일치를 확인하며, 판정기 수용률은 하한에서 48%에서 0.9 이상 구간에서 87%로 상승한다. 형식 개념 검색에서 우리의 이름-시그니처 표현과 그래프 확장은 언어모델 재순위화기 없이 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.