I was wondering whether it would be feasible/useful to formalize ML, optimization and learning theory in order to help with nuanced/tricky derivations. Taking the “proof assistant” literally. I’ve seen some works doing this for specific theorems/statements, but couldn’t find anywere to get started. if I wanted to e.g. prove the convergence of SGD on convex functions, are there standard libraries/trick to help me get started? Apperently real numbers are already formalized, but there are different constructions?