# Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization

arXiv: https://arxiv.org/abs/2403.11437 · HTML: https://mlsanity.com/paper/2403.11437/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Mar 2024.

## Built on by (most cited first, 2 of 2)

- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory](https://mlsanity.com/paper/2602.02285/) (2026)

## Abstract (arXiv)

The convergence rate of various first-order optimization algorithms is a pivotal concern within the numerical optimization community, as it directly reflects the efficiency of these algorithms across different optimization problems. Our goal is making a significant step forward in the formal mathematical representation of optimization techniques using the Lean4 theorem prover. We first formalize the gradient for smooth functions and the subgradient for convex functions on a Hilbert space, laying the groundwork for the accurate formalization of algorithmic structures. Then, we extend our contribution by proving several properties of differentiable convex functions that have not yet been formalized in Mathlib. Finally, a comprehensive formalization of these algorithms is presented. These developments are not only noteworthy on their own but also serve as essential precursors to the formalization of a broader spectrum of numerical algorithms and their applications in machine learning as well as many other areas.