TorchLean API Docs

Exact declarations, organized by API surface.

These pages are generated from Lean. Use the cards below for the main TorchLean surfaces, then use search when you need a specific definition, theorem, or module.

Read the Guide Run an Example Search Declarations

Recommended import NN.Library

The broad umbrella import for ordinary downstream use.

User facade NN.API.Public

The PyTorch-shaped public surface for model code and examples.

Tensors NN.Tensor.API

Tensor operations, shapes, and the user-facing tensor layer.

Graph IR NN.IR.Graph

The op-tagged graph representation used by lowering and verification.

Semantics NN.IR.Semantics

The executable meaning attached to IR operators and graph evaluation.

Runtime NN.Runtime.Autograd.TorchLean

Runtime autograd, compiled execution, and training support.

Verification NN.Verification.CLI

The registered certificate and verification command surface.

Float32 NN.Floats.IEEEExec

Executable IEEE-754 binary32 semantics used in float audits.

Browse By Layer

API Spec Runtime IR GraphSpec Proofs Verification Examples

Common Tasks

Start from the thing you want to do, then jump into the declaration namespace from there.

Write model code Public tensor and layer facade. Inspect lowering The shared graph object that verification and execution read. Run autograd Runtime training and reverse-mode execution entrypoints. Check certificates Commands and declarations used by verification demos.

Declaration Legend

The colored stripe on each declaration page marks what Lean generated.

def / instance theorem structure / class axiom / opaque