Skip to content
Back
Theme
Verified Deep Learning with Lean 4
2 min read
Original article ↗
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
5.7
Side quest: ResNet-50, RSB-A3 (100 epochs)
6
MobileNetV2
▶
6.1
The theorems
6.2
Example: MobileNet V2 on Imagenette
6.3
MLIR: Depthwise Convolution
6.4
ImageNet recipe
6.5
Side quest: MobileNet V4
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
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
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
Proven: the math is right
C.2
By construction: the code is the math
C.3
Cross-checked
C.4
Float32
Acknowledgments
Colophon
Dependency graph