A Python package for automated Lyapunov-based convergence analyses of first-order optimization and inclusion methods.
AutoLyap streamlines the process of constructing and verifying Lyapunov analyses by formulating them as semidefinite programs (SDPs). It supports a broad class of structured optimization and inclusion problems, providing computer-assisted proofs of linear or sublinear convergence rates for many well‑known algorithms.
A typical workflow:
- Choose the class of optimization/inclusion problems.
- Choose the first-order method to analyze.
- Choose the type of Lyapunov analysis to search for or verify (which implies a convergence or performance conclusion).
AutoLyap builds the underlying SDP and solves it through configurable backend solvers.
- User docs: https://autolyap.github.io
- Contributing guide: https://autolyap.github.io/contributing/
- Developer commands (internal):
DEVELOPER_COMMANDS.md - Changelog:
CHANGELOG.md - Release process (maintainers):
RELEASING.md - License:
LICENSE
If AutoLyap contributes to your research or software, please cite:
- Upadhyaya, Manu; Das Gupta, Shuvomoy; Taylor, Adrien B.; Banert, Sebastian; Giselsson, Pontus (2026). The AutoLyap software suite for computer-assisted Lyapunov analyses of first-order methods. arXiv:2506.24076.
@misc{upadhyaya2026autolyap,
author = {Upadhyaya, Manu and Das Gupta, Shuvomoy and Taylor, Adrien B. and Banert, Sebastian and Giselsson, Pontus},
title = {The {AutoLyap} software suite for computer-assisted {L}yapunov analyses of first-order methods},
year = {2026},
archivePrefix = {arXiv},
eprint = {2506.24076},
primaryClass = {math.OC},
}