Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

• URL: http://arxiv.org/abs/2606.11430v1
• Date: Tue, 09 Jun 2026 20:29:18 GMT
• Title: Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
• Abstract summary: We propose a bridge-Database that aligns publication metadata with formal artifacts.<n>We introduce a paper-level formalization score that measures how much of a publication is covered in formalization.<n>This framework is a first step toward integrating formal mathematical ecosystems into scalable machine-actionable knowledge.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Mathematical knowledge is split between bibliographic databases (e.g., MathSciNet, zbMATH Open) and formal proof libraries (e.g., Lean mathlib), preventing unified access between 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. 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. This framework is a first step toward integrating bibliographic and formal mathematical ecosystems into scalable, machine-actionable knowledge graphs linking publications to formal proof objects.

Related papers

• Does Syntax Matter? A Graph-Augmented Variational Topic Model for Computational Social Sciences [51.56484100374058]
  This paper introduces the Structural Contextual Probabilistic Topic Model ( SCPTM), an architecture that incorporates syntactic dependency relations into topic inference.<n>We evaluate seven topic modeling techniques across four corpora differing in register and discourse structure.<n>Results show that SCPTM's neural architecture yields substantial gains in document-topic alignment over generative baselines.
  arXiv  Detail & Related papers  (2026-09-07T17:39:06Z)
• Multi-agent Autoformalization of Tensor Network Theory [0.21847754147782886]
  We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics.<n>The agents coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously.<n>For some statements, the agents were able to explore new proof routes that are not part of the standard literature.
  arXiv  Detail & Related papers  (2026-07-08T18:43:33Z)
• The MMM Data Model -- A Normative Specification for Knowledge Interoperability in a Decentralisable Knowledge Commons [0.0]
  MMM is a data model for knowledge documentation that emerged from the practical needs of interdisciplinary collaborative research.<n>It combines a small set of normative constraints with the expressive freedom of free-text labels.<n>It is designed for interoperability across disciplines, applications and deployments without requiring semantic convergence.
  arXiv  Detail & Related papers  (2026-06-22T18:24:48Z)
• Lean-GAP: A Dataset of Formalized Graduate Algebra Problems [3.1963549333419388]
  We develop a scalable pipeline consisting of PDF-to-La Algebra preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence.<n>Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process.
  arXiv  Detail & Related papers  (2026-05-20T08:15:43Z)
• ABCD-LINK: Annotation Bootstrapping for Cross-Document Fine-Grained Links [57.514511353084565]
  We introduce a new domain-agnostic framework for selecting a best-performing approach and annotating cross-document links.<n>We apply our framework in two distinct domains -- peer review and news.<n>The resulting novel datasets lay foundation for numerous cross-document tasks like media framing and peer review.
  arXiv  Detail & Related papers  (2025-09-01T11:32:24Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• MLFMF: Data Sets for Machine Learning for Mathematical Formalization [0.18416014644193068]
  MLFMF is a collection of data sets for benchmarking systems used to support formalization of mathematics with proof assistants. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. With more than $250,000$ entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format.
  arXiv  Detail & Related papers  (2023-10-24T17:00:00Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  Autoformalization is the task of translating natural language mathematics into a formal language that can be verified by a program. Research paper mathematics requires large amounts of background and context. We propose an avenue towards tackling autoformalization for research-level mathematics, by breaking the task into easier and more approachable subtasks.
  arXiv  Detail & Related papers  (2023-10-12T00:50:24Z)
• Scientific Paper Extractive Summarization Enhanced by Citation Graphs [50.19266650000948]
  We focus on leveraging citation graphs to improve scientific paper extractive summarization under different settings. Preliminary results demonstrate that citation graph is helpful even in a simple unsupervised framework. Motivated by this, we propose a Graph-based Supervised Summarization model (GSS) to achieve more accurate results on the task when large-scale labeled data are available.
  arXiv  Detail & Related papers  (2022-12-08T11:53:12Z)
• Integrating Semantics and Neighborhood Information with Graph-Driven Generative Models for Document Retrieval [51.823187647843945]
  In this paper, we encode the neighborhood information with a graph-induced Gaussian distribution, and propose to integrate the two types of information with a graph-driven generative model. Under the approximation, we prove that the training objective can be decomposed into terms involving only singleton or pairwise documents, enabling the model to be trained as efficiently as uncorrelated ones.
  arXiv  Detail & Related papers  (2021-05-27T11:29:03Z)
• Enhancing Scientific Papers Summarization with Citation Graph [78.65955304229863]
  We redefine the task of scientific papers summarization by utilizing their citation graph. We construct a novel scientific papers summarization dataset Semantic Scholar Network (SSN) which contains 141K research papers in different domains. Our model can achieve competitive performance when compared with the pretrained models.
  arXiv  Detail & Related papers  (2021-04-07T11:13:35Z)
• Leveraging Graph to Improve Abstractive Multi-Document Summarization [50.62418656177642]
  We develop a neural abstractive multi-document summarization (MDS) model which can leverage well-known graph representations of documents. Our model utilizes graphs to encode documents in order to capture cross-document relations, which is crucial to summarizing long documents. Our model can also take advantage of graphs to guide the summary generation process, which is beneficial for generating coherent and concise summaries.
  arXiv  Detail & Related papers  (2020-05-20T13:39:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.