Formal-Informal Mathematical Alignment through and beyond Human Annotations

Overview & Synopsis

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