Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
arXiv:2606.11430
The paper proposes a relational bridge database that links bibliographic metadata with formal proof libraries and introduces a formalization score to estimate how much of a publication is covered by formal systems.
Abstract
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.