Stochastic Optimisation

Stream: Is there code for X?

[Sayantan Majumdar]

I am doing some work where we are using some convex optimisation and some stochastic optimisation . I am new to these topics and so was wondering have theorems in these topics already implemented or these topics formalised?

[Jason Rute]

It is not Lean, but you might be interested in looking at the work in https://github.com/IBM/FormalML. This includes a proof in Coq of Dvoretzky's Stochastic Approximation Theorem by @Koundinya Vajjha, @Avi Shinnar, @Barry Trager, and @Vasily Pestun.

[Sayantan Majumdar]

Thanks, I will check it right now.