AI-Assisted Mathematical Research with Lean: A Case Study in Language Generation in the Limit

Can formalization become a tool for mathematical research? I will discuss this question through my experience with AI-assisted Lean formalization. I will present GenLimitLib, a Lean 4 library for language generation in the limit, a young and rapidly developing research area in theoretical computer science. GenLimitLib organizes shared definitions, reusable proof components, and relationships across papers, providing a structured view of the literature. I will describe several mathematical findings that emerged from working with the library. I will also present LLM experiments showing that access to the library can improve AI-assisted Lean proof generation. The talk will be based on this paper: https://arxiv.org/abs/2609.36663.

Additional Information:

Prof. Peng Zhang is an Assistant Professor in the Department of Computer Science and a graduate faculty member in Statistics at Rutgers University. Her research broadly encompasses algorithm design and data science, with specific interests in causal inference, experimental design, and numerical optimization. Before joining Rutgers, Dr. Zhang completed a postdoctoral fellowship at Yale University. She received her Ph.D. in Computer Science from Georgia Tech in 2018, where her work earned the College of Computing Dissertation Award. Her research is supported by an NSF CAREER Award and an Adobe Data Science Research Award.