用 Lean 形式化 PTX 指导 GPU kernel 优化并提前发现测试遗漏错误

remior 重建 Lean 中的 PTX 形式化框架，并让 Claude 用它指导 GPU kernel 优化。形式化证明在测试前发现错误，其中还捕获了测试未能发现的 PTX 代码 `bar.sync` 同步问题。作者认为，这一证明驱动流程可加入 kernel 优化循环。