TorchLean

1. Introduction🔗

These chapters establish the working model for the rest of the guide. We start with the basic question TorchLean answers: how can one codebase support neural network programs that run, graph artifacts that tools can inspect, and mathematical claims that Lean can check?

The introduction is meant to be read linearly. It first explains the motivation, then compares the TorchLean style with familiar PyTorch workflows, and finally follows a small classifier through the main representations that appear later in the book.

  1. 1.1. What TorchLean Is
  2. 1.2. Why Verification Matters
  3. 1.3. A Tour of the API
  4. 1.4. Why Functional Programming?
  5. 1.5. Lean as the Host Language
  6. 1.6. TorchLean vs. PyTorch
  7. 1.7. A Running Example