October 2026

Lean 4.35 and Numerical Fixes

We updated Lean, mathlib and the documentation tools to 4.35, along with FloatLib. We also checked calculations near zero, at very large magnitudes and across the CPU/GPU boundary. Softplus now keeps small negative-tail values, log-cosh stays finite for large residuals, and the log and reciprocal gradients avoid unnecessary overflow in intermediate expressions.

For rounded CROWN, we now use directed bounds and start propagation from the requested input box. ODE corridor endpoints and time bounds round outward. Typed backward passes skip unreachable nodes, so an unused singular calculation cannot contaminate a gradient. Reached nodes still run their backward rules, even when their cotangent is zero.

The proof updates include binary32 reduction bounds over the tree’s own representable operands, an AdamW denominator margin that admits a zero-gradient first step, and replay-buffer theorems about stored contents and FIFO order. We removed ODE wrappers whose continuous binary32 assumption admitted only constant trajectories; real-valued interpolation needs its own stated enclosure and differential-equation assumptions.

October 2026

Running Our Own Tensor Calculations

We wanted to write our own tensor calculations in Lean without writing them again in CUDA. We can now give an ordinary Lean function a tensor and choose the device when we run it:

import NN.Kernel
open TorchLean

def square := fun (x : Float32) => x * x
def input : Tensor Float32 [3] := [1, 2, 3]

#eval square.run input
-- [1.000000, 4.000000, 9.000000]

def onGpu := square.run input (device := gpu)

CPU is the default and evaluates the original Lean function. GPU supports native FP32/FP64 and FloatLib’s configured binary formats, including binary128. Where hardware arithmetic matches the format, we use it. For wider or custom formats, we store each number in several integers and do the arithmetic on the GPU, keeping the extra precision.

We can pass parameters, branch on a value, or combine two tensors with f.zip. For calculations such as row sums and repeated updates, Program.of lets us read tensor entries and write ordered loops. It also recognizes recursive functions whose parameters stay fixed and whose step count decreases by one. CPU-only scalar types or formats keep their precision on CPU with a diagnostic. Unsupported code for a GPU-capable type and execution failures still return errors.

Lean checks that the expression we compile agrees with the function we wrote. For native FP32/FP64, we also prove that lowering and source generation preserve that expression, assuming the stated arithmetic and memory behavior. That proof doesn’t verify NVIDIA’s compiler or hardware. For configured formats, we compare GPU results against FloatLib; we haven’t proved the CUDA arithmetic implementation correct. Standard model operations continue to use LibTorch.

Ask for a gradient

We keep the function definition and turn on recording when we call it:

#eval do
  let result ← square.run input (grad := true)
  IO.println result.value
  IO.println (← result.backward)
-- [1.000000, 4.000000, 9.000000]
-- [2.000000, 4.000000, 6.000000]

This uses TorchLean’s existing tape. Whole-tensor functions such as sums and rank-two matrix products use the same call. Shapes and storage come from the input; tensors captured by the function stay constant. The frontend checks that the recorded expression matches the function.

Keep the chosen precision

We fixed precision loss in the GPU tape. It now keeps binary32 for Float32 and binary64 for Float, including saved values, gradients, optimizer state and checkpoints. Configured binary arithmetic now records on that same GPU tape, retaining complete words for both saved values and gradients. We can record addition, subtraction, multiplication, division, negation and scalar traversal, including binary128. Native model operators and optimizer checkpoints remain limited to their native dtypes.

Scalar conditionals record the chosen branch, and fixed-parameter recurrences record each step. GPU branch decisions synchronize to Lean; arithmetic and backward calculations stay on GPU. Recording keeps the intermediate values needed for backward and launches operations per step; forward-only execution can use one compiled loop instead. The count must be independent of the input we’re differentiating. At a branch boundary, the recorded gradient need not be a derivative. Arbitrary indexed programs still need their own backward calculation.

Other changes and migration notes

We also updated FloatLib. Its interval tactic now handles positive-base real powers, Real.logb and inverse hyperbolic functions, and lets us register a new function’s enclosure with its containment proof. The floating-point chapter shows a real-power bound checked by Lean. These are real-expression proofs, separate from the custom GPU execution path.

We shortened the settings users write: open TorchLean exposes cpu, gpu, native, ieee, eager and typedGraph. Input directions for higher derivatives now form one tensor, with a leading axis for the derivative order. The PINN example uses tensors for its collocation points and boundary data as well.

In the data and model APIs, collateSupervised is now collate, and firstFullBatch is firstBatch. For diffusion, diffusion.noisedSample is now diffusion.sample; its positional arguments take the step before the seed. Prefer seed := ... when migrating a call so the two numbers cannot be mixed up.

We fixed the RealWitness strict-growth assumption. It now applies to distinct inputs: requiring it at equal inputs would demand 0 > 0 and make the assumptions contradictory.

We corrected the backend reports to name the CUDA comparisons we keep in the test suite. For other GPU operations, we rely on LibTorch’s implementation. The default GPU profile allows that assumption; the strict checked profile rejects it.

Try the custom computations example for gradients, parameters, row sums, recursive updates and binary128 arithmetic. The guide chapter also explains the precision choices and proofs.

September 2026

Running CUDA Through LibTorch

We moved to LibTorch because maintaining CUDA kernels by hand was becoming cumbersome. Matrix products, convolutions, pooling, and reductions already have implementations in the PyTorch infrastructure. It makes more sense for us to reuse that work and spend our time on TorchLean’s models, differentiation, and proofs. LibTorch gives us access to those tensor operations from C++, while we keep the model definitions and autograd tape in Lean.

The CUDA backend now calls ATen through a LibTorch SDK instead of TorchLean’s own kernels. TorchLean retains its runtime tape and owns differentiation. Attention and spectral model composition live in Lean, using numerical primitives through the buffer API. About 7,000 lines of hand-written CUDA (elementwise, reduction, convolution, pooling, tensor, attention and DGEMM kernels) are gone, replaced by one shared C++ adapter, csrc/libtorch/torchlean.cpp, calling the corresponding ATen operations under a no-grad guard. The per-kernel CPU stub files went with them. A build without LibTorch now links one file, unavailable.c. Status and telemetry still work; numerical calls are rejected with a message that says how to rebuild.

Select the SDK with -Klibtorch_home=PATH or TORCHLEAN_LIBTORCH_HOME; a CUDA-enabled pip PyTorch installation works as the SDK root. The SDK notes record the tested versions and GPU checks; other SDK versions need their own CUDA suite results. Attention composes matrix products and softmax in Lean, including its local VJP, and the tape owns Q/K/V and saved probabilities. It uses full score matrices with quadratic sequence memory and no fused-attention selection. LibTorch is the standard backend for CUDA execution (-Kcuda=true, then --device cuda); the default CPU build needs no SDK or toolkit.

We renamed the Lean adapter to NN.Runtime.Autograd.Engine.LibTorch so the implementation isn’t confused with the device. .gpu and --device gpu select the supported GPU target (currently CUDA), without falling back to CPU. Explicit .cuda still works.

The Burgers example now uses the general FNO constructor and shared trainer on both devices. We removed its separate real-FFT training loop. New runs share one full-spectrum parameter layout; weights from the old GPU-only retained-bin model need a conversion before reuse.

Several native features were removed rather than ported:

Removed	Use instead
Buffer.setDeterministicReductions	Runtime.Autograd.LibTorch.setDeterministic
TORCHLEAN_CUDA_CACHE_CAP_BYTES, AllocatorStats.cacheBytes and cacheCapBytes	Buffer.memory reports allocatedBytes and reservedBytes, with Runtime.Autograd.LibTorch.setMemoryFraction and Runtime.Autograd.LibTorch.emptyCache. The limit is now a fraction of device memory, not a byte cap.
flashAttentionFwd/Bwd and native attention contexts	Buffer.attentionForward/attentionBackward, composed in Lean with tape-owned saved buffers
broadcastRowToRows, gatherVec, reduceSumByColumn	The corresponding ATen operations behind the existing buffer API
Fused FNO forward/backward externs	Lean composition of FFT, frequency mixing, and inverse FFT using numerical primitives
matmulCublas, matmulCublas32, matmulCublas64, CublasPrecision	Ordinary matmul; LibTorch chooses the BLAS call
nn.geluTanh	nn.gelu, which is the same tanh approximation

The fused LayerNorm and GELU kernels and the transpose-free matrix backward described in the August notes below are part of what was removed. ATen supplies its own implementations. We have not measured the end-to-end effect on training speed, so this entry makes no performance claim either way.

Convolution layers built through GraphSpec now start from different initial weights. They take their initialization seed from the layer’s position, the same way linear layers do, where they used to take twice that value. A model with a convolution therefore trains from a different starting point than before, even with the same seed. Linear layers and the zero or one initializations of biases and normalization parameters are unchanged.

September 2026

Choosing Scalar Precision with FloatLib

We wanted precision to be a choice users make in their tensors and models. FloatLib supplies the scalar arithmetic and rounding theory. ExecFloat.Binary 8 23 gives the familiar binary32 format; ExecFloat.Binary 15 112 gives binary128. Valid custom widths use the same API.

A wider type matters only if the extra digits reach the computation. For example, binary128 can retain $1+2^{-100}$, while binary64 rounds it to 1. The tensor chapter constructs that parameter directly from a rational, keeps it through a typed affine model, and compares its forward value, input derivatives and nn.sgdStep update with an elementary calculation. This uses software arithmetic on the typed CPU path. trainer.openTyped also retains the chosen scalar in supervised samples, predictions, loss, reports, and checkpoints. These typed sessions run on CPU, reject custom backend profiles, and do not expose Result.verify. Initialization and optimizer settings still enter through Float. The ordinary trainer’s .ieee option remains fixed to binary32. The numerical proofs distinguish rounded trees from exact accumulation followed by one final rounding. Their intermediate values can differ, so an error theorem for one does not justify the other. Native Float32 import/export and arithmetic proofs now come directly from FloatLib: addition and subtraction require finite operands, while square root covers every input through NaN-canonicalizing native export. The old local bridge files have been removed. These logical results remain separate from compiler and hardware conformance.

We also moved the shared interval, affine-quantization, and reduction-tree mathematics into FloatLib, then replaced TorchLean’s copies with imports and adapters. Users can choose the grouping and input order of a reduction tree, use a real quantization scale with their own rounding rule, or construct interval bounds with binary, decimal, or posit endpoints. TorchLean keeps the tensor lifts and backend contracts. Its numerical graph certificates still use binary32 endpoints; the broader scalar interval API does not change that certificate format.

The floating-point chapter explains the scalar API and numerical proofs.

September 2026

Derivative Theorems for the Executed Backward Sweep

This round of work was about closing gaps between what the runtime executes and what the theorems talk about, and about cutting code that no longer earned its place.

Proofs about the code that runs

The eager runtime’s dense backward sweep now has a Frechet-derivative theorem. Lowering a graph to a tape and running backwardDenseAll over it computes the adjoint of the derivative of the graph’s real semantics (backwardDenseAll_lowerGraphToTape_adjoint_fderiv), with supporting results that the sweep agrees with backpropAllCtx and that lowering preserves zero seeds. Before, the statements were about an abstract backpropagation function and the executed sweep had to be trusted to match it.

IR shape inference is proved sound against the semantics. checkShapes_sound and denoteAll_shape say that when the shape checker accepts a graph, every value produced by denotation has the inferred shape. The lowering theorem denoteAll_eq_of_lowerToForwardGraph now needs only a NoRawLog hypothesis; the NoMSELoss and NoConcat side conditions are gone because lowering covers concatenation, rank four and higher matrix multiplication, and batched linear layers. expectResultShape and every panic! were removed from the IR executor.

The real-valued CROWN transfer proofs now compose with IBP soundness. The transfer theorems used to assume IBPEnclosesVals, that the IBP boxes enclose the semantic values. EndToEnd.lean derives that premise from the IBP soundness theorem. alphaCrown_cert_encloses_semantics and the alpha-beta variant retain the graph support, topological ordering, input, local replay, and relaxation parameter hypotheses. Their conclusions concern nodes with both a certificate entry and a semantic value; the all-node variants require coverage. runIBP_encloses_evalGraphRec gives the corresponding result for the runtime IBP algorithm over real scalars, under its engine-core and coverage hypotheses. These results do not establish soundness of the rounded CLI passes.

Softmax, attention, LayerNorm, and BatchNorm derivative proofs are now stated about the Spec definitions rather than about auxiliary functions that happened to agree with them. hasFDerivAt_softmaxSpec_vec and softmaxBackwardSpec_eq_vjp cover softmax; log-softmax uses hasFDerivAt_logSoftmaxSpec_vec and logSoftmaxBackwardSpec_eq_vjp. backpropVec_eq_adjoint_fderiv_scaledDotProductAttention connects the attention tape rule to the derivative of the spec; hasFDerivAt_batchNorm, fderiv_batchNorm_eq_batchNormJvp, and layerNormJvp_layerNormBackward_adjoint do the same for normalization. The LayerNorm theorems take 0 < ε explicitly.

Two division bounds in the rounded-real approximation library were vacuous: their hypotheses could not be met at the same time, so the theorems proved nothing about any real run. They were deleted, and the sigmoid, logistic, and mean bounds were rebuilt on divPosErrorBound, with small regression theorems (reciprocal_sigmoid_bound_scalar_le_one, mean_row_bound_of_exact) so the same mistake would be caught again. The strongly convex gradient descent bound now keeps its q^k factor.

The native LayerNorm kernel now keeps its mean and centered variance in binary64 before storing binary32 normalized values. This fixes large-offset rows whose small differences were lost by rounding the mean too early. Its input, scale, and bias gradients were checked against the Float specification using the saved forward values.

LayerNorm derivative certification now returns an unsupported result. The old flattened interval rule could understate a derivative bound; the real-valued row theorems do not justify that rule. The complete transfer proof for the directed row payload is still needed before this certificate path can be enabled.

Smaller pieces

Several monolithic proofs were split into files that can be read one case at a time. alphaCrown_transfer_sound went from 1,857 lines to a 44-line dispatch over per-operation files, cert_encloses_semantics from 1,283 lines to 10, and the two dense backward lowering proofs from about 800 lines each to 64 over shared leaf and snoc lemmas.

The backend capsule layer was cut to what the runtime uses. ProofCarryingKernel, VerifiedPlannedKernel, Target, Gate, Recheck, and the TrustLevel.verified and fuzzed labels are gone; none of the maintained capsules carried a refinement theorem, so the vocabulary promised more than the code delivered. What remains is KernelCapsule with bind, checkContracts producing a ContractCheck, and a numerical policy with one field, reduction, which the numerical certificate registry reads. The installation page describes the current selection path.

The generated UnicodeData.lean table went from 5,767 lines of per-character entries to a 376-line interval table with the same lookups.

API names

TrainOptions.batchSize is now samplesPerStep, and steps is required rather than defaulted. The seq! macro is gone: nn.compose![...] composes built layers and nn.Sequential![...] is the monadic builder, both scoped so files need open TorchLean. The einops term syntax is scoped under TorchLean.Tensor, and repeat is renamed expand. Runtime.Autograd.TorchLean is Runtime.Autograd.Model, and NN.Verification.TorchLean is NN.Verification.Builtin. Trainer.Result exposes state, save, and stateShapes, Trainer.load restores a saved result, and nn.buildIO instantiates a builder outside a trainer.

Then we went looking for names that existed only so that older call sites would keep working, and deleted them. Spec.fill, Spec.zeros, and Spec.ones were thin wrappers whose own docstrings described them as older spellings of Tensor.full, Tensor.zeros, and Tensor.ones, so the canonical names are now the only ones, and the value argument follows the shape the way torch.full(shape, value) reads. The Runtime.Autograd.Model.Random module was the same idea at module scale, fourteen wrappers around Spec.Random; it is gone, and the RNG helpers now come from NN/Spec/Core/Random.lean as Spec.Random.splitmix64 and friends. Trainer runtime flag parsing now lives in NN.API.CLI.Trainer: use TorchLean.CLI.Trainer.parse, parseCommandLine, and cliArguments. The older trainer helpers and NN.Examples.Support.TrainerFlags are gone.

Smaller renames from the same pass: Tensor.tensorFoldlSpec lost its stuttering prefix and is Tensor.foldlSpec, the ONNX helpers dropped their onnx prefix now that they live in namespace ONNX, Opts is spelled Options in the verification command lines, inferNodeOutShape is nodeOutShape, and TextCorpusOptions is CorpusFileOptions. Two naming rules came out of this and are written down in docs/CONTRIBUTING.md so the next reader does not have to guess: the smart constructor of a sealed structure is create inside that structure’s own Internal namespace. Batch choices belong in named options when the shapes and semantics agree. Logit row selection now uses Tensor.get directly, without separate text-specific indexing helpers.

August 2026

Cleaning Up the Tensor API

We wanted to improve the naming and cut out repeated code. Too many public names said 2d, 3d, NCHW, or batch even when the operation itself did not depend on those choices. That made the API harder to guess and left us maintaining several routes to the same tensor operation.

Convolution was the biggest example. nn.conv, nn.convTranspose, nn.maxPool, and nn.avgPool now take a spatial rank d together with Tensor Nat [d] values for their geometry. One definition covers lines, images, volumes, and higher-dimensional mathematical specifications. Batch, sequence, and other outer axes are passed in leading : List Nat and preserved by the operation. nn.ConvGeometry.samePadding works at any spatial rank and comes with a proof that it preserves positive spatial extents. The LibTorch execution path follows PyTorch’s one-, two-, and three-dimensional convolution and pooling families.

We made the same change to normalization and shape operations. nn.batchNorm and nn.instanceNorm preserve any leading and spatial axes. permute and transpose take explicit axes instead of putting a layout in the function name. matmul handles compatible leading dimensions, and flattenAfter says exactly which prefix of the shape should be kept.

The main name changes are:

Old name	Use now
conv2d, Conv2dSpec	nn.conv, Spec.convSpec
convTranspose2d, ConvTranspose2dSpec	nn.convTranspose, Spec.convTransposeSpec
maxPool2d, avgPool2d, adaptive *2d specs	rank-polymorphic pooling operations and specs
batchNorm2d, batchNormChannelFirst, instanceNorm2dNchw	axis-general normalization
transpose2d, transpose3d*, nchwToNhwc, nhwcToNchw	permute or transpose with explicit axes
mm, bmm	matmul
flattenBatch, flattenLeading	flattenAfter

We removed the old names and migrated their callers instead of keeping aliases around. PyTorch’s rank-specific names still appear inside import and export code because that is how PyTorch spells those operations, but they are no longer TorchLean APIs.

While doing that, we got rid of vague names like General and ND too. The ordinary MLP evaluator is now just mlpEval; its scalar-input version is mlpEvalScalar. Grouped convolution and dilated geometry say so in their names, the pooling implementation lives under Pooling.Spatial, and the tensor-input Stone–Weierstrass result lives in Universal.StoneWeierstrass.

We followed the change through the specification, typed graph, IR evaluator, shape inference, eager runtime, CUDA dispatch, and reverse-mode rules. The CUDA adapter accepts the spatial ranks LibTorch implements instead of maintaining a separate higher-rank numerical kernel. Convolution has general input, kernel, bias, and transpose-convolution derivatives. BatchNorm has the matching adjointness theorem for its input, scale, and bias gradients at any spatial rank. The rounded-real proofs follow the implementation’s actual accumulation order.

The smaller tensor details got cleaned up too. Proofs can use Tensor.map_scalar, Tensor.map_dim, and Tensor.getScalar_map instead of reopening the shape recursion themselves. Classifier and regressor heads keep their leading axes. Indexed embeddings append their width to the token shape and scatter-add repeated token IDs during backward execution.

This let us delete the old tensor forwarding modules, packed/vector wrappers, fixed-rank pooling files, 2D padding helpers, and the channel-first BatchNorm proof wrapper along with their callers.

August 2026

Lean 4.33

TorchLean now builds on Lean and mathlib 4.33. The migration touched dependent tensor casts, autograd derivative proofs, graph evaluation, CROWN certificates, and the documentation toolchain.

The execution API now separates execution mode from device selection:

{ execution := typedGraph
  device := cpu }

Eager execution runs each operation immediately and builds a dynamic tape. Typed graph execution records a shape-indexed executable graph once and reuses its forward, JVP, and VJP programs. The graph stores an exact typed output reference, so a model may return an input or intermediate rather than only its final recorded node. Call nn.lowerToTypedGraph model when the graph itself is needed. The executable graph stores derivative rules; the separate proof-carrying graph establishes when those rules are mathematically correct. TorchLean now uses lowering for this conversion and reserves compilation for future optimization, fusion, scheduling, and native code generation. The previous misleading execution terminology was removed rather than retained as aliases.

The model API also distinguishes definitions from live state. nn.Sequential and nn.Layer are immutable values used by lowering and proofs. Instantiating a checked model produces an nn.Module with mutable parameters, persistent buffers, and train/eval mode. A lower-level Module.Objective pairs that state with a scalar training objective. Its name makes clear that the object owns model state as well as the loss calculation.

Training now has one public lifecycle for regression, classification, and custom losses. A trainer selects the loss once, then predict, train, checkpointing, streams, and verification reuse the same model state and runtime dispatch. The duplicate task-specific runners and definitional state layout lemmas are gone.

Lean’s Float32.Model exposes the logical definitions of core binary32 operations. TorchLean now proves agreement between that model and its independent raw-bit binary32 implementation for classification, comparison, addition, subtraction, multiplication, division, square root, negation, and absolute value. The arithmetic proofs cover normal and subnormal inputs, signed zeros, infinities, NaNs, underflow, overflow, and nearest-even rounding. NaN results are canonicalized before their bits are compared because the models retain different payload information.

Native compiler output, processors, CUDA, cuBLAS, and LibTorch retain their own backend contracts. Transcendental Float32 functions also remain outside the core logical model.

The logical model is part of Lean 4.33, and its binary32 implementation is available in Init.Data.Float.Model.Float32.

August 2026

Exact Tape Derivatives and CUDA Cache Limits

The exact autograd proof reaches the lowered tape. For a real algebraic graph, dense reverse accumulation returns the graph’s full cotangent context, and its input block is the adjoint Fréchet derivative of forward evaluation applied to the output seed. The pointwise theorem permits piecewise-smooth operators when the chosen execution point satisfies their differentiability and domain hypotheses.

The connection uses an exact correspondence between the analytic graph and the real algebraic graph with a trivial environment. Conversion preserves forward evaluation, JVPs, and reverse accumulation, and both graph conversions round-trip. The theorem can be inspected without importing an executable backend:

import NN.Proofs.Autograd.Runtime.Link.FDeriv

#check Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphToTape_adjoint_fderiv
#check Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphToTape_adjoint_fderiv_at

This result concerns the exact tape over Real. Native Float32 and CUDA executions still require the numerical-refinement assumptions described in the runtime-approximation chapter.

At the time of this update, TorchLean’s own CUDA allocator had an optional byte limit for released buffers retained for reuse. The September LibTorch migration replaced this allocator and removed the setting shown below:

TORCHLEAN_CUDA_CACHE_CAP_BYTES=$((512 * 1024 * 1024)) \
  lake -K cuda=true exe torchlean gpt2 --device cuda --steps 100

AllocatorStats.cacheBytes reported reusable device memory separately from live tensors, while cacheCapBytes reported the parsed limit. A block that would exceed the limit was synchronized and freed. The cap was fixed when the allocator first read it; 0 or an unset variable meant unbounded.

The CUDA stress suite ran the allocator in fresh subprocesses and checked a finite limit, an explicit unbounded control, malformed input, and integer overflow. Its assertion used the limit reported by the native allocator rather than reproducing the native parser in Lean.

July 2026

Lean 4.32, Numerical Proofs, and Runtime Tests

Imports, floating point, training, CUDA, and documentation

The July work touched most of TorchLean. We removed duplicate entry points, generalized tensor operations, reorganized the floating-point files, and tested the training runtime on models large enough to expose bugs that the small examples never reached.

Imports and File Layout

Most model code starts with import NN.API. The old NN.Library and NN.Entrypoint.* forwarding modules are gone. Focused imports such as NN.Spec, NN.Runtime, NN.Floats, and NN.Verification still lead directly to their declarations. The model examples remain part of TorchLean.

We also broke up several files that had become difficult to navigate. Training, data handling, schedulers, CROWN propagation, graph lowering, runtime operations, normalization, Muon, and floating-point semantics moved into smaller modules with narrower imports. The API tree is about 300 lines smaller and the guide is more than 5,000 lines shorter. The proof tree grew to include numerical certificates, rounded backpropagation, optimizer contracts, and new floating-point results.

The public neural-network API has one owner. Seeded layer builders and model-zoo constructors are declared under TorchLean.nn; NN.API gathers them without redeclaring their names. Fixed-sample training lives under TorchLean.Trainer.FixedSample. Inside the runtime, mutable parameter storage and optimizer checkpoint schemas have their own modules, separate from trainer execution and CUDA Adam serialization.

General tensors

A batch is an axis of a tensor. Permutation, reduction, reshape, and global average pooling work over declared axes. Channel normalization takes an explicit channel axis and preserves every other axis.

Models

CNNs, ResNets, ViTs, FNOs, transformers, GPT, Mamba, recurrent models, generative models, reinforcement learning, and self-supervised examples all remain available. They use the same tensor and layer API instead of carrying model-specific forwarding stacks.

Training

Optimizers share one stateful tensor interface. We kept laws that say something useful about update rules and stream composition, and removed generated tables and `rfl` theorems that only repeated a definition.

The trainer treats samplesPerStep (called batchSize at the time of this note) as the number of dataset items per optimizer update. For an ordinary dataset those items are samples. For Data.batch, each item is already a typed tensor minibatch, so samplesPerStep := 1 keeps one vectorized pass per update. Larger values accumulate gradients across several items. Logged pre-update loss comes from the same forward tapes as the gradients; training no longer runs a second forward pass just for logging.

Transformer batches use one attention tape node instead of asking the host to run the layer once per sample. The public model and typed graph preserve the declared leading shape. The eager CUDA path may fold those axes together with the attention heads for batched matrix multiplication, while TorchLean still applies the hard mask and computes the local VJP. A regression compares the vectorized forward value, input gradient, and shared weight gradients with repeated single-sample execution.

Layer normalization and tanh-approximate GELU follow the same rule: one TorchLean operation, one local VJP, and fused CUDA kernels for the numerical work. In a two-step GPT-2-small trace with batch 6 and context 1024, local profiling showed fewer kernel launches while leaving the matrix-multiplication schedule unchanged. The CUDA parity suite checks forward values and gradients against the CPU path; the native kernels remain inside the documented runtime boundary. Timing claims belong with a retained benchmark configuration and trace, so this update records the implementation and regression coverage rather than presenting one workstation run as a general speedup.

Matrix backward no longer materializes transposed copies before calling cuBLAS. The runtime passes logical transpose flags to the same batched-matrix primitive used by linear layers, projection weights, and ordinary matmul. Focused traces confirm that these temporary transpose kernels disappear, and parity tests compare the resulting forward values and gradients with the existing path.

CUDA Adam and AdamW state can be saved independently of model checkpoints. The binary format records optimizer hyperparameters, parameter shapes, mutability flags, moment tensors, and step counters using explicit little-endian fields. Loading rejects mismatched models, changed moment parameters, duplicate state entries, truncation, and trailing data. Writes close and flush a fresh sibling file before renaming it over the destination. The parameter-schema codec is shared by backend-owned optimizer checkpoints; the CUDA Adam-family codec supplies the format-specific configuration and moment payload.

Discrete model inputs have their own typed path through programs, modules, evaluators, trainers, and checkpoints. CharGPT passes token ids and targets as bounded Tensor (Fin vocab) [batch, seqLen] values; raw Tensor Nat [batch, seqLen] values are admitted only after Tensor.checkIndices validates the tokenizer boundary. The old floating-point transport and conversion step are gone. The causal Transformer API supports either an independent vocabulary head or an output projection tied to the embedding table. In the tied form, lookup and output gradients accumulate into the same parameter.

Floating-Point Semantics

import NN.Floats provides formats, rounding, finite binary32 semantics, executable IEEE binary32 operations, interval rounders, and scalar quantization. It does not pull in tensors, models, autograd, CUDA, certificate checkers, or external tools. Tensor and proof integrations sit above that import, while optional Arb checks require an explicit import.

The generic development under NN.Floats.NeuralFloat is organized by format, rounding, scalar operations, analysis, error bounds, and execution policy. It covers radix and exponent formats, directed and nearest rounding, round-to-odd, ULPs and neighboring values, double rounding, Sterbenz subtraction, and absolute and relative error bounds. Flocq influenced the layout. TorchLean’s definitions and proofs are written in Lean.

Sterbenz subtraction covers gradual underflow and has a binary32 specialization. Every finite executable binary32 bit pattern is proved representable in that specification, so the executable Sterbenz theorem can identify nearby subtraction with the exact real difference. Finite executable values also expose a checked ULP exponent, and an absorption theorem connects an unchanged binary32 accumulator to the rounded-real specification.

We use the following distinction throughout TorchLean:

• NeuralFloat and NF describe configurable rounded-real arithmetic used in proofs;
• FP32 specializes the rounded-real model to binary32-sized parameters;
• The executable binary32 model includes IEEE-754-style behavior, including special values;
• runtime bridges state how native values are interpreted by those models.

The effective-rounding example shows the whole argument on one value: choose a format and rounding mode, perform the rounding, and derive the resulting error bound. The runtime-approximation proofs then start from the ideal autograd theorems and make every extra hypothesis about rounded execution explicit.

Whole-Graph Numerical Certificates

TorchLean can build a numerical trace over the canonical NN.IR.Graph. Source intervals use exact binary32 endpoints. The checker reconstructs outward-rounded ranges for supported arithmetic, activations, directed square root, reductions, matrix multiplication, pooling, MSE, and stable softmax; malformed domains and non-finite ranges fail at the node that produced them.

Range rules live in an operation registry. The same traversal handles any architecture after lowering. Before propagation, a coverage pass lists the exact nodes whose primitives lack a range contract. The checker compares the certificate’s registry name, recomputes the ranges using the selected rules, and compares the trace and kernel audit. The name does not uniquely identify a rule implementation; changing a rule without changing those results need not cause rejection.

The same certificate contains the kernel-selection audit. Each kernel capsule records its reduction order in its numerical policy. Portable accumulations use the fixed left fold from the tensor semantics. CUDA and LibTorch accumulations are marked implementation-dependent, so their matrix products, convolutions, normalizations, FFT/FNO paths, scans, and attention kernels cannot accidentally inherit a proof for a different reduction order.

The bit-level replay evaluates every graph intermediate with executable binary32 arithmetic, checks its shape and range, and rejects NaN or infinity. A checked certificate stores the exact graph it was checked against, so replay cannot substitute a different graph. A separate proved real execution supplies the semantic enclosure; combining it with the bit-level replay yields an entrywise error trace for every node. The deep-dive example includes successful arithmetic, reduction, matmul, LayerNorm, abs -> sqrt, and softmax traces, together with deliberately tampered, invalid-domain, and wrong-reduction-policy cases. It ends with a complete two-layer MLP: ten graph nodes pass coverage, range generation, backend-capsule audit, and bit-level replay. The numerical-runtime walkthrough follows that run from source enclosures to its checked output.

Rounded Backpropagation and Optimizers

The numerical proof continues past the forward graph. Proof-bearing reverse nodes carry both their ideal VJP and their rounded VJP error transformer. The global reverse theorem composes those local bounds through gradient accumulation and connects the result to executable autograd GraphData.

One optimizer contract carries the gradient error through parameter updates. SGD and momentum SGD have no extra domain condition. AdamW uses the same interface, with step data recording errors from both moments, bias correction, square root, adaptive division, decoupled weight decay, and the final subtraction; explicit margins keep the rounded denominator away from zero. The end-to-end theorem therefore works unchanged for all three optimizers and for every model represented by a RevGraph. A model-wide update applies it at each typed parameter index.

The canonical NN.IR.Graph certificate remains a forward certificate. Its current lowering does not attach proved VJPs, so backward claims use the proof-bearing reverse graph path instead of silently attributing autograd semantics to a forward-only lowering.

Tensor Quantization

Uniform affine quantization uses FloatLib’s scalar definitions, re-exported by NN.Floats.Quantization, with a rank-polymorphic tensor adapter under NN.Spec.Quantization. The proofs cover code-range preservation, monotonicity, exact dequantize/quantize round trips for in-range integer tensors, and the half-step reconstruction bound when saturation is inactive. Layout and storage width are not part of the arithmetic: int8, uint8, int4, and custom code sets differ through their integer bounds rather than separate image-specific APIs.

Backend Contracts

Backend planning now records device, provider, operation, contracts, and evidence separately, then binds each accepted capsule to a matching runtime handler. Unavailable providers fail explicitly, and the contract check accepts a capsule’s evidence only when the profile’s assurance policy admits it, rather than relying on a trust label. The backend chapter contains the maintained profiles and full contract model; the GPU chapter covers native execution and platform boundaries.

Mathematical and Verification Corrections

Losses and masks

Huber loss and Smooth L1 have their intended, distinct scaling. Hard attention masks use exact exclusion in the softmax semantics: a blocked entry contributes zero numerator. The old finite -1000 masking convention was removed from attention paths and examples.

Bounds

Leaky-ReLU interval propagation handles a negative slope across the kink at zero. Logarithm interval checks reject nonpositive domains. Unsound or undocumented GELU and ELU candidate bounds were removed instead of being exposed under names that suggested certified enclosure.

Certificates

JSON certificate readers reject non-finite claims before array comparisons. IBP certificates are checked by recomputing the complete binary32 trace from the trusted graph, parameters, and input box; an artifact may widen that trace but may not shrink it. CROWN and $\alpha,\beta$-CROWN affine entries are compared exactly with a sequential replay instead of being propagated from certificate-supplied parents. A theorem turns successful exact replay into the local-consistency proposition used by the generic CROWN soundness development. Relating that binary32 replay to real-valued enclosure still requires the stated finite-precision refinement assumptions.

Classical models

HMM normalization records zero probability for an impossible observation, and log-likelihood is partial at that boundary. GMM covariance matrices must be symmetric positive definite, mixture weights must be positive and normalized, and singular inversion fails rather than returning the identity. The covariance gradients use the transpose-correct formulas.

Attention and diffusion

Multi-head attention reshapes sequence data to (sequence, heads, head-dimension) before exchanging the sequence and head axes. The probability-flow ODE uses the required one-half score coefficient, and its Euler sampler visits time points in descending order from the noisy endpoint.

Layer and model edges

Dropout is the identity in evaluation mode. Max pooling rejects padding configurations that would create windows containing no input values. PCA requires at least two samples for its unbiased covariance and exports the centering term as a linear bias. Linear SVM fitting calls its regularization coefficient lambda, leaving C for the standard inverse-strength convention.

Formats and smooth pooling

A radix carries a proof that its base is at least two, and a format precision carries a proof that it is positive. Checked constructors reject bad integers at configuration boundaries. Smooth max pooling uses a sign-aware pivot for both positive and negative inverse temperatures on CPU and CUDA. Zero, non-finite, or unrepresentable inverse temperatures are rejected before a native kernel runs.

Rounded CROWN no longer discards every backward objective to a constant interval. For algebraic nodes it carries lower and upper coefficient vectors with directed arithmetic, including the sign of each input interval when the final affine form is evaluated. Nonlinear or unsupported nodes still fall back to their checked IBP boxes. This improves the executable bound without pretending that an unproved floating-point transfer is exact.

The arithmetic interface separates implementation from proof. BoundOps provides executable lower and upper operations; LawfulBoundOps proves that those operations enclose exact real addition, subtraction, and multiplication. Real and FP32 endpoints have lawful instances. Host Float remains an explicitly trusted execution boundary, while IEEE special values are handled by finite-path theorems instead of a blanket ordered instance.

The Lyapunov workflow no longer contains a repository-wide oracle axiom. Python output records a region and numerical margins, and generated Lean files may prove arithmetic facts about those numbers. LyapunovCert.ValidFor proves that the reported intervals enclose the named value and orbital-derivative functions throughout that region. With strict margins, this gives positivity and decay there. A stability theorem also needs the connection to the dynamics and the appropriate region and equilibrium conditions.

The graph evaluator and verifier lowering are split by operation. Their coverage theorems still range over the full operation vocabulary, so adding a new file does not weaken the statement being proved. We removed theorems tied to incidental list lengths and retained small definitional lemmas only when later correctness proofs actually use them.

Convolution, transposed convolution, fixed-window pooling, and adaptive pooling now share channel-first contracts parameterized by spatial rank. Their public APIs take vectors of kernel, stride, padding, and output dimensions; the same definitions therefore cover lines, images, volumes, and higher-dimensional specifications. The IR, eager runtime, and shape inference use these contracts without separate rank-named wrappers; the LibTorch adapter uses PyTorch’s spatial ranks one through three. A semantic-preservation theorem connects typed convolution lowering to forward IR evaluation. The exact derivative theorem covers the same rank-polymorphic operation and proves the input, kernel, and bias reverse rules. Rounded-real theorems bound every forward and backward coordinate using the implementation’s actual accumulation order. BatchNorm now has the corresponding arbitrary-spatial-rank adjointness theorem for its input, scale, and bias gradients.

PyTorch graph import now preserves every leading dimension of a linear layer. In particular, a batched input of shape [3, 4] passed through Linear(4, 1) is imported with output shape [3, 1] rather than [3]. The runtime check includes this case alongside arbitrary-axis reductions, permutations, normalization, convolution, pooling, and attention, while continuing to reject unsupported operator semantics explicitly.

Verification artifact readers share one finite box-region parser. It rejects non-finite coordinates, negative radii, mismatched dimensions, reversed intervals, incomplete field pairs, and mixed endpoint/center schemas. Format-specific checkers can require the exact endpoint schema; the alpha-beta-CROWN leaf checker does so before checking nesting and threshold witnesses.

Lean 4.32

TorchLean builds with Lean, mathlib, DocGen, and Verso 4.32. During the upgrade we replaced the deprecated Lean.RBMap with Std.TreeMap, used mathlib’s stronger sine remainder estimate, and made several dependent casts explicit. Proof-valued runtime helpers are theorems when they serve as opaque evidence; constructors that must compute remain reducible abbrevs. We fixed the new linters rather than suppressing them.

Runtime Scaling and CUDA Ownership

The small examples had hidden an expensive habit: large parameters were first expanded into nested Lean values and only then copied into the execution engine. Parameters and gradients are materialized directly where they will run. We also stopped generic convolution backward from rebuilding the same derivative structure, and taught CUDA attention and fused FNO paths to release temporary buffers as soon as their contribution is consumed.

The most useful failure came from sparse reverse mode. A pure expression allocating a one-element CUDA seed could be shared by Lean, even though backward consumed and released the native buffer. The next use then referred to storage that was no longer alive. Seeds that cross an ownership boundary come from an effectful constructor, and transfers between gradient maps use explicit copy-and-release operations. A stress test repeats this path and fails if live CUDA allocation grows or a supposedly fresh seed is reused.

A second lifetime problem was in the FFI signatures themselves. Buffer and array inputs were being passed as owned Lean objects to native functions that treated them as borrowed, so neither side released the wrapper reference. The declarations mark those inputs as borrowed. Separate payload and wrapper counters make the distinction visible, and the stress suite checks thousands of allocations for matching finalization counts.

Shape-erased CUDA values compare the native buffer length with the recorded tensor shape before an operation runs. Dense and sparse backward also reject output seeds or initial gradients with the wrong length. The stress suite covers each rejected case.

We exercised 21 CPU workflows and 24 CUDA workflows, including dense, convolutional, attention, recurrent, operator-learning, generative, and reinforcement-learning models. On the machine used for this release, a roughly 100-million-parameter MLP completed ten CUDA optimizer steps in about 15.2 seconds. The fused Burgers FNO ran for 100 steps with no growth in live buffers; training MSE fell from 0.3260 to 0.0172 and test MSE ended at 0.0220. These numbers record what we tested on one machine. They are not a general performance promise.

Documentation and Validation

The Guide and API reference follow the new module layout. Installation has separate notes for Linux, macOS, WSL2, native Windows, CUDA, and optional LibTorch support, and the floating-point and backend chapters explain where a theorem ends and a runtime assumption begins. Repository checks build NN directly; NN.Library no longer exists.

Lyapunov results consume an explicit LyapunovCert.ValidFor proof, so a producer’s JSON flags cannot become a stability theorem by themselves.

The Graphs page contains the module-import explorer and build-performance link. The Tools page links LeanProfiler and TorchLean Verified Examples. LeanProfiler includes a TorchLean model run, Perfetto trace output, and JSON comparisons. The verified examples cover batch-invariant inference and a verifiable transformer checkpoint.

The import explorer ignores fenced guide examples, so an import shown in a tutorial is not mistaken for a source-module dependency.

Wide tables are wrapped during the documentation build, and the Guide’s equations render with KaTeX.

June 2026

CUDA, CROWN, and PINN Reliability

Native runtime, certificates, scientific ML

The June reliability pass tightened CUDA allocation checks, made CROWN certificate statements more direct, and moved duplicated PINN training code into shared helpers.

Runtime checks

CUDA and CPU stubs use shared checked size arithmetic for products, byte counts, and additions at the Lean FFI boundary. Broadcast, reduction, swap, gather/scatter, attention, convolution/pooling, tensor-copy, and spectral-convolution paths reject impossible sizes before allocation or kernel launch.

Proof API

The graph CROWN certificate theorem returns the enclosure for the node being checked. The IEEE32 version records the no-self-dependency condition on the evaluator trace, and the two-layer MLP CROWN code exposes the affine forms used by boundAffineCrown.

PINNs

The Python PINN command shares dataset loading, MLP construction, expression evaluation, gradients, constant parsing, and weight export between its evolution and stationary problems in scripts/verification/pinn/train_pinn.py.

The focused API import exposes the short TorchLean.* namespaces directly. With import NN.API, users get TorchLean.nn, TorchLean.optim, TorchLean.Trainer, TorchLean.Data, TorchLean.Loss, and TorchLean.Metrics without importing the broader NN umbrella.

June 2026

Lean 4.31 Migration

Toolchain alignment

TorchLean builds with leanprover/lean4:v4.31.0. The root Lake manifest, Mathlib pin, documentation generator pin, Verso blueprint toolchain, website metadata, README, and formalization metadata were moved together.

The migration fixed proof-term breakages in differentiability and autograd composition files where Lean 4.31 became stricter about composed functions and eventual equality.

May 2026

Repository Modularization and Comment Cleanup

Source organization

The public source tree is easier to read, easier to review, and easier to extend without changing TorchLean's intended behavior.

Structure

• Large proof and runtime files were split along conceptual boundaries.
• Umbrella modules were kept only where they make imports clearer.
• Obsolete import shells and example names were removed.

Documentation

Comments were rewritten in a more mathlib-style voice: definitions state mathematical intent, runtime boundaries name assumptions, and examples avoid stale narration.

Scope

Model semantics, verification claims, CUDA behavior, and trusted boundaries are unchanged.

The examples and website pages were rebuilt against the new module layout.

May 2026

Runtime API Update

Training loops, streams, initialization

Longer examples use the same public runtime API for initialization, minibatches, optimizer steps, logging, and checkpoint-style parameter files.

Initialization

Runtime-side Float initializers and shape-indexed initializer plans make parameter construction explicit: the model declares the parameter shape, the initializer plan selects the distribution or constant, and the runtime builds each tensor once.

Streams

Step-indexed training streams make minibatches explicit. A batch may come from a rule, a simulator, a replay buffer, or a file-backed window source, but the training loop sees a typed stream of inputs, targets, and metadata.

Language models

Integer-token embedding and row-wise cross-entropy helpers let GPT-style examples train on token ids directly, instead of expanding every target into a one-hot vector.

The runtime documentation follows the same path as the examples: initialize parameters, produce batches, run forward/autograd, update parameters, save reports, and state the native or external boundary when a backend is selected.

May 2026

CUDA Training Stability

Memory lifetime, allocator diagnostics

Longer CUDA training runs exposed allocator pressure from intermediate values that could stay attached to a run longer than needed.

The issue was not model size. Some intermediate values created during training – tape entries, gradient buffers, and kernel workspace buffers – could remain alive across many optimizer steps. The fix made the training loop and CUDA eager backend explicit about which values are returned to the caller and which buffers can be released after the step finishes.

Step counts

Loader-based model commands treat --steps as optimizer updates.

Buffer lifetime

CUDA eager/autograd releases ephemeral tape, gradient, and workspace buffers after each step.

Diagnostics

Longer CUDA examples report allocator telemetry by default, with --cuda-mem-watch N for exact sampling.

May 2026

Introductory Data Note

Reproducible builds

Some examples use public datasets and do not download them during lake build. Keeping data downloads explicit makes ordinary builds deterministic and avoids silently committing large external data.

For the model-zoo MLP example:

python3 scripts/datasets/download_example_data.py --auto-mpg

For the text and vision examples:

python3 scripts/datasets/download_example_data.py --tiny-shakespeare --cifar10

May 2026

TorchLean Released

Initial public release

TorchLean became public as a Lean 4 framework for writing, running, inspecting, and verifying neural-network programs.

Core system

Typed tensors, layers, model APIs, loaders, training loops, examples, and a shared graph IR for execution, inspection, verification, and import/export.

Semantics

Finite-precision semantics, executable IEEE-style Float32 models, autograd, optimizer support, and explicit runtime agreement boundaries.

Verification

IBP/CROWN-style bounds, certificate checkers, VNN-COMP-style bundles, Bug Zoo contracts, 3D geometry certificates, and optional CUDA/native runtime paths with documented trust boundaries.

The README example is the shortest entry point; the Guide and Examples pages carry the longer walkthroughs.