3.4.1. The Contract🔗

The workflow is:

1. describe a small typed model family in Lean,

2. export a matching PyTorch scaffold,

3. train or modify the weights in Python,

4. serialize the learned parameters to JSON,

5. re-import them into Lean, where shapes and parameter order are checked again.

That design keeps the boundary between Lean and PyTorch small enough that, when something goes wrong, the failure is usually local and comprehensible: a mismatched name, a mismatched shape, or an unexpected model family.

3.4.2. What Lean Checks On Import🔗

The importer is intentionally strict. It checks the payload before constructing the typed parameter bundle used by the rest of TorchLean.

The checks include:

• the model family tag,

• the parameter names Lean expects for that family,

• the parameter order used by the typed bundle,

• the shape attached to each tensor,

• the number of values implied by that shape,

• the scalar payload format.

For example, if Lean expects:

linear1.weight : shape![8, 2]

but the JSON contains:

linear1.weight : shape![2, 8]

the import fails before the value becomes a model parameter. That is the behavior we want: a round-trip should either reconstruct the same typed layout, or stop at the boundary with a concrete error.

3.4.3. What Gets Serialized🔗

The round-trip does not serialize an arbitrary Python object graph. Instead it serializes a small amount of model family metadata plus a named tensor payload. The exact schema depends on the family, but the shape of the contract is always the same:

• choose a known architecture family,

• agree on parameter order and tensor layout,

• serialize tensors by name into JSON,

• re-check that layout on the Lean side before constructing typed parameters.

Lean then reconstructs the typed parameter bundle that the rest of TorchLean expects. The JSON file is transport, not semantics.

3.4.4. Model Families🔗

The repository uses three family demos.

lake env lean --run NN/Examples/Interop/PyTorch/Roundtrip.lean -- --model mlp --action export
python3 NN/Examples/Interop/PyTorch/MLP/train_mlp.py
lake env lean --run NN/Examples/Interop/PyTorch/Roundtrip.lean -- --model mlp --action import

lake env lean --run NN/Examples/Interop/PyTorch/Roundtrip.lean -- --model cnn --action export
python3 NN/Examples/Interop/PyTorch/CNN/train_cnn.py
lake env lean --run NN/Examples/Interop/PyTorch/Roundtrip.lean -- --model cnn --action import

lake env lean --run NN/Examples/Interop/PyTorch/Roundtrip.lean -- --model transformer --action export
python3 NN/Examples/Interop/PyTorch/Transformer/train_transformer.py
lake env lean --run NN/Examples/Interop/PyTorch/Roundtrip.lean -- --model transformer --action import

3.4.5. TorchLean, IR, and Generated PyTorch Code🔗

A second interop path complements the JSON round-trip workflow:

• file: Torch IR and PyTorch example

This example compiles a TorchLean model to the shared IR and then emits runnable PyTorch code for a curated set of architectures:

• linear, mlp, sum, autoencoder

• cnn, conv-mlp

• mha, mha-mask

• transformer

Typical usage:

lake exe torchlean torch_ir_pytorch --arch mlp > exported_model.py
python3 exported_model.py

This is useful for two reasons:

• it shows the compiled IR as an interchange boundary, not only as an internal verifier artifact;

• it gives PyTorch users a concrete translation example for architectures richer than a single linear layer.

3.4.6. A Small Python View🔗

The Python half is intentionally ordinary. The goal is not to replace the PyTorch workflow; the goal is to make the boundary between PyTorch and Lean explicit enough that it can be audited.

import torch

model = build_exported_model()
opt = torch.optim.Adam(model.parameters(), lr=1e-3)

for step in range(steps):
    pred = model(x_train)
    loss = torch.nn.functional.mse_loss(pred, y_train)
    opt.zero_grad()
    loss.backward()
    opt.step()

save_torchlean_json(model, "mlp.json")

That is the basic shape of the round-trip: Lean defines the expected structure, Python performs the training, and Lean checks the returned payload against the same structure.

3.4.7. Where This Fits In The Guide🔗

Use the round-trip when the training workflow belongs in Python but the returned artifact should enter the TorchLean world with typed parameters and auditable metadata. Use the runtime chapters when the training loop itself should run in Lean. Use the graph and verification chapters when the next step is to inspect the model as an IR object or connect it to a theorem.

3.4.8. Guarantees And Limits🔗

When the round-trip succeeds, the result is a controlled bridge between Lean and Python:

• Lean can emit a model skeleton and helper files.

• Python can train or export weights using a matching layout.

• Lean can read the exported payload back in and continue on the proof or verification side.

Limits matter as much as successes:

• this is not a proof that arbitrary PyTorch training is semantically identical to Lean execution,

• this is not a universal importer for the full PyTorch ecosystem,

• this does not by itself settle the floating-point semantics.

Binary32 claims still require the relevant TorchLean float backend and the theorems in the floating-point chapters.

For a PyTorch-side-by-side comparison, read TorchLean vs PyTorch. Verification after import: Graphs and IR, then Verification.

3.4.9. References🔗

• TorchLean paper (George et al., 2026): project overview, shared IR architecture, and verification-driven architecture. https://arxiv.org/abs/2602.22631

• PyTorch serialization notes: the official reference for state_dict-style save/load workflows. https://pytorch.org/docs/stable/notes/serialization.html

• PyTorch nn.Module documentation: helpful background for parameter naming and module-family conventions. https://pytorch.org/docs/stable/generated/torch.nn.Module.html