Explore how TorchLean is organized: which modules import each other, where the main hubs are, and how the API, runtime, proof, and verification layers connect.
Looking for the interactive graph?
Open the module import graph.
This page starts from Lean imports. A module edge means one Lean file imports another; it does not
mean every theorem in the source file depends on every theorem in the target file.
Repository Shape
The longest chain counts the longest path through direct imports in this build. It is a rough measure of layering depth, not a correctness result.
Loading dependency audit…
Codebase Snapshot
These counts are generated from the Lean source tree during the site build. They are useful scale indicators, not semantic proof-dependency measurements.
Loading codebase statistics…
Largest Layers By Source Lines
Module Explorer
Click a module to see its direct imports and direct importers. Edges are module imports, not
theorem-premise dependencies.
Matching Modules
Selected Module
Select a module on the left.