TorchLean codebase is now available! TorchLean is a Lean 4 framework for verified neural-network software. It supports typed tensors, runnable training, graph IRs, verified autograd, Float32/IEEE semantics, CROWN / IBP-style verification, certificate checking, PyTorch interop, and CUDA/GPU execution. After feedback and comments on our original post, we expanded TorchLean substantially: neural operators/FNOs, diffusion models, GPT-style text models, GPT-2-style runs, Mamba/state-space models, RL, 3D vision certificates, Bug Zoo case studies, PyTorch interop, and more. Project page: https://lean-dojo.github.io/TorchLean/ Codebase: https://github.com/lean-dojo/TorchLean… @Robertljg, Jennifer Cruden, Will Adkisson, Xiangru Zhong, @huan_zhang12 @caltech #MachineLearning #ScientificComputing #Lean #FormalVerification

TorchLean

Source: https://lean-dojo.github.io/TorchLean/ TorchLean formalizes neural network infrastructure in Lean 4, connecting typed tensor and layer specifications, runnable training examples, graph IR semantics, floating-point contracts, CUDA trust boundaries, and artifacts that Lean checkers can inspect.

The goal is a practical bridge between modern ML workflows and formal reasoning: models can be executed, lowered, inspected, imported from PyTorch-style pipelines, and checked against explicit mathematical contracts.

What TorchLean Gives You

Where It Fits

TorchLean sits between the software people already use and the proof artifacts they want to trust. The project is written inLean 4and uses a PyTorch-style surface where that makes model code easier to read. For the Python ecosystem, see the officialPyTorch documentation; for Lean itself, start with theLean documentation.

Paper / Citation

@misc{george2026torchleanformalizingneuralnetworks,
      title={TorchLean: Formalizing Neural Networks in Lean},
      author={Robert Joseph George and Jennifer Cruden and Xiangru Zhong and Huan Zhang and Anima Anandkumar},
      year={2026},
      eprint={2602.22631},
      archivePrefix={arXiv},
      primaryClass={cs.MS},
      url={https://arxiv.org/abs/2602.22631},
}