在数学知识领域，文献数据库（如 MathSciNet 和 zbMATH Open）与形式化证明库（如 Lean mathlib）之间存在显著分隔，导致无法统一访问已发布的结果及其形式化版本。为此，我们提出了一种关系桥接数据库，旨在将出版元数据与形式化文献对齐，从而提供一个数学文献与可机器验证证明之间的互操作层。
我们引入一种论文级形式化得分，用以衡量出版物在形式化系统中的覆盖程度。作为可行性研究，我们展示了如何通过非正式文本与 Lean 形式化之间的跨文档对齐来估算此类得分，从而实现对形式化覆盖范围的大规模分析。
该框架是将文献和形式化数学生态系统整合为可扩展的机器可操作知识图谱的第一步，能够将出版物与形式证明对象链接起来。
博主点评： 这项研究为数学知识的形式化提供了新的视角，通过构建互操作层，促进了文献与形式化证明之间的连接，极大地提升了知识的可获取性与可验证性，未来或将推动数学研究的进一步发展。