Tensors🔗

TorchLean uses one tensor type for specifications and execution:

-- The scalar type and shape are independent indices of the
-- same tensor interface.
Tensor α shape

Its runtime representation is one contiguous row-major buffer whose length is certified by shape. The scalar type chooses the physical buffer through Storage: executable scalar types can use packed native storage, while general proof scalar types use the generic representation.

Proofs do not reason about raw buffer offsets. A tensor coerces to a total function on the typed coordinate space of its shape, and extensionality says that tensors with equal values at every coordinate are equal. A vector coordinate contains Fin n, so out-of-range lookup cannot be expressed. Shape induction remains available through rank-zero observation and leading-axis slicing, but those are proof views and smart constructors over the same contiguous tensor, not a second recursive physical datatype. Public shapes still use [], [n], and [m, n].

Model code uses ordinary shape lists, and a linear layer is a structure with two fields:

Tensor ℚ [2] : Type

Tensor ℚ [3, 2] : Type

LinearSpec ℚ 2 3 : Type

For a linear map from two inputs to three outputs, LinearSpec ℚ 2 3 contains

W\in\mathbb{Q}^{3\times 2}, \qquad b\in\mathbb{Q}^{3}.

Output features index the rows of the weight matrix, following PyTorch's nn.Linear convention. Each row therefore contains the coefficients for one output coordinate. Keeping that layout in the specification lets an imported PyTorch weight matrix retain its interpretation. Paszke et al. (2019) documents that layout.

The three #check results describe types, not computed tensors. Tensor ℚ [2] fixes two rational coordinates, while Tensor ℚ [3, 2] fixes a matrix with three rows and two columns. The layer type then packages a matrix and bias with compatible dimensions. These indices prevent a caller from silently passing a tensor of a different shape, but they do not constrain the numerical values inside it. Positivity, normalization, and closeness to another tensor are separate propositions.

Scalar Operations And Algebraic Assumptions🔗

The shape fixes where values live. The scalar context fixes which formulas are available. A linear layer needs zero, addition, and multiplication. Softmax also needs exponentiation and division. Square root, comparison, trigonometric operations, and Boolean decisions require their own pieces of structure.

The signature separates the storage instance from the three arithmetic operations linearSpec uses:

@linearSpec : {α : Type} →
  [inst : Storage α] →
    [Add α] → [Mul α] → [Zero α] → {inDim outDim : ℕ} → LinearSpec α inDim outDim → Tensor α [inDim] → Tensor α [outDim]

reluSpec asks for zero, a maximum operation, and Boolean equality:

@Activation.reluSpec : {α : Type} →
  [inst : Storage α] → [Zero α] → [Max α] → [BEq α] → {s : Shape} → Tensor α s → Tensor α s

At zero, ReLU returns the scalar context's zero. For a dual number, this also sets its tangent to zero, matching TorchLean's selected derivative at the kink. Boolean equality selects that branch; away from zero, the definition uses the maximum operation.

Neither signature asserts algebraic or order laws for those operations. Changing the scalar instances changes how those operations are evaluated, so the same linear-layer definition can be used over integers, intervals, or binary32 bit patterns. Algebraic laws about those operations need their own hypotheses.

TorchLean packages the common operations in Context α, so the same tensor definition can be interpreted over reals, rounded formats, interval endpoints, or executable binary32. This polymorphism requires care when stating hypotheses. A proof of a softmax identity over ℝ may use properties of the real exponential that an arbitrary Context α does not provide.

The hypotheses depend on what we want to prove:

A field would be an unnecessarily strong requirement just to define the linear formula. A derivative theorem over the reals can ask for the analytic structure it needs later. Reusing the definition at another scalar type preserves the operation sequence; the laws available for reasoning about it depend on the chosen instances. Native execution also needs a contract relating that sequence to the provider's implementation.

Linear Layer Forward And Backward Rules🔗

The forward definition is deliberately short:

-- The definition exposes the matrix product and the
-- subsequent bias addition.
def linearSpec {α : Type} [Storage α] [Add α] [Mul α] [Zero α]
    {inDim outDim : Nat}
    (m : LinearSpec α inDim outDim)
    (input : Tensor α [inDim]) :
    Tensor α [outDim] :=
  addSpec (matVecMulSpec m.weights input) m.bias

At coordinate i, this means

y_i=\left(\sum_{j=0}^{\mathrm{inDim}-1}W_{ij}x_j\right)+b_i.

Take W=\begin{bmatrix}0.8&-0.4\end{bmatrix}, b=0.2, and x=(0.1,-1). By hand,

y_0=0.2+0.8\cdot\tfrac{1}{10}-0.4\cdot(-1) =\tfrac15+\tfrac{2}{25}+\tfrac25=\tfrac{17}{25}.

Over ℚ the definition returns that fraction, exactly:

[(17 : Rat)/25]

The stored result is the fraction 17/25. Both products and the bias addition were evaluated in ℚ, so there is no rounding error to separate from the formula in this example.

The backward specification receives an upstream cotangent g=\partial L/\partial y and returns

\frac{\partial L}{\partial W}=g\,x^\mathsf{T},\qquad \frac{\partial L}{\partial b}=g,\qquad \frac{\partial L}{\partial x}=W^\mathsf{T}g.

In Lean these three tensors have shapes [outDim, inDim] , [outDim] , and [inDim] . A transposed weight gradient has the wrong type when the input and output dimensions differ. For a square weight matrix, its shape alone cannot detect the transpose.

linearBackwardSpec returns all three in a Spec.LinearGradients record. Its named fields distinguish the weight, bias, and input gradients even when two of them have the same shape, as the bias and input gradients do in a square layer. Convolution uses Spec.ConvGradients for the same reason. For the second layer of our MLP, take a hidden activation of (\tfrac1{10},0) and a cotangent of 1:

{ weightGradient := [[(1 : Rat)/10, 0]], biasGradient := [1], inputGradient := [(4 : Rat)/5, (-2 : Rat)/5] }

Check each against the formula above. The weight gradient g\,x^\mathsf{T} is the hidden activation written as a row. The bias gradient is g unchanged, because \partial y/\partial b is the identity. The input gradient W^\mathsf{T}g is the weight row transposed. All three are exact rationals that can be compared directly with the three expressions.

The source definitions are linearSpec, linearWeightsDerivSpec, linearBiasDerivSpec, linearInputDerivSpec, and linearBackwardSpec in NN/Spec/Layers/Linear.lean. Later, the autograd proofs compare executable VJP rules with these definitions. The autograd proofs chapter states the agreement theorems and their assumptions.

We chose seed one to inspect the derivative of this scalar output. With seed two, every returned cotangent would double over the rationals. In a composed model, an earlier layer receives the cotangent produced by a later layer; it cannot assume that its own output is seeded with one.

MLP Forward Semantics🔗

The running model is the composition of two linear specifications and a pointwise activation. In the library it is assembled as a chain of module specs rather than as one nested expression:

@Examples.mlpSpec : {α : Type} →
  [inst : Storage α] →
    [Context α] →
      {inDim hidDim outDim : ℕ} →
        LinearSpec α inDim hidDim → LinearSpec α hidDim outDim → Module.Chain α [inDim] [outDim]

Examples.mlpForward runs that chain on one input vector. Give it the weights from the formula at the top of the chapter,

W_1=\begin{bmatrix}1&1\\-1&1\end{bmatrix}, \quad b_1=0,\quad W_2=\begin{bmatrix}0.8&-0.4\end{bmatrix}, \quad b_2=0.2,

and evaluate it at x=(0.25,-0.75):

[(1 : Rat)/5]

We can also evaluate the three stages separately:

[(-1 : Rat)/2, -1]

[0, 0]

[(1 : Rat)/5]

So W_1x=(-\tfrac12,-1), both preactivations are negative, ReLU sends the whole hidden layer to zero, and the output is the second bias alone: exactly \tfrac15. That the composed chain and the hand expansion print the same fraction is a small but real check that Module.Chain wiring means what the formula says.

These rational evaluations also predict which parameter changes can affect the output. As long as both hidden preactivations remain negative, changing the first layer or the second weight matrix leaves the output unchanged. Crossing an activation boundary opens a path through the hidden layer, as the bias perturbation below will show.

>>> # Inspect the gradient convention chosen at the ReLU
>>> # kink.
>>> x = torch.tensor(0.0, requires_grad=True)
>>> y = torch.relu(x); y.backward()
>>> x.grad.item()
0.0

((4 / 5, -2 / 5), 4 / 5, -2 / 5)

true

(1, 0)

Runtime And Specification Comparison🔗

The same inputs can now be evaluated at Float. Tensor.linear is the runtime operation and Spec.linearSpec is its pure specification; the following comparison checks their results for this input:

[0.680000]

[0.680000]

true

They agree here, and PyTorch agrees with both:

>>> # Match dtype and parameters before comparing the affine
>>> # result.
>>> import torch
>>> import torch.nn.functional as F
>>> from torch import nn
>>> F.linear(torch.tensor([0.1, -1.0], dtype=torch.float64),
...          torch.tensor([[0.8, -0.4]], dtype=torch.float64),
...          torch.tensor([0.2], dtype=torch.float64)).tolist()
[0.68]

The comparison covers one vector input. Tensor.linear also applies along the final axis of a tensor with leading dimensions, so a batch of rows comes back as a batch of rows:

[[0.680000], [0.200000], [0.600000]]

PyTorch, same call, same three rows:

>>> # Use binary64 here to match Lean Float in the preceding
>>> # calculation.
>>> W = torch.tensor([[0.8, -0.4]], dtype=torch.float64)
>>> b = torch.tensor([0.2], dtype=torch.float64)
>>> F.linear(torch.tensor([[0.1, -1.], [0., 0.], [1., 1.]], dtype=torch.float64),
...          W, b).tolist()
[[0.68], [0.2], [0.6000000000000001]]

The third row needs a closer comparison. PyTorch prints 0.6000000000000001 while TorchLean prints 0.600000. Comparing the stored TorchLean value with the literal 0.6 reveals a difference that its printer hides:

false

0.000000

The equality check establishes that TorchLean's stored result differs from the literal 0.6, although the subtraction still prints as 0.000000. PyTorch's longer decimal output exposes a difference that six decimal places hide. These displays alone do not establish that the two libraries stored identical bit patterns; that would require a bit-level comparison. Even this one-row affine calculation shows why formatted output is insufficient for an exact numerical comparison. Goldberg (1991) is the standard account, and the runtime approximation chapter states what TorchLean actually proves about the gap.

The executable examples run runtime tensors and an autograd tape. The nn.linear builder fixes the parameter shapes and emits the runtime linear operation, while the graph interpreter assigns .linear its linearSpec denotation. The VJP proof relates the selected backward rule to linearBackwardSpec. These connections use the same parameter layout and backward convention.

Native execution adds another boundary: a capsule records the planned provider and its declared obligations, and execution checks establish which provider actually ran. The capsule's evidence determines what is known about that provider's agreement with the specification.

The batch axes have a separate role from the feature axis: projectLast applies the affine map independently to each row. It introduces no reduction across rows, so the first row's value does not depend on the second row's features.

Bias Perturbation And ReLU🔗

Now change only the first bias, from 0 to 0.6. The first hidden preactivation moves from -\tfrac12 to \tfrac1{10}, so it survives ReLU, and the output becomes

0.8\cdot0.1+0.2=0.28=\tfrac{7}{25}.

Both claims check out:

[(1 : Rat)/10, -1]

[(7 : Rat)/25]

\tfrac{7}{25} is exactly 0.28. A Float result printed as 0.280000 would need a separate comparison of its stored value, as the preceding example showed.

Interval propagation extends this calculation from one point to a set of possible inputs, bounding each intermediate tensor. The sign change is the important event here: the first hidden unit contributed zero before the bias changed, then contributed 1/10 afterwards. For an input region, we must determine which preactivation intervals stay on one side of zero and which can cross it. That is part of the analysis that the verification chapter formalizes.

Within either fixed activation region the model is affine. An analytic proof can use that formula once it has established the branch conditions. At the boundary, it must distinguish the selected backward rule from ordinary differentiability.

Scalar Polymorphism🔗

The type parameter \alpha determines what the symbols +, *, max, exp, and division mean. TorchLean reuses the tensor structure at several scalar interpretations:

Context ℚ is a scoped instance in Context/Rational.lean, which is why the MLP evaluation above had to write open scoped Spec.RationalAlgebraic to get at it. The real exponential does not in general return a rational, so this algebraic context supplies zero placeholders for the transcendental operations:

(0, 0)

Evaluating softmax with these placeholder transcendental operations produces:

[0, 0, 0]

The entries sum to zero, so this result cannot be interpreted as a probability distribution. The tensor calculation typechecks, but the real-exponential laws used to justify softmax do not hold for these placeholder operations. The scoped instance requires a file to opt in to the rational algebraic interpretation; callers still need to restrict its use to the supported algebraic fragment.

With the real exponential, softmax has the formula

\operatorname{softmax}(x)_i= \frac{\exp(x_i-m)}{\sum_j\exp(x_j-m)},\qquad m=\max_jx_j

For finite binary32 inputs, max selects an existing value without rounding. Subtraction, exponential approximation, summation, and division can introduce error. A CUDA reduction may also choose a different summation tree. The floating-point chapter and the runtime-approximation chapter state the conditions under which one interpretation encloses or approximates another; Boldo and Melquiond (2011) and Boldo et al. (2015) develop related formal accounts of rounding and numerical error in Rocq. An executable softmax needs a relation between its scalar operations and the real operations in this formula.

(10000000000000003, 10000000000000003)

(10000000000000000.000000, 10000000000000002.000000)

The Implemented Specifications🔗

The spec layer is broader than the running MLP. NN.Spec.Layers contains typed meanings for linear algebra, rank-polymorphic convolution, transposed convolution, and pooling, activations and losses, normalization, dropout, embeddings, recurrent cells, selective scan, and scaled dot-product attention. Model definitions under NN.Spec.Models compose these operations into families such as CNNs, transformers, recurrent networks, and state-space models.

An operation can have a pure definition before it has an eager tape rule, typed graph lowering, a CUDA kernel, or an end-to-end correctness theorem. The runtime and lowering chapters identify the operations supported by each route.

Shapes And Element Types🔗

The shape index s and element type \alpha answer different questions. Tensor α s fixes both for one value, and Graph.denote follows the homogeneous-element contract from Tensors And Shapes. The later IR chapter uses “heterogeneous” only for a table of differently shaped values, not for a mixed-dtype graph.

Specification Conventions🔗

Shapes are only one source of ambiguity. The spec layer also fixes choices that a model name does not determine. Each subsection below is a place where two reasonable libraries could differ, so the definition has to say which one TorchLean means.

144 / 625

[[true, false, false], [true, true, false], [true, true, true]]

[[1.000000, 0.000000, 0.000000], [0.268941, 0.731059, 0.000000], [0.090031, 0.244728, 0.665241]]

>>> # Apply the same causal support to the comparison
>>> # tensor.
>>> scores = torch.tensor([[0., 1., 2.]] * 3, dtype=torch.float64)
>>> causal = torch.ones(3, 3, dtype=torch.bool).tril()
>>> F.softmax(scores.masked_fill(~causal, float('-inf')), dim=-1).tolist()
[[1.0, 0.0, 0.0],
 [0.26894142136999516, 0.7310585786300049, 0.0],
 [0.09003057317038045, 0.2447284710547976, 0.6652409557748218]]

[1.000000, 0.000000]

[0.500000, 0.500000]

[0.000000, 1.000000]

[1.000000, 0.000000]

>>> # The comparison uses the same two score choices as the
>>> # Lean example.
>>> F.softmax(torch.tensor([0., 1000.]) + torch.tensor([0., -1000.]), dim=-1)
tensor([0.5000, 0.5000])
>>> F.softmax(torch.tensor([1., 1200.], dtype=torch.float64)
...           + torch.tensor([0., -1000.], dtype=torch.float64), dim=-1)
tensor([3.7618e-87, 1.0000e+00], dtype=torch.float64)

[0.000000, 0.000000]

2

[2, 0, 6, 0]

[1.000000, 2.000000, 3.000000, 4.000000]

>>> # Use inference mode explicitly when checking the
>>> # identity behavior.
>>> x = torch.tensor([1., 2., 3., 4.])
>>> F.dropout(x, p=0.5, training=False).tolist()
[1.0, 2.0, 3.0, 4.0]

28

14

[12, 12]

>>> # Check the corresponding convolution shapes in the
>>> # comparison API.
>>> nn.Conv2d(1, 1, 3, stride=1, padding=1)(torch.zeros(1, 1, 28, 28)).shape
torch.Size([1, 1, 28, 28])
>>> nn.Conv2d(1, 1, 5, stride=2, padding=0)(torch.zeros(1, 1, 28, 28)).shape
torch.Size([1, 1, 12, 12])

0

0

>>> # The execution API may reject a configuration whose
>>> # total shape formula returns zero.
>>> nn.Conv2d(1, 1, 5, stride=1, padding=0)(torch.zeros(1, 1, 3, 3))
RuntimeError: Calculated padded input size per channel: (3 x 3). Kernel size: (5 x 5).
Kernel size can't be greater than actual input size
>>> nn.Conv2d(1, 1, 3, stride=0, padding=1)(torch.zeros(1, 1, 8, 8))
RuntimeError: non-positive stride is not supported

MLP Specification Equivalence🔗

GraphSpec's checked MLP uses the same four parameter tensors:

-- The ordered parameter roles matter even when two entries
-- have equal shapes.
[W₁ : [hidden, input],
 b₁ : [hidden],
 W₂ : [output, hidden],
 b₂ : [output]]

The theorem NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward proves that interpreting that GraphSpec model is equal to the hand-written two-layer specification, for every parameter pack and every input, at every scalar type with Storage and Context instances:

'NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward' depends on axioms: [propext, Classical.choice, Quot.sound]

Those three are Lean's standard classical foundations, also used by Community (2020). The theorem adds no TorchLean-specific axiom or unproved placeholder.

The conclusion identifies the pure GraphSpec interpretation with W_2\operatorname{ReLU}(W_1x+b_1)+b_2. A bound on that interpretation can therefore be read as a bound on this formula, with the same parameters and input. Connecting it to an imported checkpoint, an eager tape, or a CUDA execution requires the corresponding import and runtime arguments.

Sources🔗

The definitions used in this chapter, in the order they appeared:

• Layers/Linear.lean, LinearSpec and the four forward and backward definitions;

• Layers/Activation.lean, reluSpec, softmaxVecSpec, and the log-softmax family;

• Layers/Attention.lean, causalMask, hardMaskedMax?, and hardMaskedSoftmaxSpec;

• Layers/Dropout.lean, dropoutKeepScale and the masked and inference specifications;

• Layers/Conv.lean, the window geometry;

• Models/Mlp.lean, mlpSpec and mlpForward;

• Core/Context/Rational.lean, the scoped rational backend;

• MlpSpecEquivalence.lean, the equivalence theorem.

The next chapter turns these formulas into typed architectures with explicit parameter layouts.