The controversy surrounding automated theorem proving and verifying is more or less dead at this point. The hardware in the computer that you’re using to read this was almost certainly proved to meet its specifications by means of a computer.
I’ve always found that proof rather unsatisfying, though. It’s such an intuitive theorem that there really ought to ba simple proof.
I’ve said this before.
Sigghhhhh…he was such a colorful man…and well traveled too as he had been to the four corners of the Earth many many times.
I’ll probably be lost 2 sentence into the answer to this but can someone explain how this theorem worked.
My laymans guess is that at first glance the problem has an infinite number of permutations, therefore the best you could do with a computer is just keep cranking out solutions and the more you crank out the more sure you are its true but it is still not proof.
So, my next hunch is that they used some fancy math I don’t understand to reduce that infinite set to a very large but finite set and then set the computer to work to check out that finite set.
Correct.
I like Cecil Adams’ comment on the proof, “There are those who complain that this process does not constitute a mathematical proof, as that term is usually understood, but rather falls more into the category of an experiment, understandably something of a novelty in the field of abstract mathematics.”
Okay, now time to get my head hurting.
How did they “convert” an infinite set into a large but finite one?
And as an aside, did proving the Four color theorem help to prove others?
Also I amazed at how “easy” some problems that seem hard are solved and vicesa versa.
Experiments are not exhaustive. (I almost typed Cecil was wrong, but my keyboard shocked me into realizing that Cecil just said that some people say that. Whoo.)
I was at Illinois during this time, and I got to see them talk about the proof - for a more general audience. (Of professors and grad students, so not that general.) The Times obit mentioned the IBM mainframe, but I understand that Andy also used the Cyber from CDC that ran PLATO for some of the work. He was in high school at the time.
I had Andy and Haken’s daughter Dorothea in my Assembly language class. He was a freshman, and got the second highest grades (after her.) They were both so smart that I can just imagine how smart their parents were. Her 12 year old brother also write a symphony, I believe. Enough to make you humble
Well, as a very simple example, the infinite set of integers can be broken down into a set of two: odd numbers and even numbers.
I assume that they figured out that each of the infinite set of maps fitted into one of a finite number of types of map, which they could then test for.
Yikes, I didn’t realize he was that old. He and Haken were both still active at the U of I when I was there in 1989-91.