Installation

If you want to try TorchLean on a laptop, start with the CPU build. It does not require PyTorch, CUDA, or a GPU. The repository pins its Lean version in lean-toolchain, so Elan will select the right compiler for you.

A Five-Minute CPU Install

First install Elan, the Lean toolchain manager. On Linux or macOS:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Open a new terminal so that elan, lean, and lake are on your PATH. Then clone and build TorchLean:

git clone https://github.com/lean-dojo/TorchLean.git
cd TorchLean
lake exe cache get
lake build

The cache command downloads compatible prebuilt Lean dependencies when they are available. It is safe to omit; lake build will compile anything that is missing.

Run a small model to check the executable path:

lake exe torchlean quickstart_mlp --device cpu --steps 10

If those commands succeed, TorchLean is installed. You can inspect the available examples and verification commands with:

lake exe torchlean --help
lake exe verify --help

That CPU build is the common starting point on every platform. From there, TorchLean can build its native CUDA runtime or link an external provider without changing the Lean model being run. The table below separates paths that work today from targets that are represented in the backend architecture but still need platform-specific runtime work.

Platform CPU NVIDIA GPU LibTorch provider Current status
Linux ✓ ✓ Native CUDA SDPA forward with TorchLean backward Supported
macOS, Intel or Apple silicon ✓ Not applicable Not yet CPU supported; Metal is planned
Windows with WSL2 ✓ Linux path ✓ CUDA on WSL2 Linux path Recommended Windows setup
Native Windows Bring-up target Not validated Not wired Backend target exists; native toolchain work remains

Here, “LibTorch provider” means the current scaled-dot-product-attention bridge, not a requirement for ordinary TorchLean models and not a claim that every operation is delegated to PyTorch. The CPU, native CUDA, and LibTorch sections below give the corresponding build commands.

Linux

CPU

You need Git, curl, and a C/C++ compiler. On Ubuntu or Debian:

sudo apt update
sudo apt install -y git curl build-essential

Then follow the five-minute install above. The default build uses the portable CPU runtime. It also builds harmless CUDA stub archives so that CPU-only machines can compile the complete Lean project; the stubs do not pretend that a GPU is present.

NVIDIA CUDA

Install a supported NVIDIA driver and CUDA toolkit using NVIDIA’s CUDA Installation Guide for Linux. TorchLean needs nvcc, cuBLAS, and cuFFT. Check the machine before rebuilding:

nvidia-smi
nvcc --version

Build and run the CUDA configuration:

lake -R -K cuda=true build
lake -R -K cuda=true exe torchlean quickstart_mlp \
  --device cuda --steps 10 --show-backend

The two CUDA choices happen at different times. -K cuda=true tells Lake to compile and link the native CUDA implementation. --device cuda asks the executable to use it. A CPU-linked executable rejects --device cuda instead of silently moving the run back to the CPU.

Use -R whenever you switch between CPU and CUDA configurations; it forces Lake to recompute the build description. The CUDA regression suite is:

lake -R -K cuda=true exe nn_tests_suite

The CUDA guide covers deterministic reductions, parity checks, sanitizers, and the remaining native-code trust boundary.

Optional LibTorch Attention

The normal CPU and CUDA builds do not need LibTorch. TorchLean currently uses LibTorch only through an optional scaled-dot-product-attention bridge. Download a matching GPU-enabled distribution from the official LibTorch installation page and extract it somewhere outside the repository.

The extracted directory must contain include/ and lib/. Pass its absolute path to Lake:

lake -R -K cuda=true -K libtorch=true \
  -K libtorch_home=/absolute/path/to/libtorch build
lake -R -K cuda=true -K libtorch=true \
  -K libtorch_home=/absolute/path/to/libtorch exe libtorch_sdpa_test

This enables the libtorch_forward_cuda profile for scaled-dot-product attention. The backend chapter explains its per-operation selection and backward boundary.

macOS

Install Apple’s command-line developer tools, then Elan and TorchLean:

xcode-select --install
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
git clone https://github.com/lean-dojo/TorchLean.git
cd TorchLean
lake exe cache get
lake build
lake exe torchlean quickstart_mlp --device cpu --steps 10

The CPU path works on Intel and Apple silicon. Modern macOS has no NVIDIA CUDA execution path. TorchLean already reserves --device metal in its device vocabulary, but Metal/MPS kernels are not implemented yet. Selecting Metal therefore returns an unsupported-device error; it does not quietly run the CPU implementation.

Windows

The most reliable Windows setup is Ubuntu under WSL2. Open an administrator PowerShell prompt:

wsl --install -d Ubuntu

After Windows restarts, open Ubuntu and follow the Linux instructions. For an NVIDIA GPU, follow NVIDIA’s CUDA on WSL guide. Install the Windows NVIDIA driver and the CUDA toolkit inside WSL; do not install a second Linux display driver inside WSL.

Native Windows

Native Windows is represented in the backend target vocabulary, but it is still a bring-up target rather than a regularly tested release path. Install Git, the Visual Studio C++ build tools, and the Windows SDK. Then install Elan from PowerShell:

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

The intended native CPU commands are:

lake exe cache get
lake build

The remaining work is platform engineering: the native libraries must be compiled with a compatible Windows C/C++ toolchain; CUDA and LibTorch must be discovered as .lib and DLL artifacts; Linux linker options such as -Wl,-rpath must be replaced; and the CPU stubs and GPU runtime must be tested under the Windows loader and ABI. Once those pieces are wired, the existing device, provider, and capsule abstractions do not need to be redesigned. Until then, WSL2 is the supported route for both CPU and NVIDIA GPU execution on Windows.

Use TorchLean From Another Lean Project

Add TorchLean to the downstream project’s lakefile.lean:

require TorchLean from git "https://github.com/lean-dojo/TorchLean.git" @ "main"

Then update and build:

lake update
lake exe cache get
lake build

Most model files need only:

import NN.API
open TorchLean

The numerical library has a smaller independent import:

import NN.Floats
open TorchLean.Floats

It includes formats, rounding, finite binary32 semantics, executable IEEE binary32 operations, interval rounders, and scalar quantization. It does not load the tensor, model, autograd, CUDA, certificate, or external-tool layers. Use NN.Spec.Quantization when tensor quantization is needed, and NN.Proofs.RuntimeApprox.FP32 when connecting binary32 arithmetic to runtime-approximation proofs.

For development against a neighboring checkout, use a path dependency:

require TorchLean from "../TorchLean"

From A Model To A Kernel

Installation chooses a device or a complete backend profile; the model API stays the same. The planner then selects an implementation per operation and rejects unavailable providers instead of quietly changing the request.

Read Inside the Backend Planner for capsules, provider preference, VJP ownership, assurance policies, and backend reports. Read From a Tensor Operation to a GPU Kernel for native CUDA dispatch, boundary checks, determinism, and the current operation coverage.

Check An Installation

These commands cover the normal CPU installation:

lake build
lake lint
lake exe nn_tests_suite
lake exe torchlean --help
lake exe verify --help

For CUDA, rebuild and run the suite with -R -K cuda=true.

For a complete account of Lean axioms, executable checkers, CUDA and FFI code, external artifact producers, and floating-point assumptions, read TRUST_BOUNDARIES.md.

References