I don't think that's actually the real problem. Along with the progress in answering mathematical questions, recent progress on AI-powered autoformalisation has been astonishing. All the recent AI discoveries have been accompanied by Lean proofs.

And, yes: that doesn't absolutely guarantee correctness. The Lean kernel has had soundness bugs, and may have some still. But it's pretty strong evidence of correctness nevertheless.

The concern among mathematicians is not mainly that they doubt the correctness of any of these discoveries, but that human understanding may be devalued.