TorchLean: Specifying, Executing, and Formally Verifying Neural Networks with Lean 4

TorchLean is the first unified framework based on Lean 4 that supports the specification, execution, and mathematical correctness verification of neural networks. It aims to bridge the gap between neural network development and formal verification, providing a new path for the interpretability and safety of AI systems. This framework integrates three core capabilities—specification definition, execution, and verification—allowing developers to complete the entire process from concept to deployment to correctness assurance within the same framework.

Deep learning models have achieved success in many fields, but their 'black box' nature makes it difficult to ensure their behavior meets expectations. Traditional testing only provides statistical confidence and cannot guarantee compliance with constraints under all inputs, which poses an obstacle in safety-critical domains. Formal verification ensures system specifications through mathematical proof, but the high-dimensional tensors, floating-point operations, and non-linear activation functions of neural networks make them difficult to handle with traditional tools.

TorchLean integrates three core capabilities: 1. Use Lean 4's dependent type system to define network architecture, parameters, and constraints; 2. Compile Lean definitions into PyTorch code for execution; 3. Use Lean 4 theorem proving to verify mathematical properties. The technical architecture includes: formal definition of tensor operations (compile-time shape checking), semantic-preserving compilation from Lean to PyTorch, and composable abstractions of predefined network layers with specifications. As a dependent type language, Lean 4 supports provable programming, which is the technical foundation of TorchLean.

TorchLean has practical value in multiple domains: 1. Safety-critical systems (autonomous driving, medical care, etc.): Prove core properties of controllers; 2. Interpretability research: Prove that models satisfy properties in advance instead of post-hoc explanation; 3. Model compression: Prove that compressed models retain key properties; 4. Education: Help students build precise mathematical intuition.

TorchLean is hosted on GitHub under the MIT license. As of May 2026, it has 59 stars and 6 forks. It collaborates with LeanDojo to promote the bidirectional development of AI and mathematics, with tags including ai4math, theorem-proving, and neural-network, reflecting its interdisciplinary positioning.

Current challenges include: scale issues (difficulty handling large models), floating-point precision (rounding errors affect proofs), specification writing (defining specifications for complex tasks), and toolchain maturity (need to improve predefined layers and documentation). In the future, these issues need to be addressed to expand TorchLean to industrial-grade applications.

TorchLean marks the shift from empirical-driven to principle-driven neural network development, providing a technical foundation for trustworthy AI. As AI is increasingly applied in critical domains, formal verification may become a standard practice. Project address: https://github.com/lean-dojo/TorchLean, Documentation: https://lean-dojo.github.io/TorchLean/