alt Hacker NewsIt 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.
Hm that's the question, innit. If you were a mathematician, and you have a chance at either being known for solving a particular problem, and the accolades that come with that, and the potential for money, or $X,000,000, for large values of X, in OpenAI stock, what value of X would it take to accept the OpenAI stock? Being known for solving an obscure math problem might get you money, but as academia is unreliable and full of politics, the OpenAI stock is also not a given to set you up with generational wealth, so it's also a gamble.
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.