建立数学文献与形式化证明的桥梁，实现知识互通。
Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
- 构建关联文献与形式化代码的桥梁数据库。
- 提出论文级形式化评分与验证状态分类体系。
- 支持大规模分析数学成果的形式化覆盖情况。
数学知识分散在文献数据库（如 MathSciNet、zbMATH Open）和形式化证明库（如 Lean 的 mathlib）中，导致难以统一获取已发表结果及其形式化版本。本文提出一种关系型桥接数据库，将出版元数据与形式化产物对齐，实现数学文献与机器可验证证明之间的互操作性。引入论文级形式化评分，衡量一篇论文在形式系统中的覆盖程度，并提供正确性档案，记录每条印刷命题的验证状态：已认证、已修正、未修正、待解决或未测试。作为可行性研究，我们展示了如何通过非形式化文本与 Lean 形式化间的跨文档对齐估算这些评分，支持大规模形式化覆盖率分析。进一步提出具体构建路径：基于异构形式化产物的多源评分机制、支持作者直接提交的智能收集流程、算法与人工双重验证策略，以及面向索引数学的整体形式化评分。该框架是整合文献与形式化数学生态系统的一步。
原文摘要 · Abstract (English)
Mathematical knowledge is split between bibliographic databases (e.g., MathSciNet, zbMATH Open) and formal proof libraries (e.g., Lean's mathlib), preventing unified access to published results and their formalizations. We propose a relational bridge-database that aligns publication metadata with formal artifacts, providing an interoperability layer between mathematical literature and machine-verifiable proofs. We introduce a paper-level formalization score that measures how much of a publication is covered in formal systems, together with a correctness profile recording what machine verification has established about each printed statement: certified, corrected, uncorrected, open, or untested. As a feasibility study, we show how such scores can be estimated via cross-document alignment between informal texts and Lean formalizations, enabling large-scale analysis of formalization coverage. We further outline a concrete construction pathway: multi-source scoring over heterogeneous formalization artifacts, an agentic collection workflow with direct author submission, a dual validation policy, algorithmic then human, and a global formalization score of indexed mathematics. This framework is a step toward integrating bibliographic and formal mathematical ecosystems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。