Repository navigation
We’ve changed quite a lot since v1.3. We wanted clearer names, fewer repeated implementations, and a closer connection between the computations we run and the mathematics we prove.
Tensor operations and model APIs
We replaced many rank- and layout-specific APIs with general operations whose arguments describe the shape, axes, and geometry. Matrix multiplication, convolution, pooling, normalization, and model composition now share more of their implementation. We removed obsolete wrappers and migrated the examples instead of keeping multiple names for the same operation.
LibTorch execution
Maintaining our own CUDA kernels was becoming cumbersome, especially when PyTorch already provides the numerical infrastructure. We moved standard GPU operations to LibTorch through one shared C++ adapter. Model definitions, the differentiation tape, attention composition, and spectral-layer composition remain in Lean. LibTorch computes the numerical primitives.
Differentiation and proofs
We expanded the connections between executed backward sweeps and mathlib derivatives, improved higher-order differentiation APIs, and simplified the TapeM proof interface. Derivative directions and PINN sample points now use tensors directly. Complex-valued training examples are supported, with a directional-gradient implementation intended for smaller workloads.
FloatLib and numerical verification
We now reuse more of FloatLib’s scalar arithmetic, rounding proofs, intervals, quantization, and reduction-tree mathematics. Typed CPU computations can retain configurable binary precision. We also expanded rounded IBP and CROWN soundness proofs, strengthened real graph semantics, and corrected several interval and normalization bounds.
Custom tensor computations
We can now apply ordinary Lean scalar functions to tensors and choose cpu or gpu at the call site. Supported GPU computations include FP32/FP64 arithmetic, conditionals, indexed reads, and bounded folds. These can run alongside standard LibTorch operations. The implementation includes lowering and emitted-source correctness proofs under explicit contracts. NVIDIA compilation and hardware execution remain external trust boundaries.
Documentation and validation
We updated the README, examples, API documentation, and blueprint, including a new custom-computations chapter! Excited for this big release:)!