Verified Deep Learning with Lean 4
A formal verification of the math of modern deep learning, written as a Lean 4 blueprint project and shipped as the code it proves. Mathlib's fderiv is the foundation; every layer's backward is derived as a vector-Jacobian product rather than asserted -- dense, ReLU, softmax cross-entropy, 2D convolution, max-pool, Bat...