TorchLean v1

Excited to release TorchLean!

This release is pinned to Lean v4.29.0.

Highlights

• Typed tensor and model APIs through the public NN.API surface.
• Runnable model examples through lake exe torchlean, including MLP, CNN, sequence/text models, generative examples, FNO, and RL workflows.
• Verification CLI workflows through lake exe verify, including TorchLean-to-IR and IBP-style examples.
• Shared graph infrastructure through NN.IR and NN.GraphSpec.
• Runtime/autograd infrastructure, optimizers, training loops, logging, and optional CUDA-backed execution.
• Finite-precision and IEEE-style executable semantics under NN/Floats.
• Proof layers for tensor algebra, autograd correctness, runtime approximation, learning theory, CROWN/LiRPA-style robustness, and related ML theory.
• BugZoo examples turning common ML failure modes into small checked contracts.
• Project website, guide, and API docs sources included in the repository.