When is it worth the time and effort to verify a proof FORMALLY?

(This post was inspired by Lance's tweet and later post on part of IP=PSPACE being formally verified.) 

We now have the means to verify that a proof (prob just some proofs)  is correct (one could quibble about verifying the verifier but we will not address that here). 

The Coq proof assistant (see here). This was used to verify the proof of the four-color theorem, see here.

The Lean Programming Language and Proof Verifier (see here). It has been used to verify Marton's Conjecture which had been proven by Gowers-Green-Tao (see here for a quanta article, and here for Terry Tao's blog post about it.) 

The HOL (Higher Order Logic)  is a family of interactive theorem proving systems (see here). The Wikipedia entry for HOL (proof assistant) (see here) says: 

The CakeML project developed a formally proven compiler for ML [ML is a programming language, not to be confused with Machine Learning.]

The ISABELLE is an HOL system. See here. The Wikipedia page says that it is used to verify hardware and software. It has recently been used to verify the Sumcheck Protocol which was developed to help prove IP=PSPACE (See here.)One of the authors of the IP=PSPACE paper, Lance Fortnow, said of this

Now I can sleep soundly at night.

The Kepler Conjecture was proven by Thomas Hales. (Alfred Hales is the co-author of the Hales-Jewitt. I do not know if Thomas and Alfred Hales are related, and Wikipedia does not discuss mathematicians blood-relatives, only their academic ancestors.)  The proof was... long. Over a period of many years it was verified by HOL light and Isabelle. See here. (Note- the paper itself says it used HOL-light and Isabelle, but the Wikipedia site on Lean says that Hales used Lean.) 

I am sure there are other proof assistants and other theorems verified by them and the ones above. 

My question is 

Which proofs should we be spending time and effort verifying? 

Random Thoughts

1) The time and effort is now much less than it used to be so perhaps the question is moot.

2) Proofs that were done with the help of a program (e.g., the four-color theorem) should be verified.

3) The theorem has to have a certain level of importance that is hard to define, but item 1 might make that a less compelling criteria. 

4) A proof in an area where there have been mistakes made before should be verified. That is the justification given in the paper about verifying part of the IP=PSPACE proof.

5) A rather complicated and long proof should be verified. That was the case for Marton's Conjecture. 

6) A cautionary note: Usually when a long and hard proof comes out, people try to find an easier proof. Once a theorem is proven (a) we know its true (hmmm..) and (b) we have some idea how the proof goes. Hence an easier proof may be possible. In some cases just a better write up and presentation is done which is also a good idea. I wonder if after having a verifier say YES people will stop bothering getting  easier proofs.

7) Sometimes the people involved with the original proof also were involved in the verification (Kepler Conjecture, Marton's Conjecture) and sometimes not (IP=PSPACE, 4-color theorem). 

8) When I teach my Ramsey Theory class I try to find easier proofs, or at least better write ups, of what is in the literature. I sometimes end up with well-written but WRONG proofs. The students, who are very good, act as my VERIFIER. This does not always work:  there are still some students who, 10  years ago, believed an  incorrect proof of the a-ary Canonical Ramsey Theorem, though they went on to live normal lives nonetheless. Would it be worth it for me to use a formal verifier? I would guess no, but again, see item (1). 

9) Might it one day be ROUTINE that BEFORE submitting an article you use a verifier? Will using a verifier be as easy as using LaTeX? 

10) The use of these tools for verifying code--- does that put a dent in the argument by Demillo-Lipton-Perlis (their paper is here, and I had two blog posts on it here and here) that verifying software is impossible?'

11) HOL stands for High Order Logic. I could not find out what Isabelle, Lean, or Coq stand for. I notice that they all use a Cap letter then small letters so perhaps they don't stand for anything.