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 answered similarly to another comment; this is a common question)

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?

How would these ideas be available to steal?

It would be extremely unlikely human mathematicians able to solve these kinds of problems would accept not getting credit that would set them for life professionally.

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.

Until this is replicated, we don’t.