用 Lean 形式化 NVIDIA PTX 指令集，证明 AI 编写的 GPU 内核正确

开发者 BenKoska 宣布将 NVIDIA 的 PTX 指令集在 Lean 定理证明器中形式化，以对 GPU kernel 进行形式化正确性证明。该项目面向越来越多由 AI agent 编写的 GPU 内核，旨在提供无需逐行阅读代码、也能验证内核正确性的“AI 写代码 + 机器验证”工作流。