These examples show TorchLean at work on real machine-learning problems: training models, differentiating tensor programs, moving weights through PyTorch, and checking numerical or verification claims in Lean. Open an example for the runnable code and the theorem or contract behind it.

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 a checkpoint, 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 FloatLib configured binary32 and binary128 formats: sign, exponent, fraction, and normal significand precision. Floating-Point Formats and Proofs Compare FloatLib's executable binary arithmetic with rounded FP32 models and TorchLean's proofs of agreement with Lean's logical Float32 operations. 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