The proof OpenAi presented allegedly reads like written by someone in acid.
It will take probably a while before we will get a translation into something that than will actually have a positive impact.
That could be either a second proof or a streamlined version of the AI one.
You even notice that with the recent opus and fable models by Anthropic.
If you give them a wide open problem statement, they'll start talking a lot of semi intelligible gibberish.
My guess is that this happens because that's not what they are evaluated on anymore for these kinds of tasks. The generated code is evaluated (in this case the lean code). So talking a bit of gibberish in the language part so you have more test time compute is not punished.