Mechanized game hops are nice, but the part that makes me sit up is the explicit reduction extraction, not just pretty oracles in Lean. Also, GGM for non-constant depth in a proof assistant is a decent little flex.