TorchLean: Formalizing Neural Networks in Lean
Summary
TorchLean is a Lean 4 framework that treats neural networks as first-class mathematical objects with a single semantics shared by execution and verification. It provides a PyTorch-like verified API with eager and compiled modes that lower to a common SSA/DAG IR, explicit Float32 semantics, and verification via IBP and CROWN/LiRPA-style bound propagation with certificate checking. The work demonstrates end-to-end verification capabilities including certified robustness, PINN residual bounds, Lyapunov-style neural controller verification, and includes mechanized theoretical results such as a universal approximation theorem.