1: \begin{abstract}

2: The convergence rate of various first-order optimization algorithms is a pivotal concern within the 

3: numerical optimization community, as it directly reflects the efficiency of these algorithms across 

4: different optimization problems.  Our goal is making a significant step forward in the formal mathematical representation 

5: of optimization techniques using the Lean4 theorem prover. We first formalize the gradient for smooth functions and the subgradient 

6: for convex functions on a Hilbert space, laying the groundwork for the accurate formalization 

7: of algorithmic structures. Then, we extend our contribution by proving several properties 

8: of differentiable convex functions that have not yet been formalized in Mathlib. Finally,  a comprehensive formalization of these algorithms is presented. These developments 

9: are not only noteworthy on their own but also serve as essential precursors to the formalization of 

10: a broader spectrum of numerical algorithms and their applications in machine learning as well as many other areas. 

11: % The results of this work have the potential to catalyze the development of autoformalization tools, 

12: % leveraging the foundational formalization of basic algorithms to facilitate further advancements in the field.

13: \end{abstract}

14: