You only need the problem statement to be correct in Lean, no matter what route it goes down is correct as long as the original formalization of the problem is correct, which is substantially easier to check. Not sure how many people have checked that so far, but I'm guessing the math community would be quick to point out if something basic like that was missed for something like a new bound on RH.

Nothing wrong with being skeptical, but I see no reason to be skeptical as of yet.

There's nothing to check there, they used the standard mathlib implementation of RH. THey didn't write their own for the 7/8ths proof.

Were days out, the default should probably be skepticism for about a decade.