It solved the navier stokes millennium prize problem without any reasoning? I could maybe believe it if it was just something like deep blue searching in axiom space with lean with some simple heuristics, but in this case the formalization came after as a separate step.