TorchLean Guide🔗

TorchLean is a Lean 4 library for neural network code that can be run, inspected, lowered into a shared graph IR, and connected to explicit mathematical contracts. A model can appear as ordinary user code, as a graph, as a runtime computation, and as a verification target without changing which mathematical object the project is talking about.

This guide is the readable path through that stack. It starts with the reason TorchLean exists, then follows one model through typed tensors, training, runtime execution, graph semantics, Float32/native boundaries, verification, examples, and the concluding summary.

The generated API docs are still the best place to look up an exact declaration. The module graph is the best place to explore imports. The guide gives the narrative spine: why we built the pieces, how they fit, and what kind of guarantee each layer is meant to provide.

For a first pass, read Introduction → Building Models → Runtime and Interop → Semantics and Graphs. If you are here for verification, jump from there to Verification and Certificates. If you want concrete demos, skip ahead to Examples and Applications.

If you are new to Lean, keep the official Lean material nearby: Functional Programming in Lean, Theorem Proving in Lean 4, and The Lean Language Reference. We cite papers and external tools in the chapters where they matter, instead of front-loading a bibliography before the reader has context.