Verified Deep Learning with Lean 4
1
Introduction
▶
What this book is about
The thesis
Who this book is for
Why now
Why image recognition
Why Lean
How to read this book
How this book is organized
A note on the proofs
Let’s go
2
Tensor: Calculus Foundations
3
MLP: Dense Layer
4
CNN: Convolution and Pooling
5
BatchNorm: the hard one
6
Residual: Skip Connections
7
Depthwise Convolution
8
Squeeze-and-Excitation
9
LayerNorm and GELU
10
Attention and the ViT finale
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
Axioms at a glance
Dependency graph
6 Residual: Skip Connections
Theorem
49
Residual block VJP
✓
#
Uses
Theorem 11
Theorem 13
L∃∀N
Lean declarations
Proofs.residual_has_vjp
Residual = \(f + \mathrm{id}\).