用 Lean 从零证明 Transformer 不变量，全部证明由 AI 完成

srush_nlp · x · 2026-09-16

Srush 发布「Lean Verified Transformers」项目：在 Lean 中从零证明 Transformer 的一系列关键不变量与等变性，包括张量并行、数据并行、batch 不变性、置换不变性、tiling 正确性以及稀疏注意力模型的局部性。

项目的分工方式很特别：博客的文字、注释与结构全部由人撰写，而所有证明均由 AI 完成。作者认为，随着证明成本快速下降、AI 生成代码量激增，经过形式化验证的代码价值将显著上升；与 AI 协作去证明「易于理解的性质」是人机协作的自然中间地带。文章也可作为 Lean 的高级入门材料，受 TorchLean、Verified Deep Learning with Lean 4 和 Dex 语言启发。