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

Shuangping Li; Peng Zhang

cs.LGSep 29, 2026

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

Authors: Shuangping Li, Peng Zhang

Organizations: Yale University · Rutgers University

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.

Figures & tables

Figure 1: Cumulative number of papers in language generation in the limit (source: languagegeneration.github.io , accessed September 2026).

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

Condition	Resources
P	Minimal Lean vocabulary
PML	Full research sub-library
PML-Oracle	Oracle-selected library subset

Table 1: Resource conditions.

	Success
Condition	Success H/M P	PML	PML- Oracle	Overall
Proof / H	15/25	22/25	25/25	62/75
No proof / H	14/25	22/25	24/25	60/75
Proof / M	10/25	17/25	16/25	43/75
No proof / M	9/25	18/25	16/25	43/75
Overall	48/100	79/100	81/100	208/300

Table 2: Results across resource conditions. Left: aggregate success by proof availability and reasoning effort. Right: task-level success (H/M denotes high/medium reasoning, each out of ten trajectories) and proof-relevant library reuse; library share is computed over successful proofs.

Condition	Valid proofs	API cost / valid proof
P	48/100	$2.76
PML	79/100	$1.95
PML-Oracle	81/100	$1.78

Table 3: API efficiency.

Information supplied	Accuracy (%)
Question only	41.20
Paper excerpts	70.09
Paper + unrelated Lean	71.12
Paper + Lean in file order	73.45
Paper + relevant Lean	78.55

Table 4: Lean evidence: 404 questions.

Map supplied	Accuracy (%)
No map	60.26
Relevant map	70.61
Sham map	60.51

Table 5: Paper map: 204 questions.

Appendix figures & tables5 assets

Supplementary material from the paper’s appendix.

Appendix

Finding	Proof	Lean scope
Section 4.1 : local invariant repair	Appendix A.2	Counterexample, corrected score bound, and the repaired generation guarantee, including repeated observations.
Theorem 1 : finite proper replay	Appendix A.3	Three-language impossibility, both directions of the characterization, and finite-state consequences.
Theorem 2 : exact staircase frontier	Appendix A.4	Exact guarantees, lower bounds for arbitrary deterministic generators, and Pareto optimality.

Appendix

Table 6: Proofs of the featured findings and scope of formal verification.

Task	Vocabulary files	PML-Oracle files
Case 002	6	4
Case 017	8	10
Case 024	6	13
Case 025	8	44
Case 019	8	59

Appendix

Table 7: Task-specific formal resources. Vocabulary files are used for Lean theorem statements and are provided for all conditions. PML-Oracle files are oracle-selected Lean files for the condition PML-Oracle, which form a subset of the 161-file frozen sub-library.

Setting	P	PML	PML-Oracle
Case 002
Proof / High	5	4	5
No proof / High	4	5	5
Proof / Medium	2	2	2
No proof / Medium	2	4	3
Case 017

Appendix

Table 8: Full task-level success. Each entry is the number of successful trajectories out of five independent runs. The tasks Case 002, 017, 024, 025, 019 correspond to Tasks A, B, C, D, E in Section 5.1 , respectively.

Panel A: By theorem task
	P	PML	PML-Oracle
Case 002	$2.28	$2.06	$1.91
Case 017	$1.56	$1.13	$0.99
Case 024	$2.05	$0.89	$0.95
Case 025	–	$1.43	$1.34
Case 019	–	$11.10	$5.90

Appendix

Table 9: Failure-adjusted API cost per valid proof. Panel A pools over proof availability and reasoning effort within each theorem task. Panel B pools over theorem tasks within each experimental setting. The tasks Case 002, 017, 024, 025, 019 correspond to Tasks A, B, C, D, E in Section 5.1 , respectively.

Condition	Valid proofs	API calls per run	Input tokens per run	Cache-write tokens per run	Reasoning tokens per run	Author time per run
P	48/100	55.6	3.122M	166.6K	11.3K	19.3 min
PML	79/100	51.9	3.121M	253.8K	9.33K	15.7 min
PML-Oracle	81/100	53.6	3.184M	210.2K	9.94K	17.6 min

Appendix

Table 10: Aggregated resource usage per scheduled trajectory. Each resource total is divided by the 100 total scheduled trajectories in the corresponding arm. Input tokens are cumulative across API calls and include cached prefixes; cache-write tokens measure newly cached prompt prefixes. Author time excludes scheduler queueing, setup, final validation, and packaging.

AI-Assisted Mathematical Discovery

See all 18 papers

Evaluation of LLMs for Mathematical Formalization in Lean
Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6LLM Evaluation Lean Theorem Proving
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Multi-Agent LLM Systems Automated Theorem Proving
Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
Jun 16, 2026Xiyu Zhai, Xinyi Chen, Yiping Wang +3Automated Theorem Proving Lean Theorem Proving
University of Washington · University of Innsbruck

Jun 4, 2026J/K move · Enter open · S save

Evaluation of LLMs for Mathematical Formalization in Lean

Tyson Klingner, Drew Bladek, Escher Crawford, Bohao Chen+5

Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA

LLM Evaluation Lean Theorem Proving LLM Mathematical Reasoning Large Language Model-Guided Theorem Proving

Open paper AskPDF arXiv

Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@

k

and refine@

k

metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of

<\

0.01$ per correct proof.

Abstract

AI-Assisted Mathematical Discovery

Explore similar work

Evaluation of LLMs for Mathematical Formalization in Lean

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics