Computer Assisted Proofs- still controversial?

Kenneth Appel, of Appel-Haken Four Color Theorem Fame, died recently. See here for an obit.

In 1972 I read that the four-color theorem was an open problem. From what I read it seemed like there was some progress on it (e.g., results like `if its false the graph has to be yah-big) but it seemed to be years away from being solved. I assumed that a new idea was needed to solve it.

Then, in 1976, it was SOLVED by Appel-Haken. From what I read it wasn't so much a new idea but very clever use of old ideas and a computer program. I also heard that it was just at the brink of what computers could do at the time, and that it would have taken 1200 grad student hours. (There is a good description of the proof on Wikipedia here.)

At the time I heard there were objections to the proof. Later when I read some of them they didn't seem like real objections. They boiled down to either

I wish there was a shorter proof. This is true, but not a reason to object.

It can't be hand checked. I trust a computer-checker MORE THAN a human checker

We don't know WHY its true. This is a more reasonable objection- but we do know how they got it down to a finite number of cases, so I'm happy with that.

In 1996 Robertson, Sanders, Seymour, Thomas was obtained a simpler proof. In 2005 Werner and Gontheir formalized the proof inside Coq- a proof assistant. To quote Wikipedia This removed the need to trust the various computer programs used to verify particular cases;it is only necessary to trust the Coq Kernel At this point I doubt anyone seriously doubts that the theorem has been proven.

There have been more computer-assisted proofs since then. See here for a list of some of them. That article also claims that such proofs are controversial and not always accepted. Is this really true? I thought the controversy was gone except for the topic of the next paragraph.

A famous computer assisted proof (or perhaps ``proof'') is the Kepler Conjecture. In 1998 Thomas Hale claims to have proven it. The proof involved rather complex computer calculations. The referees say they are 99% sure its true. Here's hoping an easier proof is found.

Computer assisted proofs may become more common. I just hope we still know WHY things are true.

Was Appel-Haken the first use of computer assisted proofs? I doubt it, but it was likely the first one to have an impact. It was important to know that this kind of proof could be done.

Is there a much shorter proof? A combinatorist once told me that since the function

f(n) = max size of proofs of statements of length n

grows faster than any computable functions, there have to be some statements that have very log proofs; and perhaps the four color theorem is one of them.