Comment by YeGoblynQueenne

>> I asked whether the model had been trained on, or had access to, our sessions in Codex, into which we had been putting all our drafts for the whole of this project. I was told the model did not look up user data. I asked again, about training, and I did not get an answer.

This sounds like a very big coincidence and it looks really bad for OpenAI but there is an alternative explanation that I can only state as a conjecture.

Suppose that the ability of LLMs to generate mathematical proofs is like a quiver full of arrows: each arrow, one proof. The same quiver is shared between all instances of one model and substantially similar models share substantial subsets of the arrows in the same quiver.

That would allow two independent teams to converge on the same LLM-aided solutions to the same problems. Even more likely so if the quivers were small and finite and their arrows were specific to a distinct class of problems (without being able to suggest a particular class from what we've seen so far).

This would explain the kind of LLM-mediated results we've seen so far that tend to be ... sparse. By which I mean that every time there's a new model release we get some new results and then they seem to dry out, until the next release.

It would also explain how OpenAI was about to prove the same result as Buckmaster and Alpoge, while absolving OpenAI of any misconduct. And this is one reason to prefer this explanation: one should not favour accusations of misconduct as long as there are conceivable alternatives.

But, that's just a conjecture that I can't prove.