Super excited to release TorchLean!! I’m happy to answer questions and would love to discuss verified NNs + theorem proving especially what it’ll take for the field to become widely usable in real ML systems. Blog post + codebase release soon! Prof. Anima Anandkumar (@AnimaAnandkumar) We’re excited to release TorchLean which is the first fully verified neural network framework in Lean. The Lean community has largely focused on pure mathematics. TorchLean expands this frontier toward verified neural network software and scientific computing. With the recent release of CSlib, we see this as another step toward a fully verified ML stack. We support features: 1. Executable IEEE-754 floating-point semantics (and extensible alternative FP models) verified tensor abstractions with precise shape/indexing semantics 2. Formally verified autograd system for differentiation of NN programs Proof-checked certification / verification algorithms like CROWN (robustness, bounds, etc.) 3. PyTorch-inspired modeling API with eager-style development + export/lowering to a shared IR for execution and verification Project page: leandojo.org/torchlean.html Paper: [2602.22631] TorchLean: Formalizing Neural Networks in Lean Work done @Robertljg, Jennifer Cruden, Xiangru Zhong, @huan_zhang12 and @AnimaAnandkumar. #MachineLearning #ScientificComputing #Lean — https://nitter.net/AnimaAnandkumar/status/2027907453908857298#m

→ View original post on X — @animaanandkumar, 2026-03-01 22:38 UTC