Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results.
As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.
The Lean proof is published, you can download it. The clock definitely is ticking.
Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
> Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet.
A similar rule existed for the 100-year Wolfskehl prize established in 1906 for solving Fermat's last theorem; two years after publication.
It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough
I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.
Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.