8. Formalization Map🔗

The chapters below trace the main definitions, executable boundaries, and proved results through TorchLean. This is a declaration-level map: an edge records a mathematical or implementation dependency between selected entries, and theorem proof dependencies are tracked separately from statement dependencies. The website's Graphs tab remains the place to inspect Lean module imports.

The selection favors declarations that explain an entire subsystem. Small helper lemmas stay in the API reference, where their full statements and source locations are easier to inspect.

Use a map entry after the corresponding explanation has given its declaration a meaning. An enclosure theorem, for example, depends on local transfer laws and hypotheses about the graph; following those entries shows where its premises come from. A dependency edge alone does not say that a runtime path satisfies those premises. The entry's statement and explanatory text identify the objects being related, while the source link leads to the actual definition or proof.

1. 8.1. Tensors and Graphs
2. 8.2. Floating-Point Numerics
3. 8.3. Autograd and Execution
4. 8.4. Backends and Training
5. 8.5. Verification
6. 8.6. Models and Mathematical Examples