TorchLean🔗

TorchLean is a Lean 4 library for writing, training, and verifying neural networks. The quickest way to understand it is to follow one prediction through the system. A pair of input features enters a shape-typed model, concrete parameters turn that model into a program, the runtime records the operations needed for differentiation, and a graph records the computation so that preservation and verification questions can be stated explicitly. The value may travel through several representations, but none of those handoffs is meant to be invisible.

Our companion for that trip is a small nonlinear regression network. At first it looks pleasantly ordinary: two linear layers with a ReLU between them. We will train it, inspect its parameter shapes, watch a backward pass accumulate gradients, move selected operations to CUDA, and finally ask what can be proved about its outputs. By returning to the same model, the guide can explain why a theorem about an exact real-valued specification is relevant to a particular floating-point GPU run without automatically proving that run correct.

Once that path feels familiar, the larger examples are variations on the same theme. Transformers add token and attention structure; ResNets add spatial layouts and skip connections; Fourier neural operators work with sampled functions; diffusion and reinforcement learning make randomness and state explicit. The numerical chapters supply generic formats, executable binary32 arithmetic, and error bounds. The verification chapters build interval, affine, compiler, autograd, and certificate arguments on top of those definitions.

One reading habit matters throughout: ask what kind of evidence is attached to a claim. An implemented path can be executed. A tested path has a regression or conformance check. A proved statement has a Lean theorem with the hypotheses visible in its type. A planned feature is only future work. The guide includes successful runs and deliberately rejected inputs so that these differences can be observed rather than guessed from an impressive module name.

The examples are meant to be run from the repository root. No theorem-proving background is needed to begin. Readers new to Lean may also use Functional Programming in Lean, Theorem Proving in Lean 4, and The Lean Language Reference.