TY - RPRT TI - Formalizing PTX in Lean to Prove GPU Kernel Correctness AU - Luk Koska AU - Tom Koska AU - Ben Koska PY - 2026 UR - https://arxiv.org/abs/2611.04447 ID - 2611.04447 ER -