> At present, some frontier AI labs are testing advanced mathematical problems on proprietary models that remain inaccessible to the broader scientific community. Our recommendations are formulated with this practical context in mind.

The Navier Stokes proof came from an internal model that AFAIK still has not been released even in a limited way to scientists, let alone to the general public. Publicly available models are not what these mathematicians are talking about.