TorchLean brings tensor computation, machine learning, and formal verification together in Lean 4. The cool part is that Lean is both a functional programming language and a theorem prover, so you can write computations, build and train models, and prove mathematical properties in the same language. You can start with tensors and linear algebra, use the library for general numerical programming, or work directly with the specifications and proofs.

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

A few highlights we’re excited about:

• Tensors that carry their shapes. Lean checks that the dimensions fit when you compose tensor operations. You can use the array and linear algebra library on its own, without building a neural network.
• Build and train models in Lean. Start with regression or other classical models, train a transformer or generative model, or develop a reinforcement learning agent. The training tools include automatic differentiation, optimizers, and CPU and GPU execution.
• A shared graph for computation and proofs. A typed computation graph records the operations in a model and the shapes of their inputs and outputs. We use it to describe the calculation, execute it, and state mathematical properties about it. The formalization map connects the definitions to their proofs.
• Floating-point behavior is part of the mathematics. Through FloatLib, TorchLean supports configurable binary formats, executable arithmetic, and proofs about rounding and numerical error. The floating-point guide explains the arithmetic models and how they relate to native execution.
• Ask questions about a whole range of inputs. For a classifier, we can establish conditions under which its prediction stays the same throughout an input region. The verification tools include interval bounds and certificate checking, with Lean proofs for the mathematical guarantees.

The guide walks through the library step by step. If you’d rather start by running something, try the examples.