Sure, we are likely to see soundness bugs in the current lean kernel again. And in other proof assistants too. Regarding the correctness of proofs this is not the biggest worry, in my opinion, though. Both sides of attempting to get faulty proofs in and of strengthening the kernel to keep them out have AI on their side. If AI advances more and becomes smarter it can be used on both sides. And the defending side has the easier task here. I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
The bigger worry are question that Terrence Tao is also talking about. I.e., is the proven theorem actually the theorem we are interested in? Are basic definitions of the field stated correctly? That kind of question. There is also still parts of proof assistants that are not the kernel and that can be abused. E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added. If I remember correctly I saw an example of the latter thing in the Coq (now Rocq) theorem prover many years ago. I forgot how it precisely went or where I read that.
The bigger worry are question that Terrence Tao is also talking about. I.e., is the proven theorem actually the theorem we are interested in? Are basic definitions of the field stated correctly? That kind of question. There is also still parts of proof assistants that are not the kernel and that can be abused. E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added. If I remember correctly I saw an example of the latter thing in the Coq (now Rocq) theorem prover many years ago. I forgot how it precisely went or where I read that.