Acknowledgments

Thanks to Tomáš Skřivan, whose Scientific Computing in Lean bootstrapped this project’s first MNIST trainer.

Thanks to Monica Omar on Lean Zulip, who closed the 6-level Finset.sum commutation in the Conv2D VJP proof.

Thanks to Franz Huschenbeth on Lean Zulip for reviewing early drafts and suggesting the comparator approach used in Appendix B.