[globular-toast]

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.

[hodgehog11]

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.