mlsanityData to 7 Oct 2026

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

arXiv 2609.36663 ↗First posted 29 Sep 2026cs.LG cs.LOcited by 0

Not on the map. Why?

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.

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

Builds on

35 of 46 references.

References · 35

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2019The Lean mathematical librarycited by 127
  3. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  4. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  5. 2024Language Generation in the Limitcited by 39
  6. 2024Generation through the lens of learning theorycited by 30
  7. 2024LeanReasoner: Boosting Complex Logical Reasoning with Leancited by 28
  8. 2024Exploring Facets of Language Generation in the Limitcited by 27
  9. 2026Automated Conjecture Resolution with Formal Verificationcited by 21
  10. 2025Density Measures for Language Generationcited by 20
  11. 2025Generation from Noisy Examplescited by 19
  12. 2025Representative Language Generationcited by 18
23 more
  1. 2026Advancing Mathematics Research with AI-Driven Formal Proof Searchcited by 18
  2. 2025On Union-Closedness of Language Generationcited by 17
  3. 2025Language Generation in the Limit: Noise, Loss, and Feedbackcited by 15
  4. 2025(Im)possibility of Automated Hallucination Detection in Large Language Modelscited by 14
  5. 2024On Characterizations for Language Generation: Interplay of Hallucinations, Breadth, and Stabilitycited by 13
  6. 2025Language Generation and Identification From Partial Enumeration: Tight Density Bounds and Topological Characterizationscited by 13
  7. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 13
  8. 2025Pareto-optimal Non-uniform Language Generationcited by 10
  9. 2025Language Generation with Infinite Contaminationcited by 10
  10. 2026LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Provingcited by 7
  11. 2026Language Generation with Replay: A Learning-Theoretic View of Model Collapsecited by 5
  12. 2026EconCSLib: AI-Assisted Lean Formalization for Economics & Computation researchcited by 5
  13. 2026Characterizing the Effect of Noise in Language Generation in the Limitcited by 4
  14. 2026AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theorycited by 4
  15. 2026CSLib: The Lean Computer Science Librarycited by 4
  16. 2026Mistake-Bounded Language Generationcited by 4
  17. 2026Differentially Private Language Generation and Identification in the Limitcited by 3
  18. 2026Contrastive Identification and Generation in the Limitcited by 3
  19. 2026A Theory of Time-Sensitive Language Generation: Sparse Hallucination Beats Mode Collapsecited by 2
  20. 2026On Language Generation in the Limit with Bounded Memorycited by 2
  21. 2026EconCSLib: A Lean Library for Computational Economics and AI-Assisted Researchcited by 2
  22. 2026MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Researchcited by 1
  23. 2026Dense Language Generation Made Simple: Deterministic, Randomized, and Multi-Order Algorithmscited by 1

Built on by

Not cited yet.