Introduction
▶
What this book is about
The thesis
Who this book is for
Why now
Why image recognition
Why Lean
Let’s go
How this book is organized
▶
Theorem and definition budget per chapter
Roadmap: skip to your target architecture
For readers of the first book
Foundations
▶
Mathlib’s
fderiv
Why VJPs, not Jacobians?
1
MNIST: linear classifier
▶
How the proofs are written.
1.1
The theorems
1.2
Example: MNIST linear classifier
1.3
MLIR: Linear
1.4
What’s inside
.train
?
1.5
MLIR: Training Step
2
MNIST: 1D MLP
▶
2.1
The theorems
2.2
Example: MNIST MLP
2.3
Return on width
2.4
MLIR: Dense
3
MNIST: 2D CNN
▶
3.1
The theorems
3.2
Example: MNIST 2D CNN
3.3
MLIR: Convolution
4
CIFAR with BatchNorm
▶
4.1
The theorems
4.2
Example: training dynamics on CIFAR
4.3
MLIR: BatchNorm
5
ResNet-34
▶
5.1
The theorem
5.2
Example: ResNet-34 on Imagenette
5.3
MLIR: Residual
5.4
What’s in the production recipe?
5.5
Ablation: what each ingredient contributes
5.6
ImageNet recipe
6
MobileNetV2
▶
6.1
The theorems
6.2
Example: MobileNet V2 on Imagenette
6.3
MLIR: Depthwise Convolution
6.4
ImageNet recipe
7
EfficientNet
▶
7.1
The theorem
7.2
Example: EfficientNet-B0 on Imagenette
7.3
MLIR: Squeeze-and-Excitation
7.4
ImageNet recipe
7.5
Side quests
8
ConvNeXt
▶
8.1
The theorems
8.2
Example: ConvNeXt-T on Imagenette
8.3
MLIR: Layer Scale
8.4
Data Augmentation
8.5
ImageNet recipe
9
Vision Transformer
▶
9.1
Matrix-level machinery
9.2
Attention proofs
9.3
Example: ViT-Tiny on Imagenette
9.4
MLIR: Attention
9.5
Data Augmentation
9.6
ImageNet recipe
10
Bestiary of Architectures
▶
What “\(N\) new primitives” means.
10.1
Bestiary-only
Layer
primitives
10.2
Bestiary entries
A
Data availability
B
Getting started
▶
Track 1: No-GPU Docker demo
Track 2: Native install (CUDA or ROCm)
Track 3: Proofs only (no IREE needed)
Track 4: One-command demo tiers
Common troubleshooting
C
On Verification
▶
C.1
Trust kernel
C.2
Finite-difference gradient checks
C.3
The JAX parallel pipeline
C.4
Independent kernel re-check (comparator)
C.5
Verified code generation
C.6
Inside a bridge theorem
C.7
Float32: closeness, composition, and whether it still trains
C.8
The five layers, as three kinds of certainty
C.9
What each chapter proves
Acknowledgments
Colophon
Dependency graph
Verified Deep Learning with Lean 4
Brett Koonce
Introduction
What this book is about
The thesis
Who this book is for
Why now
Why image recognition
Why Lean
Let’s go
How this book is organized
Theorem and definition budget per chapter
Roadmap: skip to your target architecture
For readers of the first book
Foundations
Mathlib’s
fderiv
Why VJPs, not Jacobians?
1
MNIST: linear classifier
How the proofs are written.
1.1
The theorems
1.2
Example: MNIST linear classifier
1.3
MLIR: Linear
1.4
What’s inside
.train
?
1.5
MLIR: Training Step
2
MNIST: 1D MLP
2.1
The theorems
2.2
Example: MNIST MLP
2.3
Return on width
2.4
MLIR: Dense
3
MNIST: 2D CNN
3.1
The theorems
3.2
Example: MNIST 2D CNN
3.3
MLIR: Convolution
4
CIFAR with BatchNorm
4.1
The theorems
4.2
Example: training dynamics on CIFAR
4.3
MLIR: BatchNorm
5
ResNet-34
5.1
The theorem
5.2
Example: ResNet-34 on Imagenette
5.3
MLIR: Residual
5.4
What’s in the production recipe?
5.5
Ablation: what each ingredient contributes
5.6
ImageNet recipe
6
MobileNetV2
6.1
The theorems
6.2
Example: MobileNet V2 on Imagenette
6.3
MLIR: Depthwise Convolution
6.4
ImageNet recipe
7
EfficientNet
7.1
The theorem
7.2
Example: EfficientNet-B0 on Imagenette
7.3
MLIR: Squeeze-and-Excitation
7.4
ImageNet recipe
7.5
Side quests
8
ConvNeXt
8.1
The theorems
8.2
Example: ConvNeXt-T on Imagenette
8.3
MLIR: Layer Scale
8.4
Data Augmentation
8.5
ImageNet recipe
9
Vision Transformer
9.1
Matrix-level machinery
9.2
Attention proofs
9.3
Example: ViT-Tiny on Imagenette
9.4
MLIR: Attention
9.5
Data Augmentation
9.6
ImageNet recipe
10
Bestiary of Architectures
What “\(N\) new primitives” means.
10.1
Bestiary-only
Layer
primitives
10.2
Bestiary entries
A
Data availability
B
Getting started
Track 1: No-GPU Docker demo
Track 2: Native install (CUDA or ROCm)
Track 3: Proofs only (no IREE needed)
Track 4: One-command demo tiers
Common troubleshooting
C
On Verification
C.1
Trust kernel
C.2
Finite-difference gradient checks
C.3
The JAX parallel pipeline
C.4
Independent kernel re-check (comparator)
C.5
Verified code generation
C.6
Inside a bridge theorem
C.7
Float32: closeness, composition, and whether it still trains
C.8
The five layers, as three kinds of certainty
C.9
What each chapter proves
Acknowledgments
Colophon