Verified Deep Learning with Lean 4
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
▶
Roadmap: skip to your target architecture
For readers of the first book
Getting started
▶
Install
One command per tier
Foundations
▶
Mathlib’s
fderiv
Why VJPs, not Jacobians?
Inference and training
What the theorems cover, and what they leave to the run
1
The framework
▶
1
MNIST: linear classifier
2
MNIST: 1D MLP
3
MNIST: 2D CNN
4
CIFAR with BatchNorm
5
ResNet-34
6
MobileNetV2
7
EfficientNet
8
ConvNeXt
9
Vision Transformer
2
The bestiary
▶
10
The kit
11
The chapter nets at work
12
Beyond recognition
13
Game theory
Appendices
▼
A
Toolchain and platforms
B
On Verification
C
The ImageNet tier
D
Data availability
Acknowledgments
Colophon
Dependency graph
Appendices
A
Toolchain and platforms
Track 1: Proofs only (no GPU needed)
Platforms
Common troubleshooting
The second lowerer
B
On Verification
B.1
What each chapter proves
B.2
Proven: the math is right
B.3
By construction: the code is the math
B.4
Cross-checked
B.5
Finite precision
C
The ImageNet tier
This tier needs Python
Running one
Running one for a day and a half
Side quests
D
Data availability
Demo datasets
Acknowledgments
Colophon