Of course I don't quite agree with the content of Opinion 51, but I can appreciate the reasoning; personally, I still find some value in the fact that I know a quick reason for the fact that 8765432187654321876543218765432187654321 is composite, and I will be less satisfied with a computer telling me that's the case.
Moreover, a proof of 4CT without computers will not change my conviction in the obvious fact that computers enable us to do lots of mathematics we cannot do without them. Hoping people will not find such a proof is essentially like hoping that people will not find a short argument for that question that someone asked John von Neumann, that can be solved either by computing an infinite sum (as von Neumann did quickly) or by multiplying the time by the speed. If we do not find the latter, shorter proof, that can serve as an evidence that we need a pencil and paper to do mathematics; do we really need evidence for that ? I don't.
I would like to oppose the opinion you stated in OPINION #51. 1) computers are the results of human efforts and human technology and as such they offer nothing deeper from the human thought that created them or that programmed them. It is just another way to do mathematics, where part of the classical reasoning and computing is replaced by a machine who was programmed by human to overcome our limited power to compute. I am far from accepting the idea that the power of computing make the difference between shallow and deep. There must be a much deeper criterion to make the distinction. 2) you use the word shallow in an absolute form namely everything we, human , can do is shallow. This means that except of things created by God or external power everything is shallow. This paradigm ( a sort of theology ) put everything that was proved in mathematics on the same level of shallowness : everything is shallow. Isn't it the case that FLT has degree 9 ( say) in shallowness scale now and sqrt(2) is irrational has degree 3 ( say ) on the shallowness scale ?? 3) that the computer can do things we can't do , needs no proof, it is obvious. In fact there are several computations, which are trivial from the mathematical point of view that are provably ( on the basis that we live 100 years X our ability to compute a multiplication of two digits in 1 second ) not within the human capability, but very easy for the computer power . I guess a reasonable example would be to compute exactly 10377! . So the fact that the computer can do something we can't and will never be able to is certainly not a certificate to be called "deep". 4) It is quite common in mathematics to have several proofs to the same theorem. The benefit is that we learn more about the issue in question by seeing various lines of attacking it and various reasoning that leads to a proof . A proof using computer and one that doesn't are of interest if they suggest alternative or new ideas. In my view Ideas are what make things deeper or leave them on the surface- shallow. By the way 4CT is in retrospect , in my view, less deeper than FLT just because it is easy to understand the reduction ( as you said) and the rest is a routine checking, and a routine checking is by no means deep. So if we can't find a human proof will not make this 4CT deeper than it is now, it will only supply another proof that we are limited in our computational power with respect to computers and that we were very wise to notice that and to invent computers to help us in our weakness. 5) Time has a role : I am sure when Euclid first proved the infinitude of primes that was a brilliant and deep idea ( still very nice today ). However as we make progress older results become less surprising and more understandable, and when we are less surprised we sometime might say "shallow". The same will be the fate of proofs by computers as the power of computation will evolve. Evolution ( and time) moves the "deep and surprising" step by step into the "shallow and obvious" relatively to the new generation of thoughts, ideas and results. 6) The question whether the program that used by the computer belongs to the computer or to the programmer reminds me the same situation in the post modernistic debate if an article ( or paper, or book ) belongs to it writer or to the reader . While I am not sure about the philosophic attitude to this question it seems to me clear that if the program "belongs" to the programmer than "shallow" goes on to the results of computer finding. 7) I still prefer a more moderate and sensitive scale to be applied on ranking mathematics and proofs ( including FLT ) rather then say it is shallow because it was proved by a man. Saying everything shallow leaves room for no other fine scale, and no way to make distinction between : the sum of degrees in a graph is an even number ( elementary ) and FLT ( far from elementary ).