# GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research

arXiv: https://arxiv.org/abs/2609.36663 · HTML: https://mlsanity.com/paper/2609.36663/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 35 of its 46 references that are in the map.
- First posted on arXiv 29 Sep 2026.

## Builds on (most cited first, 30 of 35)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Language Generation in the Limit](https://mlsanity.com/paper/2404.06757/) (2024)
- [Generation through the lens of learning theory](https://mlsanity.com/paper/2410.13714/) (2024)
- [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://mlsanity.com/paper/2403.13312/) (2024)
- [Exploring Facets of Language Generation in the Limit](https://mlsanity.com/paper/2411.15364/) (2024)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [Density Measures for Language Generation](https://mlsanity.com/paper/2504.14370/) (2025)
- [Generation from Noisy Examples](https://mlsanity.com/paper/2501.04179/) (2025)
- [Representative Language Generation](https://mlsanity.com/paper/2505.21819/) (2025)
- [On Union-Closedness of Language Generation](https://mlsanity.com/paper/2506.18642/) (2025)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [Language Generation in the Limit: Noise, Loss, and Feedback](https://mlsanity.com/paper/2507.15319/) (2025)
- [(Im)possibility of Automated Hallucination Detection in Large Language Models](https://mlsanity.com/paper/2504.17004/) (2025)
- [On Characterizations for Language Generation: Interplay of Hallucinations, Breadth, and Stability](https://mlsanity.com/paper/2412.18530/) (2024)
- [Language Generation and Identification From Partial Enumeration: Tight Density Bounds and Topological Characterizations](https://mlsanity.com/paper/2511.05295/) (2025)
- [Pareto-optimal Non-uniform Language Generation](https://mlsanity.com/paper/2510.02795/) (2025)
- [Language Generation with Infinite Contamination](https://mlsanity.com/paper/2511.07417/) (2025)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research](https://mlsanity.com/paper/2606.13306/) (2026)
- [CSLib: The Lean Computer Science Library](https://mlsanity.com/paper/2602.04846/) (2026)
- [AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory](https://mlsanity.com/paper/2602.02285/) (2026)
- [Language Generation with Replay: A Learning-Theoretic View of Model Collapse](https://mlsanity.com/paper/2603.11784/) (2026)
- [Mistake-Bounded Language Generation](https://mlsanity.com/paper/2605.10809/) (2026)
- [Characterizing the Effect of Noise in Language Generation in the Limit](https://mlsanity.com/paper/2601.21237/) (2026)
- [Contrastive Identification and Generation in the Limit](https://mlsanity.com/paper/2605.06211/) (2026)
- [Differentially Private Language Generation and Identification in the Limit](https://mlsanity.com/paper/2604.08504/) (2026)

## Abstract (arXiv)

We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit. Introduced by Kleinberg and Mullainathan at NeurIPS 2024, language generation in the limit studies a theoretical question motivated by LLMs: how to generate valid new strings from observed examples. This young and rapidly evolving field offers a natural testbed for studying large-scale formalization. GenLimitLib contains formal developments for 30 papers. It extracts shared definitions and reusable proof components while preserving paper-specific assumptions and statements, and records relationships across papers. In this way, GenLimitLib provides a concrete and structured view of the literature. We show through mathematical case studies and LLM experiments how our library can support both human mathematical research and AI-assisted research. Our Library: https://github.com/pengzhang91/generation-in-the-limit-lib.