On: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

[TZubiri]

But can you verify them? With less effort?

[dooglius → TZubiri]

I'm not sure what you mean by "verify" here. I could run the lean verifier as could anyone else. Maybe I could write my own proof checker and do a purely mechanical translation into my own thing, though I don't think that's less effort.