A Lean 4 library for neural network modeling, training, and formal verification.

⚠️ Warning: This module is a work in progress and may contain incomplete features, placeholders, and breaking changes. Use with caution and refer to the source code for the latest status.

🎖️ Acknowledgments: This project is inspired by the design of PyTorch via TorchLean (George et al., 2026) and CSLib. A warm thanks to the PyTorch and Lean communities for their support, and to everyone crazy enough to live at the intersection of formal verification and machine learning!

TorchLib brings deep learning primitives to Lean 4, combining expressive neural network construction with formal verification techniques.

It provides a composable layer system, automatic differentiation, a training loop, and certified robustness verification via Interval Bound Propagation (IBP) and CROWN.

• Core primitives - tensors, shapes, and basic operations
• Intermediate representation - computation graph IR for model inspection and transformation
• Layer library - composable building blocks (linear, activation, etc.)
• Model construction - high-level API for defining neural networks
• Automatic differentiation - forward and backward pass via Autograd
• Training - loss functions, optimizers, and training loops
• Formal verification - certified robustness bounds via IBP and CROWN
• Certificates - machine-checkable proofs of network properties

TorchLib/
├── Core.lean           # Core types and tensor primitives
├── IR.lean             # Intermediate representation
├── Layers.lean         # Layer definitions
├── Models.lean         # High-level model API
├── Runtime/
│   ├── Autograd.lean   # Automatic differentiation
│   ├── TorchLean.lean  # LibTorch/runtime bindings
│   └── Training.lean   # Training loop and optimizers
└── Verification/
    ├── Certificate.lean # Verification certificates
    ├── CROWN.lean       # CROWN bound propagation
    └── IBP.lean         # Interval Bound Propagation

• Lean 4 (see lean-toolchain for the exact version)
• Lake (included with Lean 4)

Add the following to your lakefile.toml:

[[require]]
name = "TorchLib"
git = "https://github.com/jgalego/torchlib"
rev = "main"

Then run:

lake update
lake build

git clone https://github.com/jgalego/torchlib
cd torchlib
lake build

lake build TorchLibTests
lake env lean scripts/RunTests.lean

Or run individual test modules:

lake env lean TorchLibTests/Core.lean
lake env lean TorchLibTests/Autograd.lean
lake env lean TorchLibTests/IBP.lean

Runnable examples live in the examples/ directory.

Each file is self-contained and can be checked individually:

lake env lean examples/Tensors.lean
lake env lean examples/LinearLayer.lean
lake env lean examples/MLP.lean
lake env lean examples/Autograd.lean
lake env lean examples/Training.lean
lake env lean examples/Verification.lean
lake env lean examples/VerificationMNIST.lean

Here's a feature-by-feature comparison between TorchLean and this implementation:

✅ = implemented   🚧 = partial / stub   ❌ = not implemented

This project is licensed under the MIT License. See LICENSE for details.