These examples cover the main TorchLean workflows: graph lowering, autograd, supervised training, model zoo runs, interop, floating-point semantics, reinforcement learning, verification, and certificate checking. Each page starts from runnable code or a concrete artifact, then points to the guide or API entry point that defines, lowers, checks, or visualizes the same object.

TorchLean graph IR to interval bounds example Graph IR and Bounds Lower a model to `NN.IR.Graph`, inspect node shapes, then use the same graph for execution and verifier passes such as IBP. Open graph walkthrough Autograd basics example Autograd Basics Run reverse-mode examples, inspect gradients and VJPs, and see how executable tape objects connect to the autograd proof API. Open autograd walkthrough 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 model examples API Diffusion on real images example Diffusion Train an epsilon-prediction denoiser, run deterministic DDIM sampling, and compare images plus JSON loss logs. 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 Mamba text model example Mamba Text Model Use the same corpus and logging path with a compact state-space sequence model instead of attention. Open text walkthrough PyTorch round-trip example PyTorch Round Trip Export or import weights across the Python boundary while keeping tensor shapes, parameter packs, and trust assumptions explicit. 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 float guide Reinforcement learning examples Reinforcement Learning Run PPO examples for GridWorld, CartPole, and Pong RAM, with policy-gradient code and viewer pages separated cleanly. Open RL API Bug Zoo case studies Bug Zoo Study attention masks, KV caches, tokenizer boundaries, normalization state, batch invariance, and float/autograd boundary contracts. 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. Open verification tutorial

CUDA is opt-in and treated as a boundary. The build flags and assumptions are explained in GPU and CUDA.