Numerical optimization plays a central role in many fields of computer-sciences. This is true for fundamental sciences, but also in industrial applications involving, e.g., machine learning, or operation research. First order optimization plays a central role as key enabler allowing to scale our numerical capabilities to super large input data. Still, it is crucial to understand and exploit better convergence properties of such numerical schemes. Part of the ML community has made tremendous effort to provide such results, relying on ad-hoc rather involved hand-written proofs. This is a severe restriction to the range of optimization schemes that can be analyzed. The goal of this PhD is to develop computer algebra-based algorithms that will automate such analyses.