May I remind you that this is Timothy Gowers. He says he doesn't understand, but he most certainly has far greater capacity than most to detect complete junk from a maybe plausible argument. His colleague is even better able to judge this, hence why he sent it to him.
Also if he did send me complete junk, I would still parse it for multiple days to see what is there.
Yeah, it doesn't make a difference for me. It's the generation part. Gowers should have sent his prompts to the colleagues, not the generated paper. That's all. I feel like it's creating obligations for others to help with the remaining 20% which always takes the most time, while you get to have all the fun of doing the first 80%.
I'm not criticising Gowers directly in this instance because he's exploring the possibilities, my disdain is towards the more general pattern I see emerging where people just send each other LLM outputs.
No offense intended, but this sounds like you're projecting impressions about LLM output for programming. Your words make a lot of sense to me in that context, but not as much here.
I can speak with a reasonable amount of experience here. I absolutely guarantee you that what Gowers sent over was the vast majority of the work involved for a proof. It's also an interesting exercise in general, hence the blog post.
Parsing a proof like this is _much_ easier than creating it.
Parsing code often seems like the opposite in my experience, where it is more difficult than writing it yourself.
Also if he did send me complete junk, I would still parse it for multiple days to see what is there.