arXiv preprint ·
Formal-Informal Mathematical Alignment through and beyond Human Annotations
- Published
- Source
- arXiv preprint, posted before peer review
- DOI
- 10.1145/3799682.3839951
- Original
- Read it at arXiv
- Topics
Abstract
Formalized mathematics libraries such as Lean's \texttt{mathlib} provide machine-verifiable representations of mathematical knowledge, including definitions, theorems, and their relationships. If effectively connected to informal mathematical resources, formal mathematics could help uncover previously implicit links between mathematical concepts and improve access to existing formalizations. However, connections between informal and formal mathematics libraries are currently sparse and unsystematic. In this paper, we make first strides towards better formal integration. We construct a dataset linking informal statements from the Stacks Project to their formalizations in \texttt{mathlib} by exploiting expert annotations. We evaluate retrieval, LLM-based reranking, and LLM-assisted verification to discover new unannotated informal-to-formal links. To facilitate exploration and reuse of formalized knowledge, we integrated the newly discovered alignments into the MaRDI knowledge graph, enabling mathematicians to find formal counterparts to informal mathematical content. We discuss the difficulties and challenges in using LLMs for linking formal and informal mathematical content. All code and data necessary for reproducing this paper can be found at: https://github.com/AnkitSatpute/Formal-Informal-Mathematical-Alignment
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Information Retrieval
Better Reasoning, Not Just Bigger Models: A Structure-Grounded Framework for Efficient and Reliable Inference
Scaling Graph Query Processing: Focused Exploration on Partitions Using Load Balancing
The Fusion Tax: A Diagnostic Analysis of When Hybrid Retrieval Hurts
From Item Scores to Semantic Tokens: Test-Time Collaborative Adaptation for Generative Recommendation
Compiling Autoregressive LLM Control into Policy-Exact Parallel Inference for Hierarchical RAG
Get the few papers worth your time in Information Retrieval every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.