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
8 Squeeze-and-Excitation
Theorem
54
SE block VJP
✓
#
Uses
Theorem 12
Theorem 33
Theorem 13
L∃∀N
Lean declarations
Proofs.seBlock_has_vjp
SE multiplies input by a sigmoid-gated channel mask.