Tensor Values And Shapes🔗

From the repository root, run:

# Run the same tensor constructions across the executable
# scalar types shown below.
lake exe torchlean quickstart_tensors

The output is:

== Quickstart: tensor basics ==
Rank-zero tensor: 0.500000
Float tensor:    [0.100000, 0.200000, 0.300000, 0.400000]
Rational tensor: [(1 : Rat)/10, (1 : Rat)/5, (3 : Rat)/10, (2 : Rat)/5]
Integer tensor:  [1, 2, 3, 4]
Float32 cast:    [0.100000, 0.200000, 0.300000, 0.400000]
Rank-3 tensor:   [[[1.000000, 2.000000], [3.000000, 4.000000]],
                  [[5.000000, 6.000000], [7.000000, 8.000000]]]
Reshaped matrix: [[0.100000, 0.200000], [0.300000, 0.400000]]

The first line is a rank-zero tensor written directly as Tensor Float [] := 0.5. The three length-four tensors show that the same shape can carry different scalar meanings. ℚ displays exact fractions, Float is Lean's host binary64 type, and Float32 uses Lean's native binary32 operations. The final two lines show a rank-three literal and a shape-checked tensor reshape.

The complete program is in TensorBasics.lean, and the following definitions develop the same ideas one operation at a time.

Everything from here on assumes these two lines at the top of the file:

-- The application import supplies the tensor constructors
-- and public shape notation.
import NN.API
open TorchLean

These imports cover the application examples. The theorem examples later in the chapter also require NN.Proofs.Tensor.Algebra and NN.Proofs.Tensor.Basic; the explicit float example uses FloatLib. We write ExecFloat for FloatLib.Floats.ExecFloat.

Tensor Type🔗

There are two independent questions to ask of a tensor: what is one entry, and how are entries indexed? In Tensor Float [4, 2], Float answers the first and [4, 2] answers the second. Changing the scalar type can change rounding and available arithmetic without changing any coordinate. Changing the shape can change which coordinates are meaningful even when every stored scalar remains the same. Keeping these questions separate makes later conversions, reshapes, and model signatures easier to read.

The canonical type is:

\operatorname{TorchLean.Tensor}\;\alpha\;s.

The application-facing spelling for concrete dimensions is Tensor α [dims...]. The first parameter is the element type; the second is the dimension list. All four of these are well-formed types, and Lean accepts them without any further annotation:

Shape-polymorphic code may use a variable for the complete shape, as in Tensor α s. This is the same tensor type, with s standing for the dimension list rather than writing its entries out.

Public tensor annotations use list syntax. Shape operations such as concatenation, axis lookup, and size calculation preserve that representation in application code.

[4, 2] says only that the tensor has four rows and two columns. It does not carry or infer a dtype. Lean obtains the element type from Tensor's first argument, or infers it from the value on the right-hand side when the annotation is omitted.

The trainer's arithmetic choice selects the instantiated executable element type and its arithmetic semantics. For example, arithmetic := .native instantiates the model at Lean 4.34's native Float32; it does not reinterpret an already constructed Tensor Float [4, 2]. Device storage is a further backend contract: TorchLean's CUDA path stores native Float32 model values as contiguous binary32 data. Keeping shape, arithmetic semantics, and device representation distinct prevents a shape annotation from silently deciding numerical behavior.

Shape literals are written from the outermost dimension to the innermost one:

[] is the public rank-zero shape. Shapes print in this same bracket notation, so editor output, diagnostics, and repr never require the inductive constructor spelling.

A rank-zero tensor also uses ordinary numeric syntax:

An empty dimension list has one coordinate: choosing no axis positions leaves the scalar itself. That is why [] is the shape of a scalar tensor. It differs from [0], a vector with no entries. The distinction matters for a loss function, whose output is one scalar even when the input has many axes. The following two evaluations print that sole value; the brackets disappear because there is no vector or matrix axis to display.

0.500000

3

The two printed values already say something about element types. Float renders through Lean's host binary64 formatting, so 0.5 comes back as 0.500000; Rat renders as an exact integer because three is exactly representable and no decimal expansion is involved.

There is no separate public scalar-tensor format. [] says that the tensor has no axes, while the element type still determines whether its single value is native floating point, exact rational arithmetic, an executable IEEE reference, or a proof-level number.

rankFourShape is a shape value that describes an ordinary rank-four tensor. Axis meanings come from the operation or model: [batch, channel, height, width] and [batch, height, width, channel] are two layout conventions over the same tensor type (He et al., 2016). The same tensor core can represent language tokens (Vaswani et al., 2017), PDE grids (Li et al., 2021), volumetric data, batched matrices, or an unusual scientific coordinate system.

Certified Contiguous Representation🔗

A tensor owns one contiguous row-major buffer. Its erased proof field certifies that the physical buffer length is exactly the number of scalar coordinates in its static shape. Storage α selects that physical buffer: Float uses FloatArray, UInt8 uses ByteArray, and arbitrary scalar types use the default Array α storage unless a custom instance selects another representation.

The tensor also acts as a total function from an in-bounds coordinate to a scalar. This observation view is what statements and proofs use; it does not allocate a second recursive tensor at runtime. The type therefore gives us three facts:

• every axis has the length written in the shape;

• every legal index carries its own bounds proof;

• definitions and proofs can reason extensionally over all valid coordinates.

For example, Tensor.map changes the element type while preserving every dimension:

TorchLean.Tensor.map {α β : Type} [Storage α] [Storage β] {shape : Shape} (f : α → β) (tensor : Tensor α shape) :
  Tensor β shape

Read that signature from the right: shape is bound once and appears in both the argument and the result. The result shape is therefore fixed before any values are evaluated, and no runtime check can disagree with it. Tensor.map traverses the contiguous buffer once and preserves the certified shape.

The two Storage arguments allow different physical representations on input and output. At each coordinate, map reads an α, applies f, and stores a β. A numeric conversion can therefore change the storage without changing which coordinate an entry occupies.

Tensor Literals And Shape Checking🔗

Ordinary bracket syntax constructs a tensor whenever the expected type is a positive-rank Tensor. The elaborator checks every visible dimension:

Here the correction at row zero, column one belongs to the score at row zero, column one. The resulting entry is 2.0 + (-0.1), printed below as 1.900000. There is no search for an axis along which to broadcast the correction: both tensors already have shape [2, 2]. Writing a matrix-shaped correction makes the correspondence explicit even if a later version of the program changes the values or reads them from a file.

Lean's #eval command uses the tensor's custom shape-aware Repr instance, so a tensor expression can be inspected directly:

[[1.000000, 2.000000], [3.000000, 4.000000]]

[[1.200000, 1.900000], [3.000000, 4.300000]]

No container conversion is involved. IO.println (reprStr adjusted) uses the same rendering in an IO program. Use the single typed boundary Tensor.to value TargetType only for serialization, interoperability, and other APIs that explicitly request a different container:

#[1.200000, 1.900000, 3.000000, 4.300000]

The flattened array is the clearest evidence that the literal is stored in row-major order: the last index changes fastest, so the flat order here is 1.2, 1.9, 3.0, 4.3. Tensor.to also accepts List Float and Vector Float (Spec.Shape.size [2, 2]); a vector's length is part of its type, so the target states the tensor's certified element count. Packed targets are available when their element type matches: FloatArray for Float and ByteArray for UInt8. The target type is an ordinary Lean argument: choose the container the receiving API expects.

Rank-zero tensors are the one case that does not need brackets:

The expected tensor type directs the ordinary numeric literal into the certified one-element buffer.

Rectangularity and shape compatibility are separate requirements. The next two examples violate one requirement each, and Lean rejects both while elaborating the file:

tensor literal has leading dimension 1, but the expected leading dimension is 2

The literal is not rectangular. The elaborator descends into the second row, finds one entry where the shape promises two, and reports the dimension it was checking rather than a generic "bad literal" message.

tensor literal has leading dimension 2, but the expected leading dimension is 4

The second literal has four values but the wrong structure: its outermost dimension has length two, while [4] requires a single axis of length four. Equal element counts permit an explicit reshape; they do not make a matrix and a vector interchangeable.

When the element type is ambiguous, make it explicit:

One-dimensional literals use the same notation:

Literals are for small, hand-written data. Constant tensors come from Tensor.zeros, Tensor.ones, and Tensor.full; values that already exist in memory come from Tensor.from, which reads the source's intrinsic shape and therefore needs no failure branch; and tensor.reshape reinterprets an existing buffer at another shape of the same size. Loaders that receive a claimed shape from a file or a network payload are the one place where a check is unavoidable, and they get their own section below.

Arithmetic On Tensors🔗

A weighted score connects pointwise arithmetic to reduction. Multiplication computes the contribution of each feature; summation combines those contributions into a scalar:

* multiplies matching entries and keeps the shape. It is not a matrix product:

[2.000000, -3.000000, 2.000000]

+, -, and / behave the same way, and Tensor.add, Tensor.sub, Tensor.mul, and Tensor.div are the named spellings of the same four operations.

Adding those three products is a reduction: it consumes every entry and returns one scalar.

1.000000

Multiply and then sum is the dot product, and TorchLean defines it once under that name:

1.000000

@Tensor.dotSpec : {α : Type} → [inst : Storage α] → [Context α] → {s : Shape} → Tensor α s → Tensor α s → α

Two details in that signature are deliberate. The shape s is arbitrary rather than a single axis, so the definition is "sum of elementwise products over all coordinates" and it applies to matrices and higher-rank tensors as written. And the definition really is sumSpec (mulSpec a b): one line, used both by the executable path that produced 1.000000 above and by the theorems in NN/Proofs/Tensor/Algebra.lean. The Spec suffix marks a definition that specifications and proofs quote directly. It does not mean "not executable", and runtime dot and contraction kernels have separate implementations whose relation to this reference must be established by their contracts.

The three lines that follow are the PyTorch spelling of the same three steps (Paszke et al., 2019):

# The Python expressions separate elementwise products from
# their scalar reduction.
weights = torch.tensor([0.5, -1.5, 2.0])
features = torch.tensor([4.0, 2.0, 1.0])

weights * features          # tensor([ 2., -3.,  2.])
(weights * features).sum()  # tensor(1.)
torch.dot(weights, features) # tensor(1.)

torch.dot raises at run time if either argument is not one-dimensional, while Tensor.dotSpec accepts any shape and rejects a mismatch between the two arguments during elaboration. The reduction order is also part of TorchLean's definition: Tensor.sum folds left to right over the row-major coordinates. Floating-point addition is not associative (Goldberg, 1991), so a different fold order is a different function, and pinning it down is what lets the floating-point chapter state error bounds about this exact sum.

Matrix products are separate operations because they contract an axis instead of matching one:

[-2.000000, -2.000000]

[[4.000000, 5.000000], [10.000000, 11.000000]]

The first result uses direction to subtract each row's final entry from its first: 1 - 3 and 4 - 6 both give -2. In the matrix product, the columns of basis instead select two combinations of each row. Its first column adds the first and third entries, giving 4 and 10; its second adds the second and third, giving 5 and 11. The surviving row axis therefore still has length two, while the new column axis has length two because basis has two columns.

[5.000000, 7.000000, 9.000000]

The two ones in rowWeights add the rows of frame. Each output position is one column sum, so the three entries are 1 + 4, 2 + 5, and 3 + 6. This is a different contraction from matvec: the length-two input weights rows, while direction weights the three columns.

Tensor.matmul has type Tensor α [m, n] → Tensor α [n, p] → Tensor α [m, p], so the shared inner extent is a single variable n and a mismatch is a type error rather than a runtime exception. Tensor.matvec and Tensor.vecmat are the two one-sided cases; PyTorch reaches all three through torch.matmul and decides which one it means from the ranks it sees at run time.

Whole-tensor reductions ignore the axis structure:

21.000000

3.500000

The sum visits all six entries, giving 1 + 2 + 3 + 4 + 5 + 6 = 21; the mean divides that total by six. Neither result retains a row or column axis. If the next calculation needs one number per row, reducing the entire tensor loses the grouping it needs. The named-axis reduction below keeps the row axis and removes only the column axis.

failed to synthesize instance of type class
  HAdd (Tensor Float [2, 3]) (Tensor Float [3]) ?m.4

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Total Indexing🔗

Specification-level indices use Fin, so every index includes a proof that it lies inside its axis. Indexing therefore does not return Option or throw an out-of-range exception. The result type also records which axis was removed. Runtime APIs that receive an unchecked natural-number index validate it at the boundary before constructing the corresponding typed operation.

3

The by decide in each index is the bounds proof, discharged by computation because the bound is a literal. In shape-polymorphic code the same position holds a hypothesis from the surrounding theorem instead.

The returned 3 comes from row one, column zero: the second row is [3, 4], and its first entry is selected next. After the first indexing operation the type is a length-two row tensor; after the second, it is the scalar element type Nat. The bounds are attached to the indices before either selection occurs. This lets a function accept an arbitrary Fin 2 without rechecking it, even when the function cannot know which of the two valid positions it will receive.

A complete typed coordinate can be passed to tensor.at for a direct scalar read. Chained indexing first constructs the selected row tensor, so it can incur the cost of an intermediate slice. The immutable tensor.set coordinate value and tensor.modify coordinate f operations preserve the static tensor type. Packed Float and UInt8 tensors use native copy-on-write updates, which can reuse a uniquely owned buffer; other element types use the general array-backed implementation. Their semantic laws are available to the simplifier, including (tensor.set coordinate value).at coordinate = value.

Unchecked coordinate arrays cross an explicit validation boundary: tensor.at? #[...], tensor.set? #[...] value, and tensor.modify? #[...] f return none when the rank or a bound is wrong.

This is useful in proofs: a theorem about a tensor with one or more dimensions introduces an arbitrary valid index and applies its induction hypothesis to the smaller tensor selected there.

Trusted Memory And External Data🔗

An in-memory array already has an intrinsic length, so converting it is total:

The shape in the result type mentions xs.size, which is why no failure branch is needed: the length is read off the value that was handed over rather than promised separately.

This result type is useful even when xs.size is not known until execution. “In the type” does not mean “written as a numeral in the source”: Lean can express a result whose dimension depends on an argument's value. A caller that accepts any vector length can use asVector directly. A caller that specifically requires four entries needs the extra comparison in loadTensor4. The two constructors answer different questions about the same array.

A file or network payload additionally claims a shape. That claim must be checked at the external boundary:

An input with four entries reaches the successful branch; a shorter input returns the size mismatch without constructing a Tensor Float [4]:

Except.ok [1.500000, 2.500000, 3.500000, 4.500000]

Except.error "expected 4 values, found 1"

The proof argument to reshape connects the runtime check to the static result type. Tensor.from xs has shape [xs.size], so reshaping it to [4] requires Shape.size [xs.size] = Shape.size [4], and simp [Shape.size, h] supplies it from the branch hypothesis h : xs.size = 4. Lean solves this obligation by itself when both shapes are literals; here one of them is not, so the proof is written out. That single runtime comparison establishes the length, and the proof lets downstream code use that fact through the tensor's type.

Only the parser or loader needs the failure branch. Once it has established the scalar count, the ordinary Tensor.from and zero-copy reshape operations finish construction.

This is a recurring TorchLean pattern:

-- Validation is the step that turns a runtime payload into
-- a value with a checked type.
untyped external payload
  -> parser
  -> runtime validation
  -> typed Lean object
  -> theorem or model API

The check proves something about the accepted payload. It does not prove that every future file is valid, and it does not certify the code that produced the file.

Scalar Types And Arithmetic Semantics🔗

These tensors have the same shape and different semantics:

The trainer's arithmetic field selects executable arithmetic for the run. Proofs instantiate tensors over ℝ or Floats.FP32 directly; those noncomputable types do not appear as command-line runtime choices. The generic runtime can execute complex scalar programs, but the supervised trainer only offers its two real modes. Explicit complex training uses autograd.complex.grad for a real loss, with both components retained in the state, predictions, and checkpoints. FloatLib formats use the same tensor construction API. Select binary32 and construct the decimals directly in that format:

#[1036831949, 1045220557, 1050253722]

FloatLib exposes the stored bit patterns, making the rounding in the conversion visible. The first entry, 1036831949, is 0x3DCCCCCD, and the real number it denotes is 0.100000001490116119384765625, not 0.1. The floating-point chapter uses this gap to introduce rounding error.

(true, true, true)

Mixed Element Types🔗

Tensor α s is homogeneous: it cannot place an Int, FP16 value, and FP32 value in different entries. Different tensors may still have different element types. Pointwise +, -, *, /, Tensor.add, Tensor.sub, Tensor.mul, and Tensor.div automatically choose the registered common type:

[1.500000, 3.500000, 5.500000]

The result is homogeneous Float; promotion and arithmetic happen together while the output buffer is built. TorchLean's built-in promotion order is UInt8 < Nat < Int < Rat < Float32 < Float. A custom scalar participates by registering ElementCast and ElementPromotion instances. Use tensor.cast TargetScalar when conversion is the operation you intend rather than a consequence of binary arithmetic.

This promotion chain covers the registered real numeric scalar families. Proof-oriented or domain-specific scalars such as Real, configured FloatLib binary formats, and Complex α remain valid homogeneous tensor elements, but mixed arithmetic for a new pair requires an explicit promotion instance so TorchLean never invents numerical semantics.

Current model programs and NN.IR.Semantics select one numeric α for learned parameters, activations, and outputs. Scalar polymorphism means the same definition can be interpreted again at another α. Integer indices and boolean masks use dedicated operation interfaces so they are not silently treated as differentiable numeric tensors.

Checked Shape Patterns🔗

Importing NN.Tensor or NN exposes the complete shape-pattern API on the same ordinary Tensor type. The pattern keywords are scoped syntax activated by open TorchLean.Tensor; the expand form is the einops repeat operation under a name that does not collide with Lean's repeat:

The literal pattern and every static input or output shape are checked while Lean elaborates the definition (de Moura and Ullrich, 2021). The output names select and order dimensions from the inputs, so the inferred result type records the output shape and a conflicting annotation is rejected before execution. The shape-pattern operations above do not need result annotations: Lean infers their tensor shapes, as these checks show:

transposed : TorchLean.Tensor Float [3, 2]

product : TorchLean.Tensor Float [2, 4]

For the definitions above, Lean infers:

Here are the transposed tensor and the parsed dimension names:

[[1.000000, 4.000000], [2.000000, 5.000000], [3.000000, 6.000000]]

[("row", 2), ("column", 3)]

The macros read matrix : Tensor Float [2, 3] and right : Tensor Float [3, 4] while elaborating the file, bind pattern names to those dimensions, and synthesize the result type. The implementation receives a fully checked operation after elaboration. The regression suite deliberately defines all eight results without result annotations and then checks them against the types in this table. Multi-input einsum and pack automatically promote registered element types just as ordinary arithmetic does. pack retains the exact star shapes needed by unpack, so the round trip does not repeat dimensions or expose an anonymous tensor-metadata pair. parse_shape returns ordinary named dimension data, here [("row", 2), ("column", 3)], rather than a new tensor.

The transpose output is a useful check on the pattern's meaning: [1, 4] is the original first column, now printed as a row. Merely reshaping the same six flat values to [3, 2] would group them as [1, 2], [3, 4], [5, 6], which is a different operation. The type [3, 2] alone cannot distinguish those results. The pattern supplies the coordinate correspondence, while the type checks that its dimensions fit.

Packing preserves a different piece of information. The flat payload has eight values, but eight alone does not say where the length-two component ends or how to reconstruct the matrix. The recorded star shapes retain that partition. Choosing component zero or one in restored then recovers its respective type, so downstream code can consume a vector and a matrix without guessing their original boundaries from a single flattened buffer.

Tensors And Arrays🔗

TorchLean uses Tensor for numerical data. A length-n value has type Tensor α [n], including when n is computed at runtime. The shape already records its length, so it does not need a separate Vector wrapper. Arrays remain useful for JSON decoding and collections of heterogeneous records; numerical algorithms consume tensors after decoding.

Lists in types such as Tensor α [batch, width] are shape syntax. They also index dependent parameter packs whose tensors have different shapes.

Tensor.window takes a one-dimensional tensor and constructs a fixed-length slice, filling positions beyond its end with the supplied padding value:

[20, 30, 40, 50]

[20, 0, 0, 0]

The result length is the length argument in the type. offset selects the first input coordinate, and pad fills positions beyond the input. The second call explains why the operation is total: a window that runs off the end of a short tensor still has the promised length, and the pad value is visible in the source rather than chosen by the implementation. The constructor works for every registered storage, including packed floats and bytes, exact rationals, executable IEEE references, and boxed complex values.

At offset one, the long input supplies positions one through four. The short input supplies only position one; the other three requested positions become padding. Thus [20, 0, 0, 0] describes an explicit data transformation, rather than evidence that the source contained four values. For a sequence model, the program must still decide whether padding participates in attention or the loss. A fixed output shape makes the window easy to consume, while the padding policy determines what its values mean.

Runtime Tensor Storage🔗

The tensor is also the native CPU representation. Users still write and receive Tensor α shape. A CPU eager node internally stores SomeTensor α, which pairs one runtime shape with a Tensor α shape. This shape erasure lets one autograd tape contain activations and gradients of different shapes in a single array. Recovering a typed tensor requires checking the stored shape before exposing the value.

TensorPack α shapes solves a different problem. It is a statically heterogeneous tuple: the full list of member shapes remains in its type. Model parameters, gradients, and typed graph contexts use it when a fixed collection contains tensors of different shapes. It does not erase shapes, and it is not an alternative input or output tensor type.

For example, the two weights and two biases of a small MLP have four different positions in a known state layout. A TensorPack can describe that whole layout statically. An eager tape, however, grows as operations execute and may contain a matrix, a vector, and a scalar loss. SomeTensor lets those entries share an array while retaining each entry's runtime shape. Both wrappers contain ordinary tensors; the difference is how much of the collection's structure the surrounding program knows before execution.

A model program does not pass those values around directly while it records a computation. It uses Runtime.ValueRef m α shape, a shape-indexed handle owned by one session. Reading the handle returns the corresponding tensor value. It has no meaning in another session and is not a second tensor datatype. Session-backed runtime handles carry an owner token and recording generation; operations reject handles from another session and handles retained across resetTape.

CUDA execution is the one place where the physical representation must differ. An AnyBuffer contains a runtime shape and a native device buffer in contiguous row-major order. Upload and download functions connect it to Tensor; CUDA tape operations validate the stored shape and buffer size before dispatch. Proofs about graph evaluation and explicit kernel contracts cover the operations for which TorchLean has established a bridge. The native CUDA compiler, driver, and hardware remain named external boundaries rather than being treated as consequences of the tensor definition.

Linear Layers And Prefix Dimensions🔗

PyTorch's Linear(in_features, out_features) acts on the last axis (Paszke et al., 2019). TorchLean follows that useful convention while checking the complete map. The same layer constructor, with an explicit prefix argument when needed, supports:

-- The last axis changes width while every leading batch or
-- sequence axis is retained.
[2]              -> [8]
[batch, 2]       -> [batch, 8]
[batch, time, 2] -> [batch, time, 8]

Use nn.linear 2 8, nn.linear 2 8 [batch], or nn.linear 2 8 [batch, time] respectively. The prefix defaults to []; it is not inferred backwards from a surrounding model annotation. Any leading shape can serve as the prefix; it need not mean “batch” or “time.” One linear definition therefore works for single examples, minibatches, sequences, and higher-rank collections.

The value-level operation behaves the same way. A linear map acts on the final input axis and preserves every leading axis:

projected : Tensor Float (Shape.replaceLast [2, 4, 3] 5)

Lean prints the shape computation Shape.replaceLast [2, 4, 3] 5 without reducing it to [2, 4, 5]. These expressions are definitionally equal: evaluating the shape function gives the literal shape.

There are eight length-three vectors in activations: two choices on the first axis and four on the second. Each meets the same five rows of projection, producing five output features, and each receives the same length-five bias. Nothing in this operation mixes the eight leading positions. ReLU then changes individual output values while preserving all three axes. This example uses zeros to keep the values incidental; the #check result is about the shape of that whole composition. An annotation can therefore use the shorter spelling without an explicit proof:

The input's final extent fixes the input width as three; the weight fixes the output width as five; and Tensor.linear replaces only that final extent. A mismatched weight is rejected during elaboration, and the message names the exact obligation that failed:

failed to synthesize instance of type class
  Shape.EndsWith 4 [2, 4, 3]

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Shape.EndsWith 4 [2, 4, 3] identifies the mismatch: the weight requires a final input width of four, while the activations have width three.

The same check applies one level up. Change the second linear layer in the quickstart MLP from nn.linear 8 1 to nn.linear 7 1 without changing the preceding layer, and the sequential model no longer composes: one layer produces a last dimension of eight while the next requires seven. The error appears when the model is defined, before initialization, data loading, or training.

Reshaping🔗

A reshape from [2,3] to [6] is permitted because both shapes contain six values. It still needs an explicit operation because the indexing interpretation changes. Conversely, reshaping [2,3] to [2,4] is impossible because the element counts differ.

The layout convention matters at the representation boundary. In row-major order:

\operatorname{flatIndex}(i,j)=3i+j

for a 2\times 3 matrix. A column-major native library would use a different equation. Shape equality does not prove layout agreement, so backend capsules record layout requirements separately.

Proof Observation And Native Storage🔗

Proofs and CPU execution use the same tensor value. A proof observes the tensor through total coordinate lookup; generated code traverses its contiguous storage. There is no materialization step between a proof tensor and a host tensor.

For trusted memory, construction and reshape are separate:

[[1.000000, 2.000000, 3.000000], [4.000000, 5.000000, 6.000000]]

#[1.000000, 2.000000, 3.000000, 4.000000, 5.000000, 6.000000]

The round trip returns the original six values in the original order. For Float, Tensor.from raw packs the boxed array into a FloatArray, and reshape reuses that buffer without copying. Converting back with Tensor.to grid (Array Float) materializes a boxed array; requesting FloatArray instead exposes the packed buffer directly. CUDA remains a separate device representation connected by checked upload and download operations.

grid provides matrix coordinates; converting it to an array provides a flat sequence. An array consumer needs the dimensions separately if it is to reconstruct those coordinates.

Cost And Representation Notes🔗

The shape indices remove ambiguity, but they do not erase the cost of an operation. The useful cost model is:

Big-O notation alone cannot settle provider agreement. Two matrix multiplications may both take O(mnk) arithmetic operations while accumulating in different orders and returning different Float32 bits. The graph and backend chapters keep the operation, provider, and numerical contract separate for this reason.

Comparing Tensor Performance🔗

The checked representation does not make every scalar family equally fast. Compare the same operation, scalar type, input shape, and ownership conditions. Allocate inputs before timing, warm up each implementation, and check numerical results before comparing elapsed times. Record thread settings as well: a sequential baseline and a task-parallel contraction measure different execution policies.

Measure end-to-end training separately. Graph construction, parameter initialization, autograd, and optimizer state can dominate even when individual tensor kernels are fast.

Common Tensor Declarations🔗

The examples above use these declarations for construction, coordinate access, and arithmetic:

The generated API reference gives the complete signatures. This table is the smaller working set used by the examples in this guide.

Tensor Inspection In The Lean Infoview🔗

Open NN/Examples/DeepDives/TensorOperations.lean in VS Code with the Lean extension. Place the cursor on:

-- The value view shows coordinates; the statistics view
-- summarizes the same matrix.
#tensor_view matrix
#tensor_stats_view matrix

The first widget renders a tensor; the second summarizes its values. Move the cursor to #tensor_view firstRow to see the shape change after indexing.

Shape Guarantees🔗

If a model accepts Tensor α input, Lean checks that every statically represented layer composes and that the final result has the declared output shape. It can also check that a parsed runtime payload has the length promised by its dimensions. That is not a small property: automated testing of production tensor frameworks keeps finding shape and type inconsistencies that survive review (Liu et al., 2023).

Shape safety does not, by itself, prove:

• that external memory uses the expected row-major layout;

• that two axes have the intended domain meaning;

• that a CUDA kernel wrote within bounds;

• that an arithmetic operation is numerically correct;

• that training converges.

Model Construction🔗

The next chapter turns shape maps into layers and model architectures. The most useful sources to keep nearby are:

• NN/Tensor.lean for the public tensor surface and its focused conversion, construction, printing, and operation modules;

• NN/Tensor/Internal/Representation/Basic/Core.lean for the certified contiguous representation;

• NN/Proofs/Tensor/Basic.lean for flattening, unflattening, and algebraic laws;

• NN/Proofs/Tensor/Algebra.lean for the dot-product and matrix-product algebra used above.