{"id":"arxiv/2602.22631","url":"https://arxiv.org/abs/2602.22631","tags":["cs.MS","cs.LG","cs.LO","cs.PL","math.NA"],"score":0,"title":"TorchLean: Formalizing Neural Networks in Lean","domain":"cs.MS","source":"arxiv","authors":["Robert Joseph George","Jennifer Cruden","Will Adkisson","Xiangru Zhong","Huan Zhang","Anima Anandkumar"],"reviews":0,"subject":"cs.MS","summary":"Neural networks are increasingly deployed in scientific, safety critical, and mission critical pipelines, yet verification and analysis are often performed outside the programming environment that defines and runs the model. This creates a semantic gap between the executed network and the analyzed artifact: guarantees can depend on implicit conventions about operator semantics, tensor layouts, preprocessing, floating-point behavior, graph transformations, accelerated kernels, and external certificates. We present TorchLean, a unified framework for formalizing, executing, and verifying neural…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-26","reactions":{}}