Formal-Informal Mathematical Alignment through and beyond Human Annotations
Noah Gießing, Ankit Satpute, Hamid Rahkooy, André Greiner-Petter, Moritz Schubotz
cs.IR
Oct 22, 2026 · v1
TL;DR
Builds a dataset linking Stacks Project tags to Mathlib statements via the @[stacks] attribute, and evaluates LeanSearch retrieval plus LLM judging.
Abstract
Formalized mathematics libraries such as Lean's 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 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-AlignmentProblem
Connections between informal mathematics resources and formal libraries such as Mathlib are sparse and unsystematic. This makes existing formalizations hard to find and reuse.
Approach
The authors extract the 482 expert-annotated @[stacks] attribute links in Mathlib, which point to 325 Stacks Project tags, and assemble them into the SPmathlib dataset. They evaluate LeanSearch retrieval and Qwen-based LLM reranking on recovering these links from informal queries. They then use an LLM-as-judge to classify retrieved candidates (Exact, Generalization, Equivalent, Implies, No, Invalid) as a way to discover unannotated links. The alignments are integrated into the MaRDI knowledge graph.
Results
Reranking improves LeanSearch R@1 from 0.36 to 0.46 and MRR@10 from 0.56 to 0.67. LLM judgments reach about 72–77% accuracy for Exact matches, and accuracy rises with agreement across repeated runs. Generalization and Equivalence judgments remain unreliable, which the authors attribute to unclear rules for what counts as a canonical formalization.
| Method | R@1 | R@5 | R@10 | MRR@10 |
|---|
| LeanSearch | 0.36 | 0.65 | 0.73 | 0.56 |
| LeanSearch (Reranked) | 0.46 | 0.69 | 0.72 | 0.67 |
Retrieval of annotated Stacks–Mathlib links
