If I understood that paper right, what it claims isn't quite the bombshell that it initially looks like. (Though it is still startling.)

I think they are saying: when OpenAI put out their paper purporting to prove that Navier-Stokes with smooth forcing can blow up, along with something purporting to be a Lean formalization of that paper, (1) the Lean formalization really is a proof that Navier-Stokes with smooth forcing can blow up (so they genuinely did prove the thing that the Clay Institute wanted them to prove), but (2) the Lean formalization doesn't perfectly match the paper. I think the jury is still out on whether the paper itself is also a valid proof of the result, even if not quite the same proof as is in their Lean formalization.

I'm a bit surprised that the workflow for AI theorem-proving hasn't turned out to be a sort of interleaving of natural-language theorem proving and Lean formalization. That seems like it could work better and leave less room for this sort of gap between "kinda human-comprehensible writeup, may or may not actually be a proof" and "incomprehensible Lean formalization, definitely a proof of something, may or may not have much to do with the natural-language writeup". Instead, what seems to happen is that they set the robots loose on writing a natural-language proof, and then (sometimes) also get them to produce a Lean formalization of what they've done.