Quickstart: Proving Small TorchLean Facts

TorchLean examples are not only executable scripts. Many guarantees are ordinary Lean theorems: shape round-trips, typed tensor construction, activation identities, and later full verification statements.

The boundary where TorchLean becomes more than an executable ML library is:

• compile-time guarantees from shape-indexed tensor types, and
• ordinary mathematical lemmas about the public API.

The deeper proof libraries live under NN.Proofs.*, NN.Verification.*, and NN.MLTheory.*.

def NN.Examples.Quickstart.Proofs.twoVector : TorchLean.Tensor.T Float (Tensor.shapeOfDims [2])

A tensor's shape is part of its type.

If this definition compiles, Lean has already checked that the literal has exactly two entries and therefore really is a Vec 2. The commented shape-mismatch below is the kind of bug Lean catches before runtime:

-- def badVector : Tensor Float (shape![3]) := tensor! [1.0, 2.0]

theorem NN.Examples.Quickstart.Proofs.matrix_shape_roundtrip : TorchLean.Shape.ofDims (Spec.Shape.toList (Tensor.shapeOfDims [2, 3])) = Tensor.shapeOfDims [2, 3]

Runtime dimension lists can still be related back to static TorchLean shapes.

This is the compact theorem behind many JSON/CLI/data-loader paths: parse dimensions dynamically, then recover the precise Shape used by the typed tensor API.

theorem NN.Examples.Quickstart.Proofs.relu_eq_self_of_nonnegative (x : ℝ) (hx : 0 ≤ x) : Activation.Math.reluSpec x = x

ReLU fixes every nonnegative real number.

theorem NN.Examples.Quickstart.Proofs.relu_eq_zero_of_nonpositive (x : ℝ) (hx : x ≤ 0) : Activation.Math.reluSpec x = 0

ReLU clamps nonpositive real inputs to zero.