7.7.1. Lab One: A Tensor Has A Shape And A Scalar Meaning🔗

Run:

lake exe torchlean quickstart_tensors

The current output is:

== Quickstart: tensor basics ==
[Float] [0.100000, 0.200000, 0.300000, 0.400000]
[ℚ] [1/10, 1/5, 3/10, 2/5]
[Int] [1, 2, 3, 4]
[IEEE32Exec] [0.100000, 0.200000, 0.300000, 0.400000]
[Float] [[[1.000000, 2.000000], [3.000000, 4.000000]],
         [[5.000000, 6.000000], [7.000000, 8.000000]]]
Expected failure printing Tensor ℝ: Refusing to print `Tensor ℝ` (proof-level);
cast to `Float`/`IEEE32Exec`/`ℚ` to display.

The first four tensors have the same vector shape and superficially similar entries, but their scalar meanings differ:

• Float is Lean's native executable floating-point value;

• ℚ is exact rational arithmetic;

• Int is exact integer arithmetic;

• IEEE32Exec is TorchLean's explicit executable IEEE-754 binary32 model;

• ℝ is suitable for proofs but is not an object the runtime should pretend to print.

The shape of the final tensor is 2\times2\times2. It is represented by nested, length-indexed dimensions, so the eight entries cannot accidentally be interpreted as a 4\times2 matrix without an explicit reshape proof.

Read TensorBasics.lean beside the output. Change one scalar type at a time and let Lean show which operations require a different algebraic context.

7.7.2. Lab Two: Reverse And Forward Differentiation🔗

The autograd quickstart uses a linear map from two inputs to three outputs. Run:

lake exe torchlean quickstart_autograd

For input

x=(0.5,-1.2),

the Jacobian of y=Wx+b with respect to W has three block rows. The command prints those rows:

jacrevOutParams rows = 3 (should be size(out)=3)
  row[0] dW = [[0.500000, -1.200000],
               [0.000000, 0.000000],
               [0.000000, 0.000000]]
  row[1] dW = [[0.000000, 0.000000],
               [0.500000, -1.200000],
               [0.000000, 0.000000]]
  row[2] dW = [[0.000000, 0.000000],
               [0.000000, 0.000000],
               [0.500000, -1.200000]]

That output is easy to check by hand:

\frac{\partial y_i}{\partial W_{jk}} =\begin{cases} x_k,&i=j,\\ 0,&i\ne j. \end{cases}

The same program then prints VJPs, JVPs, an HVP, a Hessian, and gradients through detach. The detach check is especially useful:

loss(mse ∘ detach) = 0.165133
gradParams (mse ∘ detach) gW = [[0.000000, 0.000000],
                                [0.000000, 0.000000],
                                [0.000000, 0.000000]]
gradParams (mse ∘ detach) gb = [0.000000, 0.000000, 0.000000]

The value is unchanged while the gradient path is cut. This is an executable check against a closed form, not by itself a theorem about every autograd operation. Proof coverage for individual forward and backward rules lives in the proof modules described earlier in the guide.

Source: AutogradBasics.lean.

7.7.3. Lab Three: Train A Small MLP🔗

The training quickstart generates 25 regression samples for a two-input, one-output function and uses a hidden layer of width eight.

lake exe torchlean quickstart_mlp \
  --device cpu --steps 20 --seed 2026

The command reports the same two probes before and after optimization:

== Quickstart: simple MLP training ==
seed  = 2026
steps = 20
dataset size = 25
mean_loss(before) = 0.761530
predictions(before)
  center:  x=(0.000000,0.000000)   target=0.200000  pred=[0.000000]
  heldout: x=(0.250000,-0.750000) target=0.200000  pred=[0.043283]
step 0: loss=0.000866
mean_loss(after) = 0.459876
predictions(after)
  center:  x=(0.000000,0.000000)   target=0.200000  pred=[-0.132460]
  heldout: x=(0.250000,-0.750000) target=0.200000  pred=[0.012967]
steps=20 loss0=0.761530 loss1=0.459876
predict(heldout) = [0.012967]

The step-zero loss belongs to the first streamed sample, while mean_loss covers the dataset. Their labels prevent those two statistics from being confused.

lake exe torchlean quickstart_mlp \
  --device cpu --dtype ieee754exec \
  --steps 2 --seed 2026

lake exe torchlean quickstart_mlp \
  --device cpu --steps 200 --seed 2026

mean_loss(before) = 0.761530
mean_loss(after) = 0.003234
heldout x=(0.25,-0.75), target=0.2, prediction(after)=[0.210239]

7.7.4. Lab Four: Learn From Data You Can See🔗

Before introducing files, downloads, or preprocessing scripts, it helps to train once on a dataset small enough to draw on paper. TorchLean's band samples are single-channel 4\times4 images. Class zero contains a vertical band; class one contains a horizontal band. Three offsets per class make the six training examples.

Run the compact classifier:

lake exe torchlean quickstart_cnn \
  --device cpu --steps 2 --batch 2 --seed 2026

The current run ends with:

dataset size = 3
mean_loss(before) = 0.689656
mean_loss(after) = 0.685960
steps=2 loss0=0.689656 loss1=0.685960
vertical-1 expected=0 = [[0.125427, -0.069819],
                         [0.125427, -0.069819]]

Why does a six-image dataset report size three? --batch 2 packs the samples into three batches. The final line repeats the same probe twice to form a batch and prints two logits per copy. The first logit is larger in this run, so the probe's predicted class is the expected vertical class. That is a useful sanity check, not an accuracy theorem.

The reusable definitions in NN.API.Data.Bands separate rendering from training. renderBand constructs one image from an axis, offset, and thickness; dataset combines any list of class descriptions and offsets; train and probes cast the concrete Float images into a supported scalar context. The quickstart uses the canonical four-by-four data through Data.Bands.dataset.

This tiny problem removes dataset provenance and parser behavior from the experiment, which makes it good for debugging model construction, batching, loss, and optimization. It does not tell us how the same CNN behaves on natural images. The CIFAR case studies earlier in this part address that different question.

Source: SimpleCnnTrain.lean.

7.7.5. Lab Five: Lower A Model And Bound Its Output🔗

The previous labs evaluated one concrete input at a time. Interval bound propagation starts from an input box

x\in[\ell,u]

and computes an output box enclosing every supported model evaluation in that region.

Run the registered workflow:

lake exe verify -- torchlean-ibp

Current output:

=== TorchLean → IR → IBP (small MLP) workflow ===
[TorchLean] Float32 mode: IEEE32Exec: executable IEEE-754 binary32 kernel
compiled IR nodes: 20
output box lo: [1.904000]
output box hi: [2.256000]

The path is:

TorchLean model
  -> canonical IR
  -> supported-operation check
  -> IEEE32Exec interval propagation
  -> output box

For an affine layer y=Wx+b, IBP separates positive and negative weights:

\begin{aligned} \ell'_i &=\sum_j \left(\max(W_{ij},0)\ell_j+\min(W_{ij},0)u_j\right)+b_i,\\ u'_i &=\sum_j \left(\max(W_{ij},0)u_j+\min(W_{ij},0)\ell_j\right)+b_i. \end{aligned}

For ReLU,

[\ell_i,u_i] \longmapsto [\max(0,\ell_i),\max(0,u_i)].

The command's result belongs to the supported IR fragment and numerical policy used by this workflow. It does not certify an arbitrary model command merely because that command also contains linear layers and ReLUs.

Discover the other registered workflows with:

lake exe verify -- list

The implementation of this path is reachable from NN/Verification/CLI.lean.

7.7.6. Lab Six: Replay A Numerical Certificate🔗

The numerical-certificate example moves from an in-memory bound result to a checked artifact. Run:

lake exe torchlean numerical_certificate

The command checks positive and negative cases:

TorchLean numerical runtime certificate
  ok  base certificate
  ok  base IEEE replay
  ok  tampered range rejected
  ok  misplaced source rejected
  ok  duplicate contract rejected
  ok  registry mismatch rejected
  ok  unsupported operation rejected
  ok  fixed-left reduction
  ok  portable matmul
  ok  CUDA matmul policy rejected
  ok  directed sqrt
  ok  negative sqrt domain rejected
  ok  portable LayerNorm
  ok  CUDA LayerNorm policy rejected
  ok  stable softmax
  ok  two-layer MLP certificate
  ok  two-layer MLP IEEE replay
All numerical certificate checks passed.

A certificate is useful only if malformed evidence is rejected. That is why the example includes a tampered range, an unsupported operation, a bad square-root domain, and numerical policies that do not match the declared backend.

The graph checker and its proof layer are:

• GraphNumericalCertificate.lean;

• NN.Proofs.RuntimeApprox.Graph.NumericalCertificate.

The certificate uses outward-rounded IEEE32Exec ranges and can replay concrete inputs in the bit-level interpreter. A native runtime remains a separate provider whose agreement requires the appropriate backend evidence.

To inspect the scalar boundary behind that certificate, also run:

lake exe torchlean float32_modes

It contrasts proof-level rounding, executable IEEE binary32 behavior, and native-runtime agreement on finite, exceptional, and non-associative examples. It is a semantics demonstration; the numerical-certificate command is the separate graph-level checker.

7.7.7. Lab Seven: An External Graph Producer🔗

TorchLean can ask PyTorch to export model graphs and then parse the resulting artifact:

lake exe torchlean pytorch_export_check

The command accepts supported examples such as small MLP, CNN, normalization, Transformer-shaped, and single-head-attention graphs. It deliberately rejects unsupported structures, including multi-head attention outside the currently implemented lowering fragment.

The important chain is:

Python/PyTorch producer
  -> JSON value graph
  -> Lean parser
  -> canonical TorchLean IR
  -> WellShaped result or explicit rejection

Acceptance proves that the parsed graph is well shaped through the parser theorem. It does not prove PyTorch's exporter, Python interpreter, or original model source correct.

Source: TorchExportCheck.lean.

7.7.8. Building The Example Suite🔗

Before changing maintained examples, build the curated umbrella:

lake build NNExamples

That checks elaboration across the example tree. It does not execute every long-running model or external dependency. Runtime regressions, CUDA checks, dataset preparation, and certificate replay remain separate validation steps.