Comment by balaclava9

They are claiming that we do not know if Astra formalized all the elements of the Navier-Stokes proof in Lean correctly.

The Clay Mathematics Institute has not yet accepted the proof.