1. Introduction🔗

Before touching an optimizer, we need a reason to put a neural network in a proof assistant at all. We begin with a prediction whose surrounding claim is unclear, learn just enough Lean to read the code, and then write the regression model that will stay with us through the rest of the book.

1. 1.1. The Problem TorchLean Solves
2. 1.2. Why Running The Model Is Not The Whole Story
3. 1.3. A First Walk Through The API
4. 1.4. Why The Model Is Written As A Function
5. 1.5. Enough Lean To Begin
6. 1.6. TorchLean and PyTorch
7. 1.7. A Running Example