In this talk, we present Peppy, an AI-assisted workflow for discovering tight, analytic convergence proofs for optimization algorithms. While existing automated tools can generate numerical convergence bounds for first-order methods, translating these numerical certificates into analytic Lyapunov proofs independent of iteration number remains a complex manual task. Peppy bridges this gap by combining structured, verifiable blocks with AI agents. Case studies on first-order methods demonstrate its ability to support a rigorous, practical, and reproducible paradigm for AI-assisted theorem synthesis in optimization.