7.7.1. The Examples At A Glance🔗

The tree is organized around questions:

• Can I build and inspect small tensors? Read Quickstart.

• Can I train a model in Lean? Read Models and Data.

• Can I cross the PyTorch boundary without losing shapes? Read PyTorch interop.

• Can I see the graph that a verifier sees? Read Advanced GraphSpec and IR demos.

• Can I check a property or certificate? Read the verification examples and fixtures.

• Can I see common ML bugs as checked Lean case studies? Read Bug Zoo.

Most model demos run through one executable:

lake exe torchlean <demo> [args...]

The source-level umbrella is NN.Examples.Zoo. Building it is the quick health check for the curated example surface:

lake build NN.Examples.Zoo

7.7.2. Three Walkthroughs To Read First🔗

lake exe torchlean mlp --cpu --steps 10
lake exe torchlean cnn --cpu --n-total 20 --steps 1

lake exe verify -- torchlean-ibp

-- State the behavior directly, then make the boundary explicit.
#check Spec.hardMaskedSoftmaxSpec
#check runtimeFloat32_add_rewrites_to_ieee32

7.7.3. Fast Kernels, Bug Cards, and Verification🔗

A useful way to read the examples is as one chain:

1. Fast kernel: a runtime path uses an optimized implementation, such as fused CUDA attention.

2. Bug card: BugZoo states the semantic hazard, such as mask polarity, cache position mismatch, or floating-point boundary mismatch.

3. Contract: the spec names the intended mathematical behavior.

4. Checker or theorem: Lean checks an artifact, proves a local theorem, or records the remaining trust boundary.

For attention, the chain looks like this:

• Runtime: CUDA multi_head_attention may call fused native flashAttentionFwd and fused VJP kernels.

• Spec: Spec.flashAttention and Spec.scaledDotProductAttention name the forward contract.

• Theorem: flashAttention_eq_scaledDotProductAttention states that the fused spec denotes SDPA.

• Bug card: BugZoo.AttentionMask records the exact mask property, including future tokens getting zero attention under causal masking.

• Verification fixture: torchlean-transformer-ibp pushes a tiny transformer style graph through the same verifier surface.

This is the preferred TorchLean pattern: faster execution is welcome, but it is paired with a named semantic contract and a visible proof or test boundary.

The pattern is either equality with the spec, or membership in a safe enclosure around the spec.

If the equality is proved, the fast path becomes an optimization. If it is checked only by tests, we say that plainly. If the kernel is external CUDA code, the CUDA chapter names the assumption instead of letting it disappear into the demo.

7.7.4. How The Tree Is Organized🔗

The examples are grouped so each subtree has a job:

• Quickstart examples Typed-tensor warmups, autograd basics, and the smallest training tutorials.

• Model examples The main model zoo used by lake exe torchlean: MLP, CNN, ResNet, ViT, RNN/LSTM, Transformer, GPT text demos, Mamba demos, diffusion, and RL examples.

• Advanced examples GraphSpec, float-mode, tensor-bridge, and TorchLean-to-PyTorch IR demos.

• PyTorch interop examples PyTorch round-trip scripts and generated-code interop examples.

• Verification fixtures Small bundled certificate/checker demos used by lake exe verify -- ... (with untrusted producers under scripts/verification/).

• Widget gallery Infoview widgets used in the editor rather than through a long training run.

• RL widget viewers File-backed PPO/GridWorld dashboards colocated with the RL examples they visualize.

• Bug Zoo Small checked case studies for attention masks, KV caches, tokenizers, normalization state, batching, floats, and autograd boundaries.

• real data paths and model data helpers Shared paths and loaders for prepared real datasets under data/real.

That structure helps the examples read as one system: start with tensors, run models, lower graphs, then check properties.

7.7.5. A Good First Pass Through The Examples🔗

For one short pass that touches the main layers, use this order:

1. Build once: lake build

2. Build the curated examples umbrella: lake build NN.Examples.Zoo

3. Typed tensor demo: lake env lean --run NN/Examples/Quickstart/TensorBasics.lean

4. Float-backend comparison demo: lake exe torchlean float32_modes

5. Widgets demo, opened in the editor: open the widgets example API

6. Autograd demo: lake env lean --run NN/Examples/Quickstart/AutogradBasics.lean -- --dtype float

7. Model-zoo training demo: lake exe torchlean mlp --cpu --steps 10

8. Small complete verification demo: lake exe verify -- torchlean-ibp

Read the output alongside this book: training-focused material starts with Training From Scratch and Runtime and Autograd; graph and verification artifacts start with Graphs and IR, then Verification.

7.7.6. What Success Looks Like🔗

Expected outputs on a healthy run:

• tensor_api_demo: small typed tensors print cleanly.

• float32_modes_demo: the same numeric expression is evaluated under different float32 semantics.

• autodiff_demo: prints a value and a gradient, not only a successful build.

• lake exe torchlean mlp --cpu --steps 10: prints a short loss trace trending downward.

• lake exe torchlean gpt_adder --steps 50 --cuda (after lake build -R -K cuda=true): runs the minGPT addition demo on GPU when the CUDA backend has been built.

• torchlean-ibp: prints interval bounds for the output node, not raw graph internals.

This framing distinguishes a meaningful semantic check from a command that merely exits with code zero.

7.7.7. Dtype And Backend Flags🔗

Most training and runtime examples are written once and then instantiated by the command line wrapper with a scalar type and backend chosen on the command line.

7.7.8. Model zoo and real data🔗

The model surface is wide: classical feedforward and conv nets, ViT and ResNet blocks, recurrent and attention language models, state space and diffusion demos, and PPO RL environments, not only the original MLP/CNN tutorials. Model demos are driven by:

lake exe torchlean <demo> [flags...]

The model examples API contains the implementations, and the example runner API defines the public subcommand names.

First run:

lake exe torchlean --help

lake exe torchlean mlp --cpu --steps 10
lake exe torchlean cnn --cpu --n-total 20 --steps 1
lake exe torchlean resnet --cuda --n-total 20 --steps 1
lake exe torchlean vit --cuda --n-total 20 --steps 1
lake exe torchlean rnn --cuda --tiny-shakespeare --steps 1
lake exe torchlean transformer --cuda --tiny-stories --steps 1
lake exe torchlean mamba --cuda --tiny-shakespeare --steps 25
lake exe torchlean diffusion --cpu --steps 5
lake exe torchlean gpt2 --cuda --steps 1
lake build -R -K cuda=true && lake exe torchlean gpt_adder --steps 50 --cuda

7.7.9. Data Loading, Transforms, And Schedulers🔗

The NN/API/Data* surface is richer than a first glance suggests. The current tutorial set covers three increasingly realistic patterns:

• csv_loader_train Disk-backed tabular data, Data.Transforms.Compose, minibatch loaders, and a learning-rate schedule (train.stepEpochLR).

• npy_loader_train NumPy/PyTorch .npy interop with typed dataset reconstruction on the Lean side.

• cifar10_npy_cnn_train A more realistic offline image workflow: load .npy, split train/test, batch, train, and report accuracy.

Those are worth calling out because they answer a common question from PyTorch users:

Is TorchLean only comfortable with in-memory tutorial tensors?

The answer is no. The examples cover CSV and .npy file readers, typed transforms, deterministic batching, callbacks, and scheduler-driven training loops.

7.7.10. GraphSpec And Export Demos🔗

Two examples highlight newer architecture and interop work beyond the smallest tutorials.

7.7.11. BugZoo Case Studies🔗

BugZoo deserves its own reading pass because it explains what kinds of mistakes TorchLean is trying to make visible. The BugZoo API contains the checked cards, with the full motivation in the BugZoo overview.

The case studies are compact, but they cover a broad range:

• Shape and broadcast: missing axes and wrong broadcasts; TorchLean uses tensors indexed by shape and explicit broadcast evidence.

• Stable loss: unstable loss formulas and invalid domains; TorchLean names stable logit losses and safe-domain ops.

• Ignored labels: all-ignored label reductions; TorchLean uses an explicit contribution mask and empty-reduction policy.

• Autograd domain: masking after undefined division; TorchLean uses epsilon-protected division before masking.

• Attention mask: mask polarity and fully masked attention; TorchLean states exact causal-mask zero-weight properties.

• Compiler boundary: optimized graph wrong-code bugs; TorchLean asks for a source/target semantic preservation contract.

• Float boundary: real-proof versus float-deployment gaps; TorchLean names the bridge from runtime float32 to IEEE32Exec.

• Normalization state: BatchNorm formula/state mismatch; TorchLean makes epsilon placement and running statistics explicit.

• Batch invariance: serving output depends on batch composition; TorchLean states per-example batching behavior.

• KV cache: shifted or malformed decode cache; TorchLean names append-last key/value invariants.

• RoPE position: position mismatch during decoding; TorchLean names the position schedule.

• Tokenizer boundary: vocabulary/config mismatch; TorchLean represents token ids as Fin vocabSize.

These cards do not solve every production incident. They show a repeatable method: take a bug that normally sits inside an opaque runtime, name the boundary, and attach a small checked statement to it.

Useful build target:

lake build NN.Examples.BugZoo.All

For readers coming from ML systems, BugZoo is often the most concrete entry point: a recognizable bug class, the exact object TorchLean uses as the contract, and the theorem or boundary that follows.

7.7.12. Verification Application Workflows🔗

The verification side has also grown beyond one tiny IBP demo. The current example tree covers several distinct application styles.

7.7.13. A Paper-Oriented Reading Path🔗

To mirror the paper's example ordering, try:

1. simple_mlp_train

2. pytorch_loop_mlp_train

3. graphspec_mlp_demo

4. torchlean-ibp

5. torchlean-crown-ops

6. pinn-cert or pinn-cli

7. ode

8. vnncomp-mnistfc

That sequence starts with familiar training, then introduces typed authoring, then compiled IR, then the verifier workflows that are specific to TorchLean's research program.

7.7.14. Widgets In Practice🔗

Some of the most useful examples are not command line programs at all. They are editor files that render live views in the infoview.

The full widget family includes several views; the short list cited most often is:

• tensor views,

• graph and shape-inference views,

• float32 bit-layout views,

• verification-state views,

• autograd tape and gradient views.

Start with the widgets example API, then return here for a compact map of each widget family.

7.7.15. Smoke Tests🔗

After edits, the fastest regression check for the public surface is:

lake test

7.7.16. Adding A New Example🔗

Checklist for adding a new example to the curated zoo:

• Put it in the right subtree: NN/Examples/Models for model zoo demos, NN/Examples/Quickstart for small tutorials, NN/Examples/Advanced for architecture/IR demos, and NN/Examples/Verification + scripts/verification for verifier workflows.

• If it belongs in the public runner, register it in the model runner API and make sure NN.Examples.Zoo imports it.

• Use the public facade where appropriate: open NN.API and stick to nn, Data, train, and optim unless the example is explicitly advanced.

• Add a short module docstring at the top with:

  1. what the example demonstrates, and

  2. the exact lake env lean --run ... command.

• Parse flags consistently: support --seed when randomness is involved, and use train.run to parse --dtype and --backend.

• Keep it cheap by default: small dataset, small model, few steps or epochs; heavier runs remain behind flags.

There is a central model runner for model demos (lake exe torchlean ...), while advanced/tutorial files can still be run directly with lake env lean --run ....

Command-line overview: CLI Entry Points. From examples into the verifier stack: Graphs and IR, then Verification. For GPU build details, Runtime and Autograd.

7.7.17. References and further reading🔗

• George et al., TorchLean (2026): project overview. https://arxiv.org/abs/2602.22631

• Vaswani et al., Attention Is All You Need (2017): transformer baseline. https://arxiv.org/abs/1706.03762

• He et al., Deep Residual Learning (2015): ResNet. https://arxiv.org/abs/1512.03385

• Dosovitskiy et al., An Image Is Worth 16x16 Words (2020): ViT. https://arxiv.org/abs/2010.11929

• Ho, Jain, Abbeel, Denoising Diffusion Probabilistic Models (2020): DDPM. https://arxiv.org/abs/2006.11239

• Gu & Dao, Mamba (2023): selective state spaces. https://arxiv.org/abs/2312.00752

• Dao et al., FlashAttention (2022): IO-aware exact attention. https://arxiv.org/abs/2205.14135

• Odena et al., TensorFuzz (2019): fuzzing numerical failures. https://arxiv.org/abs/1807.10875

• Liu et al., NNSmith (2023): generated valid tests for DL compilers. https://arxiv.org/abs/2207.13066

• Schulman et al., Proximal Policy Optimization (2017): PPO. https://arxiv.org/abs/1707.06347

• PyTorch documentation: user-side analogy for NN.API. https://pytorch.org/docs/stable/index.html