Skip to content
Back
Theme
Verified Deep Learning with Lean 4
2 min read
Original article ↗
1
Introduction
▶
What this book is about
The thesis
Who this book is for
Why now
Why image recognition
Why Lean
Let’s go
2
You Are Here
▶
How to read this book
How this book is organized
▶
Foundation: Mathlib’s
fderiv
Why VJPs, not Jacobians?
Worked example: the dense layer
Theorem and definition budget per chapter
Roadmap: skip to your target architecture
For readers of the first book
3
MNIST: 1D MLP
▶
3.1
Example: MNIST MLP
▶
Dataset overview
Architecture
Code: the full training program
Results
What is actually in those “20 502 chars”
3.2
What’s inside
.train
?
4
MNIST: 2D CNN
▶
4.1
Example: MNIST 2D CNN
▶
Architecture
Code: the full training program
Results
Why this network is still 99% dense-head
5
CIFAR with BatchNorm
▶
5.1
Example: the BN lift on CIFAR
▶
The two specs, differing by one keyword per layer
Training: one learns, one doesn’t
Where the BN lift actually lives
6
ResNet-34
▶
6.1
Example: ResNet-34 on Imagenette
▶
The architecture
Results
What’s in the production recipe?
6.2
Ablation: what each ingredient contributes
7
MobileNetV2
▶
7.1
Example: MobileNet V2 on Imagenette
▶
The architecture
Results
8
EfficientNet
▶
8.1
Example: EfficientNet-B0 on Imagenette
▶
The architecture
Results
8.2
Side quests
9
ConvNeXt
▶
9.1
Data Augmentation
10
Vision Transformer
▶
10.1
Example: ViT-Tiny on Imagenette
▶
The architecture
Results
What Part 1 has established
11
Bestiary of Architectures
▶
11.1
Bestiary-only
Layer
primitives
11.2
Bestiary entries
▶
11.2.1
Vision classifiers — Part 1’s primitives at scale
11.2.2
Object detection
11.2.3
Semantic segmentation
11.2.4
Image generation
11.2.5
Reinforcement learning
11.2.6
Beyond vision
A
Getting started
▶
Track 1: No-GPU Docker demo
Track 2: Native install (CUDA or ROCm)
Track 3: Proofs only (no IREE needed)
Common troubleshooting
B
On Verification
▶
B.1
Trust kernel
B.2
Finite-difference gradient checks
B.3
The JAX parallel pipeline
B.4
Independent kernel re-check (comparator)
B.5
The four layers, summarized
Acknowledgments
Dependency graph