L'optimisation numérique joue un rôle central dans de nombreux domaines d'informatique. Cela est vrai pour les sciences fondamentales, mais également pour les applications industrielles impliquant, par exemple, l'apprentissage automatique ou la recherche opérationnelle. L'optimisation du premier ordre joue un rôle central en tant qu'outil clé permettant de faire évoluer nos capacités numériques à des données d'entrée de très grande taille. Toutefois, il est crucial de mieux comprendre et exploiter les propriétés de convergence de ces schémas numériques. Une partie de la communauté de l'apprentissage automatique a fait d'énormes efforts pour fournir de tels résultats, s'appuyant sur des preuves ad hoc écrites à la main et souvent complexes. Cela constitue une limitation majeure dans la gamme des schémas d'optimisation qui peuvent être analysés. L'objectif de ce doctorat est de développer des algorithmes basés sur le calcul formel pour automatiser de telles analyses.