Let’s train a model, compute some gradients, or check a numerical claim in Lean. Pick an example below for the code and commands.

• Custom Tensor Computations Let’s square a tensor with an ordinary Lean function, then choose CPU or GPU when we run it. Try the CPU example directly in Lean’s Infoview.

• 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.

• Autograd Basics Compute gradients for small tensor functions and inspect the recorded operations and local gradient calculations.

• Supervised Training Build a model, load its training data, and train it in Lean. Save the loss curve to see how the run went.

• Diffusion Train a small denoiser, run deterministic DDIM sampling, and inspect both the generated images and the saved loss log.

• GPT-Style Text Tokenize bytes, build next-token examples, train a small causal transformer, save a checkpoint, and sample continuations.

• Scientific ML Train a Fourier neural operator on Burgers data or a PINN from an equation, then explore separate checks for PDE residuals and datasets.

• PyTorch Round Trip Export PyTorch weights, load them into a TorchLean model, and check that their shapes match.

• Checking a Captured Computation Use torchlean.verify with a PyTorch or JAX function. Check the graph’s types and shapes, then compare its mixed-precision outputs on an example.

• JAX Computations and Lean Proofs Bring a JAX function into the same graph IR, compare its outputs, and prove that a sum of squares is unchanged by permuting its inputs.

• Floating-Point Formats and Proofs Choose a floating-point format with FloatLib, compare rounded calculations, and see how we prove their numerical properties.

• Numerical Runtime Certificates Compute intervals for a small MLP, then replay its binary32 calculations and check each intermediate result.

• Reinforcement Learning Run PPO on Lean-native and Gymnasium environments, then inspect the rollout, reward, and policy artifacts that enter training.

• Bug Zoo See how common ML bugs become small Lean contracts: causal masks, KV caches, token ids, normalization state, batching, and Float32 behavior.

• 3D Vision Certificates Export camera and box tensors from a detector, recompute projection in Lean, and reject boxes that do not enclose projected corners.

• IBP and CROWN Verification Bound a model’s outputs over an input region using IBP or CROWN, and check certificates exported by other verification tools.