I wish people would stop generating stuff they don't understand only to forward it to someone who does. Something about that really rubs me the wrong way.
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.
