How do we know that these "internal models" are not just half computer and half a giant team of mathematicians?
How do we know that OpenAI actually came up with these solutions and didn't steal them from outside researchers?
Also lean proofs are notoriously tedious and slow to write so this level of output is very likely to be from LLMs. The number of people able to understand this level of math and prove it using Lean is a few hundred at most.
We'd have to accept that there are hundreds of such mathematicians willing to take the OpenAI stock options for that conspiracy to be true, and that no one leaked being offered that at all, so personally I don't think that's possible. Which leads me to conclude that OpenAI's AI did indeed create the proofs, with some level of help from humans to guide it.
We all know it’s only a matter of time before lawsuits in this area become widespread particularly in lawyer happy America.
There are suddenly many new solutions to problems that have resisted sustained attacks (e.g. the Uniform Games Conjecture as detailed in TFA at some length). Where do you think they are coming from? Why is there suddenly a bunch of results to be stolen?