> I can say the first LLM generated proof Levent sent me was the most horrendous I have ever read; we verified it on Lean on August 22nd. Since this point, we have been working around the clock to understand this proof and turn it into something readable.

People are acting as if OpenAI's cold machines snatched the result from the warm hands of human researchers. That's why people are so involved, they see it as humans vs. machines.

But in reality, those humans in question rely heavily on AI and would not be able to do what they did without AI. So the situation can be seen as "humans are trying to minimize the impact AI/incl. OpenAI had on getting a solution".

The situation is not "humans vs. machines", but "machines with a tiny bit of human involvement vs. machines with an even smaller amount of human involvement".

However much the researcher's chat history may have influenced AI, this pales in comparisson to how much AI has influenced researchers. They are not even closely in the same universe. The conversation about the level of plagiarism is silly.