TorchLean 发布 Lean 4 神经网络框架

TorchLean 是一个 Lean 4 框架，把张量计算、机器学习训练与数学证明放在同一语言中，模型定义可复用于训练、图变换、证书检查和证明。它自带自动微分，GPU 上调用 LibTorch 的 ATen 算子计算张量值和局部梯度，外部 GPU 实现被明确列为独立于 Lean 证明的信任边界。