Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.
How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”
Anthropic sent out its Fermat's Last Theorem result to an expert on formalizing Fermat's Last Theorem in Lean, for what that's worth.