Double Agent built explicit regular graphs whose shortest cycles beat the 4/3 bound Margulis and Lubotzky, Phillips and Sarnak set in 1988, pushing it to 8/5 with a Lean-checked proof, so the referee on new math is now a compiler.