# Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

arXiv: https://arxiv.org/abs/2606.11430 · HTML: https://mlsanity.com/paper/2606.11430/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 32 references that are in the map.
- First posted on arXiv 9 Jun 2026.

## Builds on (most cited first, 8 of 8)

- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs](https://mlsanity.com/paper/2511.18760/) (2025)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [Formalizing multi-graded Brenner-Schr"oer Proj schemes and dilatations of rings in Lean4](https://mlsanity.com/paper/2606.01438/) (2026)
- [A Formal Proof of the Irrationality of zeta(3)](https://mlsanity.com/paper/1912.06611/) (2019)
- [The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction](https://mlsanity.com/paper/2509.15116/) (2025)
- [Formalizing all indexed mathematics as a benchmark for general reasoning, with the example of implementing dilatations of categories](https://mlsanity.com/paper/2606.03835/) (2026)

## Abstract (arXiv)

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.