Backpropagation formalized in Lean.

Stream: new members

[Tony Johnson]

Hi, I'm looking to formalize backpropagation (http://neuralnetworksanddeeplearning.com/chap2.html) in Lean as a learning exercise. 1) Is this too difficult for a beginner in Lean 2) If not, could somebody familiar with Lean and Backprop possibly point me in the right direction.

Thanks!

[Dominic Steinitz]

Caveat: I last looked at this area over 10 years ago and am somewhat new to Lean. I don't know what you mean by formalise here. Do you mean a Lean version of what has been done in Haskell: https://hackage.haskell.org/package/backprop? I haven't looked but I haven't seen anything about AD on zulip or stochastic gradient descent for that matter.

[Dominic Steinitz]

And although I have programmed in Haskell for over 30 years, I found proving things in Lean a steep learning curve.