Well perhaps we should use occam’s razor here.

If it doesn’t seem like the lllm understands the proof, it probably doesn’t.

Just because it generated something that works doesn’t mean it understands it, and the evidence from its proof is that it does not, which is not very surprising given the technology we’re talking about, which generates likely phrases based on a corpus and training.