Maybe that particular proof wasn't in its training data, and presenting it in the input added it to the model's corpus for your session?

These models seem to work similarly with code. If you ask them to recreate something that appears in hundreds of GitHub repositories, no problem, a little bit of rubber-ducky debugging and you'll have a working solution. If you ask it for something novel, without many publicly-available implementations, the quality of its output appears to drop off a cliff.