Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

Technical Summary: Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

Problem Statement
Modern mathematical knowledge is currently fragmented across two structurally independent infrastructures. On one side, bibliographic databases such as MathSciNet and zbMATH Open index the human-readable research record, capturing publication metadata, citation networks, and expert reviews. On the other side, formal proof libraries (e.g., Lean's mathlib) and interactive theorem provers (ITPs) encode machine-verifiable mathematics as formally checked objects. While these ecosystems are complementary, they remain disconnected: bibliographic systems do not indicate whether results have been formalized, and formal libraries are organized around internal dependency graphs rather than publication metadata. Although "alignment artifacts" (such as survey papers or documentation) exist to map classical results to mechanized developments, these mappings are fragmented, non-standardized, and not systematically integrated into a queryable layer.

Methodology
The paper proposes a relational bridge-database designed to integrate these existing infrastructures without replacing them. The core methodology involves three components:

1. Architectural Integration: The system acts as an alignment infrastructure that links bibliographic records (from MathSciNet and zbMATH Open) with formal artifacts (from Lean, Reservoir, etc.). It does not perform new peer review or formal verification but serves as an archival platform that records correspondences between publications and formal code.
2. Formalization Scoring ($S(P_i)$): The authors define a quantitative metric to measure the extent of formalization for a specific paper $P_i$.
   • The paper is treated as a collection of mathematical statements $S_i$ (definitions, lemmas, theorems, conjectures, etc.).
   • A binary indicator $\phi(s)$ is assigned to each statement $s$: 1 if fully formalized in Lean, 0 otherwise.
   • Distinction in Requirements:
     • Pure statements (definitions, constructions, conjectures) require only the existence of the formal object.
     • Proved statements (theorems, lemmas) require both the formal statement and a complete formal proof.
   • The score is calculated as: $S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$.
3. Feasibility Study via Cross-Document Alignment: To demonstrate that these scores can be estimated at scale, the authors utilized Large Language Models (LLMs) in a zero-shot setting. The model was tasked with comparing an informal mathematical paper (PDF 1) against a formalization document or Lean implementation (PDF 2). The model was instructed to:
   • Extract granular mathematical statements from the informal text.
   • Classify them as "Pure" or "Proved."
   • Identify semantic correspondences in the formal text.
   • Compute the formalization score based on the ratio of matched statements.

Key Contributions

• Interoperability Layer: A proposal for a database that unifies bibliographic registries with formal verification environments, linking publication metadata to formal code repositories.
• Formalization Score Definition: A rigorous, paper-level metric ($S(P_i)$) that quantifies the coverage of a publication within formal systems, distinguishing between the existence of definitions and the presence of proofs.
• Feasibility Demonstration: A proof-of-concept study showing that LLMs can successfully estimate these scores by aligning informal texts with formal artifacts, enabling large-scale analysis of formalization coverage.

Experimental Results
The authors conducted experiments on six mathematical papers using Google Gemini without fine-tuning. The results demonstrated the system's ability to distinguish between varying degrees of formalization:

• High Coverage: The sphere packing problem in dimension 8 received a score of 100, indicating full formalization.
• Partial Coverage: Papers on the irrationality of $\zeta(3)$ and multi-graded Proj schemes received scores of 50 and 67.74 (and 96.30 in a second experiment), reflecting substantial but incomplete formalization.
• Low/No Coverage: A paper on "Dilatations of categories" received 41.67, and a survey on "Algebraic magnetism" (which had no Lean implementation) received 0 when matched against unrelated documentation.
• The experiments confirmed that the model could correctly identify when no relevant formalization existed and could differentiate between fully and partially formalized works.

Significance and Claims
The paper positions this work as a first step toward integrating bibliographic and formal mathematical ecosystems into scalable, machine-actionable knowledge graphs. The authors explicitly state that the proposed system is not a replacement for existing publication or verification infrastructures. Instead, it serves as a "connective layer" that systematizes existing, informal alignment knowledge into a structured, queryable resource.

The significance lies in the ability to:

1. Provide unified access to published results and their formal counterparts.
2. Enable large-scale analysis of how much of the mathematical literature has been formalized.
3. Create a foundation for linking publications to formal proof objects, potentially supporting future AI-generated mathematics and human-AI hybrid workflows.

The authors acknowledge limitations, noting that PDF parsing introduces ambiguity, retrieval quality affects scoring accuracy, and LLMs may produce spurious correspondences. Consequently, they frame the system as a "best-effort framework" for relational alignment rather than a perfectly faithful mapping, with the expectation that hyperlinks and mappings will eventually be curated manually or via supervised processes similar to current bibliographic practices.