In my limited experience it seems like the "why" of a proof requires a theory of mind from the perspective of the author of the proof.
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.
Though, say we finally solve chess. There's not always going to be a "why" the suggested move is the best. There might be heuristics, or even some set of rules in the end game or certain situations that a human's brain can retain to perfection. But for the vast majority of the game, the correct move is what it is, because that's what the computer says, and there's not much more you can do to simplify it.
Maybe a good proof golf game would be finding the least computationally intensive proof of tic tac toe or rubics cube or something.
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.