Maybe type theory is good to know! I would like to see cutting edge NN libraries for Coq or Lean or Optimization ecosystem like Scipy or Scikit for Agda.

You develop your algorithm and you prove a bunch of theorems about it at the same time, incredibly difficult but totally wild!

There's some scattered projects like this https://github.com/OUPL/MLCert