TorchLean🔗

TorchLean is a Lean 4 library for writing, training, and reasoning about neural networks. Tensor dimensions appear in types, model definitions are executable, and supported programs can be recorded as graphs for differentiation, export, and verification.

The running example is a nonlinear regression model with two linear layers and a ReLU. We train it, inspect its parameters and gradients, run it through different numerical backends, and state exact claims about the corresponding mathematical definitions. The distinction matters: a theorem about real-valued matrix multiplication does not by itself verify the floating-point instructions issued by a GPU kernel.

The same questions recur in larger models. An attention mask changes which tokens can influence a prediction; a reduction order changes where arithmetic rounds; a certificate needs to identify the weights and input region it covers. We will follow these connections from small calculations to transformers, ResNets, Fourier neural operators, diffusion, and reinforcement learning.

All commands are run from the repository root. Readers new to Lean may also use Functional Programming in Lean, Theorem Proving in Lean 4, and The Lean Language Reference.