2.5.1. The Namespaces🔗

You can read the import as a small workbench rather than a module-tree lesson. Tensor gives us values, nn turns them into models, Data supplies examples, and Trainer carries the model through optimization and prediction. The remaining names become useful when we ask a more specific question:

The lowercase nn.linear, nn.relu, and optim.adam names are the canonical spellings. Internal implementation namespaces may be longer because they distinguish specification, runtime, and proof layers. Application code should not depend on those names unless it genuinely needs the lower layer.

2.5.2. Make A Scratch Program🔗

Create Scratch.lean at the repository root:

import NN.API

open TorchLean

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

def xs : Tensor.T Float (shape![4, 2]) :=
  tensor! [
    [0.0, 0.0],
    [0.0, 1.0],
    [1.0, 0.0],
    [1.0, 1.0]
  ]

def ys : Tensor.T Float (shape![4, 1]) :=
  tensor! [[0.0], [1.0], [1.0], [0.0]]

def data : Trainer.Dataset (shape![2]) (shape![1]) :=
  Data.tensorDataset xs ys

def trainer :=
  Trainer.new model
    { task := .regression
      optimizer := optim.adam { lr := 0.03 }
      dtype := .float
      backend := .eager
      seed := 2026 }

def main : IO Unit := do
  let trained ← trainer.train data
    { steps := 20
      batchSize := 4
      logEvery := 5 }
  trained.printSummary

  let heldout : Tensor.T Float (shape![2]) :=
    tensor! [0.25, -0.75]
  let yhat ← trained.predict heldout
  IO.println s!"prediction={Tensor.pretty yhat}"

Check the definitions without starting the training run:

lake env lean Scratch.lean

Lean normally stays silent here apart from diagnostics. To execute the main already present in the file, run:

lake env lean --run Scratch.lean

The current deterministic run ends with:

dataset size = 4
mean_loss(before) = 0.299386
step 0: loss=0.265440
step 5: loss=0.117008
step 10: loss=0.052596
step 15: loss=0.013994
mean_loss(after) = 0.001102
steps=20 loss0=0.299386 loss1=0.001102
prediction=[0.683571]

The loss says that this small network fit the four supplied rows well; the final line is one prediction at a fifth point, not a generalization claim. The --run path is convenient for a one-file experiment. A maintained command should still receive a Lake executable target so it can be built and invoked by name.

2.5.3. Read The Types In VS Code🔗

Place the cursor on model. The infoview should show:

nn.M (nn.Sequential (shape![2]) (shape![1]))

Then change the final layer from nn.linear 8 1 to nn.linear 7 1. The error is attached to model construction rather than the training call.

Place the cursor on trained.predict. Its input and output are trainer-facing Float tensors with the model's checked shapes. The retained runner handles conversion to the scalar selected by the training configuration.

2.5.4. Builder, Trainer, And Trained Handle🔗

These three values have different lifetimes:

model : nn.M (nn.Sequential inputShape outputShape)

Trainer.new model config

trainer.train data options

2.5.5. Persistent And Per-Call Configuration🔗

Persistent choices can be expressed as Trainer.RunConfig:

def eagerCpu : Trainer.RunConfig :=
  { optimizer := optim.adam { lr := 0.03 }
    dtype := .float
    backend := .eager }

def compiledCpu : Trainer.RunConfig :=
  eagerCpu.compiled.cpu

def configuredTrainer :=
  Trainer.new model
    (Trainer.Config.fromRunConfig
      compiledCpu .regression
      (seed := 2026))

RunConfig contains the optimizer, scalar implementation, execution mode, and complete backend profile. The profile keeps device, providers, evidence policy, and VJP ownership consistent.

Per-call TrainOptions controls step count, sample grouping, logging cadence, and artifact fields. Not every task dispatch consumes every optional field: exact-bits loadParams? and saveParams? are currently wired through classification/cross-entropy training, while regression and custom-loss code should use the direct checkpoint helpers described in the training chapter. trainWithRun applies a temporary runtime configuration for one call.

2.5.6. DType Means Scalar Semantics🔗

For an ordinary executable trainer, .float selects Lean's host Float, while .float32 selects the bit-level IEEE32Exec implementation by default. These are not two labels on the same untyped buffer: the choice changes the implementation of +, *, exp, reductions, and the other scalar operations used by the run.

The dtype language also names proof-oriented interpretations. .real denotes mathematical reals, and .float32 { mode := .fp32 } denotes the rounded-real binary32-precision model with gradual underflow but without an upper exponent bound or IEEE special values. They can appear in common configuration and theorem-facing code, but an IO trainer rejects them because they are noncomputable. The generic dispatcher can construct executable complex binary32 as well; the high-level trainer currently rejects complex training and prediction because it has no host-Float readback path.

One run follows the scalar contract from Tensors And Shapes. The comparison with PyTorch explains the present mixed-precision boundary.

For theorem work, instantiate specification tensors directly over ℝ or FP32. For a runtime run, choose an executable scalar and record the provider boundary.

2.5.7. Data Is Runtime-Polymorphic🔗

Trainer.Dataset σ τ knows how to materialize samples after the trainer selects a scalar:

Data.tensorDataset
Data.regressionGrid
Data.supervisedNpyDataset
Data.tabularCsvDataset
Data.batchDataset

The model and dataset must agree on σ and τ. A file loader checks runtime dimensions before constructing the typed dataset.

A true tensor minibatch changes shapes to [batch,...]. Data.batchDataset stores each fixed-size minibatch as one dataset item, so TrainOptions.batchSize := 1 executes one vectorized forward/backward pass per update. On an unbatched dataset, the same option counts individual samples. Values above one always mean gradient accumulation across several dataset items. The data chapter develops both forms.

2.5.8. Explicit Differentiation🔗

For a tensor function:

autograd.func.grad
autograd.func.valueAndGradScalar
autograd.func.vjp
autograd.func.jacfwd
autograd.func.jacrev
autograd.func.hessian

For a checked model:

autograd.model.gradParams
autograd.model.gradInputs
autograd.model.valueAndGradParamsScalar
autograd.model.vjpParams
autograd.model.jvpParams
autograd.model.hvpParams

Derivatives are returned as values. Parameter derivatives have the same dependent tensor-pack structure as the parameters; there is no mutable .grad field on Tensor.T values.

2.5.9. Functional Tensor Operations🔗

Use nn.functional when constructing a differentiable tensor program:

def energy :
    autograd.func.Fn (shape![4]) Shape.scalar :=
  fun x => do
    let x2 ← nn.functional.square x
    nn.functional.mean x2

This program can be differentiated by autograd.func. An arbitrary Lean function over Spec.Tensor is useful for specifications but does not automatically carry runtime graph and derivative behavior.

The distinction is analogous to an embedded differentiable language: operations must register the semantics needed by execution and AD.

2.5.10. Classical Models🔗

Statistical and classical ML models do not need a neural layer stack. Their definitions live in Spec, alongside the tensor mathematics they use.

Keeping these models in the library does not require pretending they are neural networks. What they share with the neural code is the shape-indexed tensor foundation and explicit data, not one forced architecture abstraction.

Here is a complete executable k-nearest-neighbor classifier. The model stores its labeled samples; evaluation computes distances and applies a deterministic majority vote, including deterministic tie-breaking by neighbor order.

import NN.API

open TorchLean
open Spec

def point (x y : Float) : Tensor.T Float (shape![2]) :=
  tensor! [x, y]

def labels : KNN Float String 2 :=
  KNN.fromData Float String 2 3 [
    (point 0.0 0.0, "blue"),
    (point 0.0 1.0, "blue"),
    (point 3.0 3.0, "orange"),
    (point 3.0 4.0, "orange")
  ]

#eval classify Float String 2 labels (point 0.2 0.1)
-- "blue"

The exported families deliberately expose different amounts of fitting and inference machinery:

These definitions execute directly when their scalar Context is executable, as Float is in the example. They are pure tensor/reference algorithms rather than automatic Trainer.new, compiled graph, LibTorch, or CUDA routes. Shape indices rule out dimensional mismatches, but they do not by themselves prove statistical assumptions, optimizer convergence, or a family-wide correctness claim; consult each declaration's hypotheses and result type, especially Option-returning GMM and HMM likelihood operations.

2.5.11. When To Import More🔗

Use:

import NN

when a file genuinely needs several lower layers, such as model code plus proof declarations and backend inspection.

Focused subsystem imports include:

import NN.Spec
import NN.Runtime
import NN.Floats
import NN.Verification
import NN.GraphSpec

Prefer the narrowest stable import that expresses the file's responsibility. A numerical theorem should not import the entire executable model zoo merely for convenience, and a training script should not depend on an internal tape constructor.

2.5.12. API Boundaries Are Semantic🔗

These objects may all refer to the same architecture:

The TorchLean API makes the common path concise without collapsing these meanings.

2.5.13. Find A Declaration🔗

Use the generated API search:

/docs/search.html

The path works on the published site and on a local site preview. For source search:

rg -n "def valueAndGradParamsScalar|theorem .*sound" NN

The API reference answers “what is the exact declaration?” The surrounding chapters explain why and when to use it. Source remains authoritative when a lower-level contract matters.

2.5.14. Continue From Here🔗

Run:

lake exe torchlean --help
lake exe torchlean quickstart_tensors
lake exe torchlean quickstart_autograd
lake exe torchlean quickstart_mlp --steps 20

These four commands cover the tensor, derivative, model, dataset, trainer, and prediction interfaces without requiring backend or proof internals.

Lean's source-file and module reference explains how these imports determine the environment in which a file elaborates. With the common path in one place, the next chapter keeps this same model and changes only how it executes.