TheoremGraph：连接正式和非正式数学

数学知识是围绕陈述及其依赖关系组织的，但这种结构暴露得不均匀：非正式论文主要在文档级别进行引用，而正式图书馆则记录了规模小得多的数学主体的细粒度依赖关系。我们引入了 TheoremGraph，一个涵盖非正式和形式数学的统一语句级依赖图。在非正式方面，我们从数学 arXiv 解析 1170 万个类似定理的环境，并恢复 1830 万个候选定向依赖项，每个依赖项都由提出它的提取器标记，以便下游用户可以用覆盖率换取精度。在正式方面，我们发布了 LeanGraph，这是一个 Lean 4 精炼者级提取器，在 25 个精益项目中生成 388,105 个声明节点和 1130 万条类型边。我们通过将生成的自然语言口号嵌入到共享语义空间中，跨论文和跨非正式/正式鸿沟链接相关语句来连接这两个图； LLM 法官在 0.8 余弦下限之上确认了 47,952 个此类匹配，法官接受率从整个下限的 48% 上升到 >=0.9 层的 87%。在正式概念检索中，我们的带有图形扩展的名称和签名表示与 LeanSearch v2 的重新排名 Recall@10（0.775 与 0.780）相比，在没有 LM 重新排名器的情况下相差不到 0.5pp。我们发布了数据集、提取器、HTTP API 和 MCP 接口，作为数学搜索、归因和检索增强推理的基础设施，可在 theoremsearch.com 和 Huggingface.co/datasets/uw-math-ai/theorem-matching 上获取。