Papers With

← All papers
First page of GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research

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

Shuangping Li, Peng Zhang

cs.LG Sep 29, 2026 · v1 cs.LO
formalization theorem-proving-ml ml-theory logic
Read PDF arXiv abstract Code
TL;DR
Builds a Lean 4 library formalizing 30 papers on language generation in the limit, and evaluates LLM proof generation using it.
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.
Problem

Language generation in the limit, introduced by Kleinberg and Mullainathan in 2024, is a young and rapidly growing literature. Its shared objects, essential assumptions, and reusable proof ideas are not yet organized. The authors ask whether formalization can give this literature a structured view and support human and AI-assisted research.

Approach

GenLimitLib is a source-aligned Lean 4 library covering 30 papers, including classical identification results of Gold and Angluin. It extracts shared definitions and reusable proof components, keeps paper-specific assumptions and statements, and records cross-paper relationships. Humans chose which papers and results to formalize and at what level (semantic versus finite-query). LLM experiments compare proof generation with minimal vocabulary (P), the full sub-library (PML), and an oracle-selected file subset (PML-Oracle), and also test mathematical reading comprehension.

Figure 2: Research paper clusters in language generation in the limit. We follow the order in languagegeneration.github.io to number the papers.
Results

Formalization exposed a gap in a published proof (Charikar–Pabbaraju, Claim 7), which was repaired. It also transferred a construction between papers and solved an open problem for the staircase family, all verified in Lean. Library access raised LLM proof success from 48/100 (P) to 79/100 (PML) and 81/100 (PML-Oracle), with lower API cost per valid proof.

ConditionValid proofsAPI cost / valid proof
P48/100$2.76
PML79/100$1.95
PML-Oracle81/100$1.78
Valid Lean proofs and cost by resource condition