This paper introduces Peppy, a workflow that uses AI to find tight, analytic convergence proofs for first-order optimization algorithms. Convergence proofs explain how fast an algorithm gets close to a solution. A “tight” proof gives bounds that are hard to improve. Peppy aims to make finding those proofs more systematic and reproducible.

The authors build Peppy around domain knowledge for optimization rather than a one-size-fits-all AI approach. Instead of treating every math problem the same way, Peppy steers the AI toward patterns and identities that are common in optimization. The system then produces structured, human-readable proofs and checks them using SymPy, a symbolic math library for Python. The paper contrasts this with other projects that use large language models and the Lean 4 proof assistant; Peppy focuses on minimal, accessible verification rather than deep formalization.

At a high level, Peppy combines AI-driven suggestion with symbolic checks. The AI proposes candidate inequalities, parameter choices, and proof steps that are typical in analyses of first-order methods. First-order methods are algorithms that use only gradient information, like the fast gradient method introduced by Nesterov. Peppy then uses symbolic computation to verify algebraic steps and to produce final analytic bounds.

The authors report experiments that show Peppy can produce rigorous, practical, and reproducible proofs from examples. They highlight that the workflow was able to address several open problems in tight convergence analysis, including conjectures about Nesterov’s Fast Gradient Method. If broadly adopted, this approach could make parts of algorithm analysis faster and less reliant on manual trial-and-error.

There are important caveats. The results are presented as experimental demonstrations, so the approach is supported by examples rather than by a proof of general applicability. Verification is done with SymPy, which is accessible but is not a full formal proof assistant like Lean 4; that means the checks are symbolic and practical but not necessarily a machine-checked formal proof in a proof system. Also, Peppy leans heavily on domain-specific knowledge, so it may be less useful outside first-order optimization problems or in areas with very different proof patterns.