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 d

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 https://github.com/OUPL/MLCert