TheoremGraph: Мост между формальной и неформальной математикой

Аннотация

Математическое знание организовано вокруг утверждений и их зависимостей, однако эта структура раскрывается неравномерно: неформальные статьи ссылаются в основном на уровне документов, тогда как формальные библиотеки фиксируют детализированные зависимости над гораздо меньшим объёмом математики. Мы представляем TheoremGraph — унифицированный граф зависимостей на уровне утверждений, охватывающий как неформальную, так и формальную математику. Со стороны неформальной математики мы разбираем 11,7 млн теоремоподобных окружений из математического раздела arXiv и восстанавливаем 18,3 млн кандидатных направленных зависимостей, каждая из которых помечена экстрактором, предложившим её, чтобы конечные пользователи могли выбирать между широтой охвата и точностью. Со стороны формальной математики мы выпускаем LeanGraph — экстрактор уровня элаборатора Lean 4, который порождает 388 105 узлов-деклараций и 11,3 млн типизированных рёбер из 25 проектов на Lean. Мы связываем оба графа, встраивая сгенерированные слоганы на естественном языке в общее семантическое пространство, объединяя связанные утверждения между статьями и через разрыв неформальной/формальной математики; LLM-судья подтверждает 47 952 таких совпадения при косинусном пороге выше 0,8, при этом доля принятия судьёй возрастает с 48% около порога до 87% на уровне >=0,9. В задаче извлечения формальных понятий наше представление имени и сигнатуры с расширением графа достигает Recall@10, переранжированного в 0,775 против 0,780 у LeanSearch v2, но без LM-реранкера (разница менее 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.