Now, that still doesn’t help an LLM distinguish between good and bad correct proofs. But it still really helps a lot. On top of that, taste in proofs is a lot more uniform than taste in coding. That helps LLMs be better at judging the quality of a proof, because there’s less disagreement in the wider world.
(Although in general, there's no true difference between "I answered the question correctly, but the question was mapped to this thing we call 'reality' wrong", and "I answered the question incorrectly", because you can (try) adding the constraints that you really wanted targeted in case A, to case B, and boom, suddenly a question/answer pair that was "Answered correctly, but question doesn't map to reality" now becomes, "You answered this question wrong". However, individuals generally tend to have some breakpoint to differentiate between the two).