But you can't do it with their internal model that is the same or a successor to the one that solved the navier stokes millenium prize problem.

With 40% formalized they probably have a good idea of how many were found to have fatal issues in the formalization attempt, and they hired some mathematicians to verify some of them, especially the big headline ones.