{"id":"arxiv/2609.35762","url":"https://arxiv.org/abs/2609.35762","tags":["math.OC"],"score":0,"title":"Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms","domain":"math.OC","source":"arxiv","authors":["Jaewook J. Suh","TaeHo Yoon","Edward Duc Hien Nguyen","Bicheng Ying","Shiqian Ma"],"reviews":0,"subject":"math.OC","summary":"This paper presents Peppy, an AI-assisted workflow for discovering tight, analytic convergence proofs for first-order optimization algorithms. Generic approaches to using LLMs to conduct mathematical research target an unspecified, broad spectrum of problems and sometimes use the Lean 4 proof assistant for formalization. On the other hand, Peppy leverages domain-specific knowledge more heavily and is thereby capable of constructing the proofs in a more structured manner, which allow a minimal and accessible verification through SymPy. We experimentally demonstrate through examples that Peppy…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-28","reactions":{}}