To bluntly put it in a nutshell, and state the obvious:

If you don’t understand the problem you can’t be sure that the computer does.

As a programmer I definitely get annoyed when I see code and I don't understand what it does.

But I also definitely don't understand the problem if I can't get the computer to understand it, with tests.

In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.

With all of these questions in the air, epistemology might be making a comeback.

Well, if you can formalise the problem statement (this is the hard part) sufficiently well that the computer can produce a proof, you can be very sure the proof is sound.

A fundamental property of any formal proof is that it can be checked by a fairly stupid machine, automatically, because every step is a simple mechanical operation that names one of a handful of axioms and refers to a handful of earlier steps, the truth of which has already been established. So while coming up with a proof may require genius-level thinking, checking an existing fully fleshed out proof is simple -- just potentially very tedious because of the sheer number of steps.

That said, a typical human-written proof omits many steps considered "obvious" to a trained mathematician. Converting this to a formal proof involves interpreting what the original author "must have meant", which requires a lot of expertise and can go wrong -- or it may reveal that there is some inconsistency in the original claim itself.

Almost another layer in the peer review process in the best case right? Just a different kind of peer you have to review.

lean compiles or it doesnt