Source-linked AI summary
Formal-Informal Mathematical Alignment through and beyond Human Annotations
Noah Gießing, Ankit Satpute, Hamid Rahkooy, André Greiner-Petter, Moritz Schubotz
TL;DR
Connections between informal and formal mathematics libraries are sparse and unsystematic, limiting access to existing formalizations. This paper builds expert-annotated Stacks Project–mathlib links and evaluates retrieval and LLM judging to find additional alignments. Exact-match judgments proved highly reliable in manual review, though broader alignment categories remain less dependable.
Problem
Connections between informal and formal mathematics libraries are sparse and unsystematic, despite the potential value of linking informal statements to existing formalizations.
Source: §1 · p. 1Method
The authors use expert-annotated Stacks Project–mathlib links to evaluate retrieval, LLM reranking, and LLM judging for identifying further alignments.
Source: §1 · pp. 1–2, §4 · p. 3Results
Manual review found 14 of 16 Exact false positives were correct, while LLM judgments for Equivalence and Generalization correlated less well with ground truth.
Source: §4 · p. 3Takeaways & Limitations
Exact judgments can serve as reliable indicators of valid formalizations in this evaluation, while Equivalence and Generalization judgments often require human oversight.
Source: §4 · p. 3
Abstract
from arXiv · showhide
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
1 Introduction
Formal libraries make mathematics machine-verifiable but remain difficult to navigate and write in. This paper links Stacks Project statements to mathlib using expert references and evaluates retrieval and LLM-based methods for finding further alignments.
1 Introduction
- Formal proof assistants provide machine-verifiable definitions, theorems, and proofs, but writing formal mathematics remains difficult and time-consuming.Reusable libraries such as mathlib reduce the detail needed in formal proofs, while their volume and technical content make available material difficult to survey.Source: §1 · p. 1
- Connecting informal statements to formal counterparts could reduce the effort needed to navigate and reuse existing formal libraries.Formal libraries also offer machine-readable, explicit relationships that can support knowledge graphs, while informal links can be difficult to interpret or rely on hallucination-prone language models.Source: §1 · p. 1
- The paper constructs an informal-formal dataset from expert-provided Stacks Project–mathlib connections and evaluates automated retrieval of those links.It investigates LLM-based reranking and judging to improve retrieval and identify previously undiscovered candidate alignments.Source: §1 · pp. 1–2
2 Related Work
Prior aligned corpora commonly translate statements from one modality into another, whereas this work links existing statements from informal and formal libraries using expert annotations. The paper also studies LLM judgments of these cross-library relationships against expert judgments.
Corpora of aligned formal-informal data
- Existing aligned corpora often translate statements from either formal or informal collections, manually or with LLMs, for theorem-proving benchmarks, model training, or retrieval.Datasets formalizing informal statements target problem solving and may not reflect formal-library style; corpora sourced from formal libraries such as HERALD serve training and retrieval.Source: §2 · p. 2
- This work instead links existing statements in informal and formal libraries using expert annotations as ground truth.Its stated aim is closer integration between the two modalities.Source: §2 · p. 2
LLM for formalizations
- The paper investigates LLM judgments of relationships between formal-library items and informal statements in comparison with expert judgments.Prior work has used LLMs to check autoformalized statements, while informal lemma retrieval commonly compares queries with embeddings of informalized mathlib entities.Source: §2 · p. 2
3 Linked Dataset
The authors build SPmathlib from Stacks Project source tags cited by mathlib declarations, then assess retrieval of those links with LeanSearch and an LLM reranker. The dataset covers a small share of mathlib files overall, with greater coverage in relevant subject areas.
3.1 Source and Target Data
- SPmathlib contains 482 mathlib links to 325 Stacks Project tags, found across 209 mathlib files.These links cover about 3% of all files, rising to 22% in Algebraic Geometry and 35% in Field Theory.Source: §3.1 · p. 2
- The source, Stacks Project, is an open-source algebraic geometry textbook organized into 20,950 tags, including lemmas, definitions, sections, and chapters.Mathlib authors can cite those tags using the @[stacks] attribute.Source: §3.1 · p. 2
- LeanSearch informalizes mathlib statements and uses dense passage retrieval to return formal statements matching an informal query.The evaluated reranker asks Qwen3.5-35B-A3B to reason over LeanSearch’s top ten results; matches are assessed by exact statement or shared module file.Source: §3.1 · p. 2
- LeanSearch’s top-ranked result recovers annotated statements in fewer than half of cases, while reranking raises Statement Match R@1 by 28%.Under the relaxed Module Match criterion, more than half of first retrieved results are considered relevant.Source: §3.1 · p. 2, Table 1 · p. 2
4 Expanding the dataset using LLM-as-Judge
LLM-as-Judge can reliably identify exact matches in the evaluated setting, but judgments for equivalence and generalization remain less aligned with expert labels. Applying the method surfaced additional candidate links, while repeated voting improves exact-match automation at added computational cost.
Correctness of baseline evaluations
- Manual review found 14 of 16 LLM Exact false positives were correct, making Exact judgments highly reliable indicators of valid formalizations.The two errors arose from truncated LeanSearch output and were corrected when the full code was supplied; Generalization and Equivalence judgments correlated less well with ground truth.Source: §4 · p. 3
Expanding the dataset
- From 1,810 candidates retrieved for 20,950 unreferenced Stacks statements, the LLM identified 228 Exact matches, with 103 of 108 reviewed formal statements judged accurate.The candidates included 108 formal statements from 67 previously unseen sections and 12 from eight unseen chapters; after correcting five errors, five unseen chapters remained.Source: §4 · p. 3
Increasing certainty through majority voting
- The authors attribute five misclassified statements to randomness rather than systematic error, and report that reprompting or a larger model corrected all five.They propose larger models or majority voting to mitigate such errors, accepting higher computational costs.Source: §4 · p. 3
- Majority voting consistently improves accuracy for Exact and rejection judgments, but gains for Equivalence and Generalization vary across settings.Unanimous agreement can support Exact-match automation at higher cost and with fewer candidates, while high-confidence Equivalence and Generalization judgments often still require human oversight.Source: §4 · p. 3
5 Discussion and Conclusion
The paper places Stacks Project–mathlib links in the MaRDI knowledge graph and discusses how annotation policies affect which formalizations are identified. It also proposes ways to sharpen alignment judgments and outlines validation and future-work directions.
5 Discussion and Conclusion
- Omissions are often accidental, but deliberate choices reflect annotation policies; tendencies toward generalizations and longer proofs have exceptions.Source: §5 · p. 3
- The authors propose canonical-formalization rules or near-duplicate clusters and plan to validate newly found Stacks links with mathlib maintainers.Future work will study the pipeline in other mathlib–informal mathematics link settings.Source: §5 · pp. 3–4
- Table 3 organizes accuracy by agreement threshold, with statement counts in parentheses and default versus reranked rankings in separate blocks.Source: Table 3 · p. 4
- The authors place 482 mathlib–Stacks Project links in MaRDI, alongside links through literature citations and the 1000 theorems project.Source: §5 · p. 4
A Examples
The examples span Exact, Generalization, Equivalent, and partial matches, including retrieved candidates that may be unannotated formalizations. They illustrate how an annotated statement and a retrieved candidate can relate differently to an informal statement.
A Examples
- The examples cover Exact, Generalization, Equivalent, and partial matchings, with two highlighting candidates as potential unannotated formalizations.Source: A Examples · p. 4
- One example labels the annotated statement a Generalization of the informal statement and gives its formal condition.Source: A Examples · p. 4
- A further example states the Stacks Project definition of a quasi-finite ring map using finite type and quasi-finiteness at all primes.Source: A Examples · p. 4
- In another example, the annotated statement is Equivalent to the informal statement, while the retrieved candidate is an Exact match.Source: A Examples · p. 4
- For a local-ring inequality, the annotated lemma proves equality, while the unannotated retrieved statement proves the general inequality.Source: A Examples · p. 5