How AI helped auction off $19-billion worth of radio spectrum