Quickstart: Proving Small TorchLean Facts

Many TorchLean guarantees are ordinary Lean theorems. These examples cover:

• compile-time guarantees from shape-indexed tensor types, and
• ordinary mathematical lemmas about the public API, and
• derivative formulas checked against mathlib with autograd, and
• convergence of a quadratic's gradient-descent iteration with converges.

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

def NN.Examples.Quickstart.Proofs.twoTensor : TorchLean.Tensor Float [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 has type Tensor Float [2]. The commented shape mismatch below is the kind of bug Lean catches before runtime:

-- def badTensor : Tensor Float [3] := [1.0, 2.0]

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.

theorem NN.Examples.Quickstart.Proofs.mean_square_deriv (a b c : ℝ) : HasDerivAt (fun (t : ℝ) => (t ^ 2 + b + c) / 3) (2 * a / 3) a

Differentiate one coordinate of mean squared error, holding the other terms fixed.

theorem NN.Examples.Quickstart.Proofs.affine_loss_deriv (w₁ w₂ b t x₁ x₂ : ℝ) : HasDerivAt (fun (w : ℝ) => (w * x₁ + w₂ * x₂ + b - t) ^ 2) (2 * (w₁ * x₁ + w₂ * x₂ + b - t) * x₁) w₁

The weight gradient is twice the residual times the corresponding input feature.

A new function can reuse the same rules. Registration lets later proofs use its derivative without unfolding it. local keeps this tutorial's rule out of other modules' search sets.

noncomputable def NN.Examples.Quickstart.Proofs.smoothPenalty (x : ℝ) : ℝ

A smooth penalty combining a quadratic term with an exponential.

theorem NN.Examples.Quickstart.Proofs.smoothPenalty_deriv (x : ℝ) : HasDerivAt smoothPenalty (2 * x + Real.exp x) x

Prove the new function's rule before registering it for composition.

For the loss x² / 2, the gradient is x. Proving that derivative is one task; proving that repeated gradient steps reach zero is another. Here the step size must lie in (0, 2). These are exact-real statements, not claims about rounded runtime iterates.