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

Explore TorchLean

01 Write and run models Define typed tensors and models, then train them with Lean-native autograd. 02 Lower to graph IR Inspect operation nodes, shapes, payloads, semantics, and execution traces. 03 Choose a backend Run on CPU or CUDA, with explicit contracts for native and external providers. 04 Check verification artifacts Replay robustness bounds and certificates against their Lean predicates. 05 Turn bugs into contracts See causal masks, stable losses, normalization, and KV-cache bugs reduced to precise claims.