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.

A fixed model can be recorded as a shape-indexed SSA graph for execution and differentiation. Supported forward programs can also be lowered to TorchLean's shared operation IR for verification and export. Theorems about derivatives are stated separately from these executable graph representations, and backend assumptions remain explicit.

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.