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.

This file is intentionally small. It shows the two proof styles a new user should recognize first:

• 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 : Spec.Tensor 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 : Tensor.shapeOfDims (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 small 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) : API.Semantics.relu x = x

The host-side public ReLU agrees with the usual mathematical identity on nonnegative real inputs.

This is deliberately a small theorem, but it has the same form as larger library facts: state the semantic contract once, prove it in Lean, and use it downstream without trusting comments or tests.

theorem NN.Examples.Quickstart.Proofs.relu_eq_zero_of_nonpositive (x : ℝ) (hx : x ≤ 0) : API.Semantics.relu x = 0

ReLU clamps nonpositive real inputs to zero.