1.1.1. A First Program🔗

Application code uses the focused NN.API import:

import NN.API

open TorchLean

def model :
    nn.M (nn.Sequential (.dim 2 .scalar) (.dim 1 .scalar)) :=
  nn.Sequential![
    nn.linear 2 8,
    nn.relu,
    nn.linear 8 1
  ]

The model accepts a length-two tensor and returns a length-one prediction. The dimensions occur in the model's type, so the output of a layer with width seven cannot be fed to a layer expecting width eight. nn.M means that this is a seeded model builder. It describes initialization but has not yet chosen the random seed or produced concrete parameter tensors.

We can initialize it directly:

def initialized :=
  nn.run 2026 model

or ask the trainer to initialize and execute it:

def trainer :=
  Trainer.new model
    { task := .regression
      optimizer := optim.adam { lr := 0.001 }
      seed := 2026 }

The notation is intentionally familiar to a PyTorch user, but Lean learns more from the declaration. It checks the input and output dimensions while elaborating the file. It distinguishes the seeded builder from the initialized model. Once initialized, the model exposes the exact order and shape of its parameter tensors. That information is available later to the trainer, graph compiler, and verifier without rediscovering it from runtime metadata.

1.1.2. Opening The Model Up🔗

The same initialized model can participate in several parts of TorchLean.

1.1.3. Shapes Catch The Bug Where It Starts🔗

A TorchLean tensor has a scalar type and a shape:

\operatorname{Tensor.T}\;\alpha\;s.

For example,

def predictions : Tensor.T Float (shape![32, 1]) :=
  tensorOfList! [32, 1] (List.replicate 32 0.0)

def labels : Tensor.T Float (shape![32]) :=
  tensorOfList! [32] (List.replicate 32 0.0)

These are different types. A loss that expects equal shapes cannot silently broadcast the label vector across the second axis. Lean asks us to choose: reshape the labels, squeeze the predictions, or use another loss. That is exactly where the ambiguity belongs.

Shape typing is deliberately modest. It catches structural mistakes while they are still local. Questions about units, label quality, normalization, finiteness, and generalization appear later as their own definitions and hypotheses instead of being smuggled into the word "tensor."

The scalar parameter is equally explicit. Tensor.T α s is homogeneous: every element of that tensor has type α. The tensor chapter develops that point once, alongside the distinction between scalar polymorphism and mixed precision.

1.1.4. From One Output To A Statement🔗

Suppose the trained model has parameters \theta, its graph is g, and the two input features vary in a box B. A range statement might be

\forall x\in B,\qquad |\operatorname{denote}(g,\theta,x)_0-y^\star|\leq\delta.

This line records the details that are easy to lose in prose:

• g identifies the operation graph;

• \theta identifies the concrete trained parameters;

• B identifies the quantified input convention;

• denote identifies the scalar and operator semantics;

• index 0, target y^\star, and tolerance \delta identify the output property.

An interval pass can compute lower and upper output bounds. A Boolean check can then confirm that the whole interval lies in [y^\star-\delta,y^\star+\delta]. The last ingredient is a soundness theorem saying that the computed interval really encloses denote for this graph.

The guide uses the following vocabulary throughout:

1.1.5. Fast Kernels Still Belong🔗

PyTorch has far broader operator coverage, distributed training, mature compilers, pretrained models, and years of production optimization. Reimplementing all of that inside Lean would be a poor use of both systems.

TorchLean can therefore call native CUDA or LibTorch for expensive operations. The source model, parameter layout, and graph remain TorchLean objects; a backend profile chooses the implementation. For example, LibTorch may compute the forward value of scaled dot-product attention while TorchLean records the tape node and applies its own backward rule. Another profile may use native TorchLean CUDA for both directions. Later we will inspect the capsule that records this choice.

This gives the project a practical division of labor: use established kernels where scale matters, and use Lean to make the surrounding mathematical claim precise.

1.1.6. Imports🔗

Use the focused TorchLean API for application code:

import NN.API
open TorchLean

Use the complete library import when one file combines application code with proofs, verification, floating-point semantics, backends, or widgets:

import NN
open TorchLean

Focused subsystem imports such as NN.IR, NN.Floats, NN.Proofs, and NN.Verification avoid loading the whole project when only one layer is needed.

1.1.7. References🔗

• Leonardo de Moura and Sebastian Ullrich, “The Lean 4 Theorem Prover and Programming Language”, CADE 2021.

• Adam Paszke et al., “PyTorch: An Imperative Style, High-Performance Deep Learning Library”, NeurIPS 2019.

• Shiqi Wang et al., “Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification”, NeurIPS 2021.