Running a proof assistant as a user and focusing on a given formal proof, how can one assert that there are no unexpected errors or "bugs" that could invalidate the provided proof?
More specifically, if the considered formal proof says a given theorem (e.g., about prime numbers) holds, what guarantees could users have to be sure that everything (from the definition of prime numbers to the statement of the theorem to its "truth" itself) is correct?
One is always going to sit between two extremes. On one extreme we can't be 100% fully certain of anything. For example, we might be living in a computer simulation, or it might be that every axiom system we have ever dealt with (Peano Arithmetic, ZFC, DTT) are all inconsistent.
On the other extreme, a lot of thought and care has gone into building proof assistants and it would be reckless to say they obviously have fatal bugs just because they are software, or they are obviously no better than any other ad-hoc computer checked proof such as the original four color theorem proof.
The middle ground is that proof assistants are unparalleled in their attention to robust guarantees but they also try to be practical systems, and bugs do sometimes creep in. More and more work has goes into making bugs less likely.
There is a phrase in this field called trusted computing base meaning basically all the components you have to trust to trust your end result. This includes the software as well as the hardware.
The main line of defense in a proof assistant is a small kernel. While a proof assistants may provide a great deal of automation and user tools, those tools just construct (and communicate) the proof. The kernel is the part that actually checks the proof. HOL-Light famously has one of the smallest kernels at just about 400 lines of OCaml code. DTT kernels in say Lean and Coq are usually larger since the logic is more complicated, but even Lean's kernel for example tries to stay small and be very robustly checked.
Another advantage of a kernel is that if one day a bug is found (there were two bugs found in say the HOL Light kernel over time) then all proofs can be rechecked with the fixed kernel. This still requires that the proof hasn't bit rotted, etc, but it does provide a way to quickly recover from errors.
Also, the kernel can export the proof. Then the proof can be checked in another implementation of the kernel. Lean for example has a number of external checkers which reimplement Lean's kernel. If I understand correctly, they are regularly run over the exported term proofs of Lean's main mathematical library mathlib. Also, it is possible (although I don't know it is done in practice) to check Lean's term proofs in Coq. Similarly, I think there are other similar tools for many of the other proof assistants. These tools don't guarantee that the full implementation of the logic is correct, but just that the current proofs follow the logic as implemented in all the checkers. This significantly reduces the possibility of a bug due to an error in implementing the logic.
As for the logics themselves, it is advisable to use standard logics which are well understood. While it can be nice to add new features, they run the risk of introducing inconsistencies. HOL-Light has actually formally verified that their logic is consistent. (They avoid Gödel's incompleteness theorem by verifying Con(HOL - Infinity) in HOL, and Con(HOL) in Con(HOL + large cardinals) or something like that.) Mario Carnerio's thesis gives a pen and paper proof of Lean's consistency including all the implementation features.
Other provers go further and try to verify the actual code implementing the prover. I don't know a lot about this, but CakeML and Coq in Coq are projects along this line.
A new project is Mario Carneiro's Metamath Zero which plans to be an external checker for all logics which has a formally verified implementation done to the x86 byte code. Further, Mario has done a lot of thinking about what parts still need to be human inspected such as the axioms of the logic and the statements of the theorems and definitions used in the final result. (The statements of the lemmas and intermediate definitions don't matter to correctness if you trust the kernel.)
On a practical side, a major source of errors in math proofs is just missing cases, or thinking something is obvious when it isn't. Proof assistants force you to deal with those explicitly. This is even more an issue when verifying hardware and software since a proof of correctness of say an implementation of floating point arithmetic doesn't have the beauty of the proof of say FLT. While the latter is much more complicated, it is also built on a number of beautiful mathematical ideas. Whereas, forgetting one value in a table could make it so that your algorithm implementing floating point numbers is wrong. Therefore, proof assistants provide a larger value add for software and hardware verification than mathematical theorems.
Even if a kernel as a bug, to get a wrong result you usually have to be meticulously exploit that bug. This may involve invoking logical inconstancies like in Russel's paradox, or carefully abusing variables in an unnatural way. (Or it may even require you to exploit the programming language used under the kernel.) As such, it is unlikely that a proof written by a competent and trustworthy human would succumb to those bugs. Nonetheless, as automation and AI becomes more common in theorem proving, maybe it is more likely that an AI just trained to find proofs could learn to exploit a bug. Similarly, imagine if one is paying someone over the Internet to prove theorems for you. Can you really trust that they have the integrity to not exploit a bug? (Similarly for theorem proving competitions?) Last, what if someone no one has ever heard of claims to have a formal proof of the Reimann Hypothesis in Coq? I would strongly imagine that the Clay Foundation would put a lot of work into understanding the proof and ways to double check it rather than just except Coq's output. So the motivation and trustworthiness of the user, as well as the importance of the result, probably matters here as well.
Last, as a user you have to know how to use the system correctly. All these systems have back doors where you can use sorry, CHEAT_TAC, etc to temporarily fill in a hole of the proof. You have to know how to look for those in the end. (And sometimes they are not named what you think they are. Lean has a few synonyms for sorry.) Also, theorem provers usually provide the ability to add custom axioms, so you have to check which axioms are used in the proof. Even in Lean if you don't see any red squiggles, it could be because of an axiom, or even just that the Lean front end crashed.
Similarly, sometimes definitions don't behave as you think. An obvious example is that in many systems 1 / 0 = 0 for practical reasons. So your should understand the definitions you are working with (especially at edge cases).
Also, as a user you have to pick a system which a lot of quality work has gone into. Some proof assistants are just playgrounds for ideas and have known logical inconsistencies like Type : Type. This is fine if you know how to avoid this, but take it into account. Whereas Lean, Isabelle, Coq, Metamath, Mizar, HOL-Light and many others have put a lot more work into making everything as air tight as they can.
So to summarize, if you know how to use the system, I wouldn't worry too much practically. Nonetheless, this is still an ongoing area of research, especially if you want to make your system robust against adversarial exploitation (or against skeptics who don't trust anything).
This question is both complex (because it amounts to considering many "layers of trust") and paramount (because trust and correctness play a very important role in the domain of Proof Assistants).
First, whatever is the considered proof assistant, it is endowed with a logical system (typically, tightly related to a given type theory). So, before dealing with the proof-assistant software part anyhow, the question just amounts to know whether:
Let us now assume that we trust the chosen logic.
Addressing item 2. can then be viewed as a typical use case for proof assistants. To refine this item, we can follow the approach outlined by Pollack in this paper:
Namely, once the result has been formalized, accepting the formalized result as "correct" can be split into two sub-problems:
Note that this two-step approach fully matches the concept of V & V, in systems engineering and formal methods, that is, asking:
Furthermore, in the context of proof assistants, we can refine these two steps as follows:
The question of item 3. can be answered by a machine (using a proof checker, which is generally a sub-component of the proof assistant, but can just as well be a separate, independent software project). To trust its outcome, we "just" need to trust the hardware, the operating system… and the proof checker software implementation (I will not elaborate on these problems; but each of them is a research problem by itself).
Still, trusting this tool may sound "easier" than believing the (possibly very long) pen-and-paper proofs, because:
the proof checker needs not "discover" the proofs, it only needs to check them;
for proof assistant satisfying the so-called "De Bruijn's criterion", as they have a reasonably-small proof-checking kernel, their TCB (Trusted Computing Base) will be equally smaller; see also this handbook where this term "De Bruijn's criterion" was introduced:
Note anyway that the computational capabilities of the proof assistant, that make it possible to "discharge some proofs by a mere computation", do belong to this TCB.
The question of item 4. is mostly an informal question, which thus requires some human-directed review; but this step is definitely well-surveyable, because:
Finally, note that some technical impediments may also creep in this latter validation process, especially regarding the parsing and the pretty-printing of the formal statement of the theorem. A formal study of this problem (surveying several proof assistants on this topic) can be found in this paper:
