From a typed model to execution, analysis, and proof.

TorchLean is the first unified deep-learning framework built in Lean 4. It brings model construction, training, and formal reasoning into one library, so executable neural-network code and the mathematics used to study it do not become separate projects.

You use it much like an ordinary ML library: define a model, load tensors, and train on CPU or GPU. Tensor shapes are part of the types, so incompatible layers and malformed operations are caught while the program is being written rather than during a training run.

Once a model runs, its Lean definition can be lowered to the graph used by the runtime. Backends and accelerated kernels remain explicit, including the assumptions made at external library boundaries. The graph can then be studied with formally verified floating-point arithmetic, autograd theorems, robustness bounds, and certificate checkers.

Start reading View examples Build performance Read the paper

Working Paths

01 Write and run models Use Lean-native training loops, tensors, and autograd examples. 02 Lower to graph IR Inspect shapes, payloads, graph semantics, and executable traces. 03 Choose a backend Keep one model while choosing CPU, CUDA, LibTorch, or named future accelerator targets. 04 Check verification artifacts Replay bounds and certificates, then read the Lean statements they support. 05 Turn bugs into contracts Study small checked examples for masks, losses, normalization, caches, and runtime edges.