Apart from an irrelevant appeal to the left wing political sentiments common among mathematicians, Devlin has expressed a point of view about proofs held by quite a few mathematicians and even more prevalent among philosophers of mathematics. The main pioneer of this view was Imre Lakatos in his book _Proofs and Refutations_. The book concerned proofs of Euler's formula E + 2 = F + V for the number of edges, faces and vertices of a plane polygon. My opinion is that Euler's proof was correct though informal. I suppose my own view would be characterized by Devlin as even more right wing than any he mentions. My solution to the difficulty of verifying very long and complicated proofs is to check them with an interactive computer prover and verifier. If computer programs are used to check some of the conjectures, then these programs need computer verified proofs that they meet their specifications. However, the state of the art of interactive theorem proving needs great improvement before it is practical for hard theorems. It seems to me that no great theoretical advance is needed, just a lot of hard work. I'm not well acquainted with the state of the art, but one landmark for me was Shankar's proof of the first Gödel incompleteness theorem using the Boyer-Moore interactive prover ACL2. One of their students gave a 50 step verified proof that a checkerboard with two diagonally opposite corner squares removed cannot be covered by dominoes, each covering two adjacent squares. I gave a four step version of the usual informal proof using set theory. Alas, there is no verifier that can accept my proof. I conjecture that until there is such a verifier, interactive provers will not be used by mathematicians for difficult theorems. I used Jussi Ketonen's interactive prover EKL for first order logic in class, and the students used it successfully to prove easy theorems about Lisp functions. I did not have the energy or resources to carry the project further. I see the major step toward use of interactive provers in mathematics as being the creation of what I call heavy-duty set theory (HDST). ZFC, is normally axiomatized using a minimal set of axioms, because the main use of the formalization has been to prove metatheorems, e.g. the independence of the continuum hypothesis about ZFC rather than to prove theorems within ZFC. HDST should have a large number of theorems of ZFC as axioms and admit verification in a single steps inferences that are automatically verifiable. Once the prover itself has been proved correct and the proof verified, we can have confidence in proofs produced and verified interactively using it. Note that proving the prover correct is a single mathematical task, and it is unlikely to be anywhere near as onerous as checking candidate proofs of the twin primes conjecture. Proving correct the verifier, the compiler for the language in which the verifier is written, and the machine used are a small number of small tasks that can be done once.