Mathematical knowledge is significantly divided between bibliographic databases (e.g., MathSciNet, zbMATH Open) and formal proof libraries (e.g., Lean mathlib), hindering unified access to published results and their formalizations. We propose a relational bridge-database that aligns publication metadata with formal artifacts, creating 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. As a feasibility study, we demonstrate how such scores can be estimated via cross-document alignment between informal texts and Lean formalizations, enabling large-scale analysis of formalization coverage.
This framework represents a first step toward integrating bibliographic and formal mathematical ecosystems into scalable, machine-actionable knowledge graphs linking publications to formal proof objects.
Blogger's Review: This research offers a fresh perspective on the formalization of mathematical knowledge. By establishing an interoperability layer, it fosters a connection between literature and formal proofs, greatly enhancing the accessibility and verifiability of knowledge, which may drive further advancements in mathematical research.