What I mean is that one could choose a particular tactic to proving a lemma or even rely on certain lemma where that choice is intended for the audience the author has in mind in order to help them understand the steps better.
The context an LLM uses is limited (though growing). However its context is lacking the ability to understand the mind of the interlocutor and the proof they would expect or find helpful.
"Why this proof?" also has a more global context as well. It seems there are have been styles and shifts in cultural norms over the years in proofs. Even though the Elements stood up until the 19th century we don't necessarily write proofs in the style of Euclid even though we may refer to those themes and styles, on purpose, in order to communicate a subtle point.
Maybe a good proof golf game would be finding the least computationally intensive proof of tic tac toe or rubics cube or something.