TorchLean includes runnable training, autograd, data-loading, export, generation, and verification examples. Each page records the command, input data, produced artifact, and the claim checked by Lean.

TorchLean graph IR to interval bounds example Graph IR and Bounds Follow a small model as it becomes a graph with named operations, then use that graph for shape checks, execution traces, and interval bounds. Open guide page Autograd basics example Autograd Basics Compute gradients for small tensor functions, then inspect the tape and VJP objects that make reverse mode explicit. Open guide page MLP and CNN training example Supervised Training Instantiate supervised models, build loaders, fit for multiple epochs or fixed steps, and save loss curves from the same Lean runner. Open training guide Diffusion on real images example Diffusion Train a small denoiser, run deterministic DDIM sampling, and inspect both the generated images and the saved loss log. Open diffusion walkthrough GPT-2 style text example GPT-Style Text Tokenize bytes, build next-token examples, train a small causal transformer, save parameters, and sample continuations. Open text walkthrough Scientific ML pipeline from Burgers data to FNO training and Lean checks Scientific ML Prepare the Burgers dataset, train a 1D Fourier neural operator, export prediction artifacts, and connect PDE residual checks to Lean. Open scientific ML pipeline PyTorch round-trip example PyTorch Round Trip Move weights across the Python boundary while keeping tensor shapes, parameter packs, and import checks visible. Open interop guide Float32 and IEEE-754 checks example Float32 and IEEE-754 Compare real specifications, rounded FP32 models, executable IEEE bit semantics, and runtime Float32 bridge assumptions. Open floating-point guide Numerical certificate and binary32 replay for a two-layer MLP Numerical Runtime Certificates Run a two-layer MLP through operation coverage, interval propagation, backend-capsule audit, and bit-level binary32 replay. Open the complete run Reinforcement learning examples Reinforcement Learning Run PPO on Lean-native and Gymnasium environments, then inspect the rollout, reward, and policy artifacts that enter training. Open RL guide Bug Zoo case studies Bug Zoo See how common ML bugs become small Lean contracts: causal masks, KV caches, token ids, normalization state, batching, and Float32 behavior. Open Bug Zoo walkthrough 3D Vision Certificates example 3D Vision Certificates Export camera and box tensors from a detector, recompute projection in Lean, and reject boxes that do not enclose projected corners. Open 3D vision tutorial IBP and alpha-CROWN verification example IBP and CROWN Verification Attach input boxes to an IR graph, propagate interval or affine bounds, and check small external certificates through Lean. PINN examples use the same artifact-first style. Open verification tutorial

CUDA is opt-in. The build flags, runtime path, and agreement assumptions are explained in GPU and CUDA. For the broader backend design, read Backend Selection and Trust. For long CUDA training runs, model commands also expose allocator telemetry through --cuda-mem-watch N; longer runs choose a small default cadence so device-memory behavior is visible while the example is running. The report separates live tensor storage from released blocks kept for reuse. Set TORCHLEAN_CUDA_CACHE_CAP_BYTES before launch to bound that reuse cache; the GPU chapter shows the command and explains the allocator fields.

The command registry is:

lake exe torchlean --help
lake exe verify --help

The help output is the authoritative list of runnable entry points and their current flags.