Perhaps, but due to the slop nature of OpenAI proofs, the proofs remain unaccepted by mathematicians, which leads one to question how many are valid proofs and how many are nonsense. If we see that they are nonsense, then OpenAI has wasted a huge amount of effort in mathematics. Famously the ABC conjecture proof of 500 pages is still unaccepted despite having been written in 2012.
Already people are seeing that the lean proofs provided don’t match the paper and lean proofs have not been provided for all paper proofs.
Already people are seeing that the lean proofs provided don’t match the paper and lean proofs have not been provided for all paper proofs.