Abstract
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.
Keywords
Subject
Publication details
- Journal
- Not available
- Open access
- Green open access
Cite this article
APA 7
Li, S., & Zhang, P. (2026). GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research. https://omanscience.com/en/articles/genlimitlib-a-formal-library-for-language-generation-in-the-limit-and-ai-assisted-mathematical-research
MLA 9
Li, Shuangping, and Peng Zhang. "GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research." https://omanscience.com/en/articles/genlimitlib-a-formal-library-for-language-generation-in-the-limit-and-ai-assisted-mathematical-research.
Chicago (author–date)
Li, Shuangping, and Peng Zhang. 2026. "GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research." https://omanscience.com/en/articles/genlimitlib-a-formal-library-for-language-generation-in-the-limit-and-ai-assisted-mathematical-research.
Harvard
Li, S. and Zhang, P. (2026) 'GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research', Available at: https://omanscience.com/en/articles/genlimitlib-a-formal-library-for-language-generation-in-the-limit-and-ai-assisted-mathematical-research.
Vancouver
Li S, Zhang P. GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research. https://omanscience.com/en/articles/genlimitlib-a-formal-library-for-language-generation-in-the-limit-and-ai-assisted-mathematical-research
IEEE
S. Li, and P. Zhang, "GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research," https://omanscience.com/en/articles/genlimitlib-a-formal-library-for-language-generation-in-the-limit-and-ai-assisted-mathematical-research.