How Short Can a Branchless Sort Be? Certified Optimality of AlphaDev's sort3 and sort4 Kernels, and What Stands in the Way for sort5

AlphaDev (Nature 2023) found x86 kernels that sort 3, 4 and 5 integers in 17, 28 and 42 instructions. We ask whether shorter kernels exist. We state a precise model (mov, cmp, cmovl, cmovg, cmovle, cmovge on signed 32-bit values, inputs and outputs in memory, every instruction counted, unbounded registers, correctness for all inputs with ties and all initial register and flag values) and reduce the question to a finite search through a chain of lemmas, each with a paper proof and a Lean 4 proof. Results: (i) sort3 needs 17 instructions, with ten independent proofs, among them LRAT certificates checked by the verified checker cake_lpr, a Lean theorem that uses only the Lean kernel and the three standard axioms, and a Rocq proof. (ii) sort4 needs 28 instructions, by an exhaustive search over 1.39e9 abstract states with reviewed pruning rules; its certificate is checked in Lean up to k <= 17. (iii) For sort5 we find no kernel shorter than 42; we find a second kernel family with 8 instead of 9 comparisons, show that no pure min/max kernel of length <= 41 exists and that garbage registers never help, and isolate the remaining open case. (iv) If cmp and cmov may read memory (legal on x86, excluded by AlphaDev), the kernels fit in 7, 15, 26 and 39 instructions for n = 2..5. Code, programs and proofs: https://github.com/jeffchen006/alphadev-sort-optimality