How to formally prove that random guess is the best attack
But how to argue there is no better algorithm than guessing?

Show that, if there is a better algorithm than guessing, you can distinguish the PRF from random.