Slashdot Mirror
Are Computers Ready to Create Mathematical Proofs?
DoraLives writes "Interesting article in the New York Times regarding the quandary mathematicians are now finding themselves in. In a lovely irony reminiscent of the torture, in days of yore, that students were put through when it came to using, or not using, newfangled calculators in class, the Big Guys are now wrestling with a very similar issue regarding computers: 'Can we trust the darned things?' 'Can we know what we know?' Fascinating stuff."
> 'Can we know what we know?' Fascinating stuff.
Reminds me of Rumsfeld... "Reports that say that something hasn't happened are always interesting to me, because as we know, there are known knowns; there are things we know we know. We also know there are known unknowns; that is to say we know there are some things we do not know. But there are also unknown unknowns -- the ones we don't know we don't know."
The headline does a slight disservice in describing the article that way: Whether or not computers can create proofs isn't an issue. The problem comes when the resulting proof is too involved to be verified by a human, and so the computer's work has to be trusted.
and there are already programs out that help with this. Here's one for example...
It's not hard to *see*. It's hard to *prove*. Very little of mathematics is consumed with proving deep, mystical statements that no one would ever anticipate to be true. Much (maybe most) of mathematics is built around proving (relatively) obvious things. Why bother? because sometimes, relatively obvious things turn out to be false, and there's no way to know that they won't until you've prooved them true. In general, showing that discrete (or semi-discrete) phenomena are optimal is fairly tricky; you can't just appeal to calculus to optimize some function. You often have to somehow break the search space up into a bunch of disjunct cases that span all the possibilities, and be able to prove that they span all possibilities. Then, if you're lucky, you can use some kind of calculus-type argument on the continuous spaces you're left with.
20th century mathematics has seen some pretty amazing things, but at the same time, there are very real questions as to what constitutes "proof" any more.
consider this: the hypothesis of the famous Riemann Zeta problem has been tested for trillions of different solutions, and it has held true in every case. (If you want an explanation of the Zeta problem, look elsewhere, I don't have the time)
Now that means that it's *probably* true, but nobody accepts that as mathematical proof.
On the other hand, the classification problem for finite simple groups has been rigorously solved, but the collected proof (done in bits by hundreds of mathematicians working over 30 years) is tens of thousands of pages in many different journals. given the standards of review, it is a virtual certainty that there is an error somewhere in there that hasn't been found. So, again, the solution to this problem is *probably* right, but it has been accepted as solved.
What's the difference between these two cases really? What's the difference between these and relying on computer proofs that are, again, *probably* right?
In this light, the math of the late 19th century and early 20th century was something of a golden age, modern standards of logical rigor were in place, but the big breakthroughs were still using elementary enough techniques that the proofs could be written in only a few pages, and the majority of mathematically literate readers could be expected to follow along. These days proofs run in the hundreds of pages and only a handful of hyper-specialized readers can be expected to understand, much less review them.
In Capitalist America, bank robs you!
Automated theorem provers have been around for a long time, if you can express your thoughts using first order logic. Here's a program from 1986... lisp code
as a graduate in the fields of mathematics, i spent a large portion of my five undergraduate years doing proofs. there are a great many ways to prove things, sometimes applicable sometimes not. (e.g. using inductive proofs for numeric theorems is all well and good but completely useless for any sort of ring-theory or spatial proofs)
there are also several levels of depth for proofs, ranging from "i've found a counter example so i can write the whole thing off as garbage" to "i have exhaustively and rigorously proved this starting with the basic axioms of number theory and worked my way on up"
the latter is really the only acceptable way to prove anything seriously. sometimes when you are reworking an already- done proof to illustrate a point, other mathematicians will allow a bit of latitude when it comes to cutting corners, but for a proof as far-reaching as the one in the article, i would only be interested in a "rigorous" proof, that is, one that started with the foundational tenets of mathematics and combined those to form and prove other postulates, etc. very much a form of abstraction, not unlike large development projects.
the problem arises when one (or several) humans have to be able to objectively check the whole thing. to use my prior example of a large development project, no one developer at microsoft understand the whole of windows. it's too big for a single human to understand. each developer knows what he needs to do to complete his part, and so on and so forth.
traditionally, for proofs, a single mathematician (or a small group) would hammer out the whole proof, so the level of complexity remained at a human-understandable level. (even if tedious) my concern, as a mathematician, with using an automated solution would be the rapidly growing order of complexity needed to properly back up increasingly complex proofs. as stated in the article, it's like trying to proofread a phonebook. (only, you must also consider that for every element of the proof (a particular listing) there are several branching layers of complexity (fundamental, underlying proofs many layers deep) underneath. this gets more complicated in an exponential fashion) obviously this approach will only remain human-checkable for relatively small problems. (programmers: think of some horrible nondeterministic- polynomial problem like the "traveling salesman" problem. systems, like humans, are a finite resource, but if you increase the size of the problem, the complexity will quickly grow far beyond your ability to compute. large proofs suffer from the same difficulties, if not quite as concrete and pronounced as NP algorithms)
in closing, i would have to agree that proofs, no matter the effort and computing time put into them, really should not be viewed as being as rigorous as those provable "by hand" and human- understandable, even if the computer has arrived at a satisfactory conclusion, because we have no way of KNOWING if the computer has built up the proof correctly, except that it says it has.
In Soviet Russia jokes are formulaic and decidedly non-humorous.
once upon a time, only advanced mathematicians knew calculus, but now we learn it in high school. Just wait until warp theory is an entry level college engineering course
Once upon a time, the majority of adult males knew how to trap a rabbit (or similar creature), gut it, skin it, start up a fire, cook it, and eat it.
I don't.
Heck, I couldn't even look up at the sky at night and tell you which way was north.
Once upon a time, most people could.
All I'm saying is that the amount of knowledge and skills the average human being can possess will not increase expontentially over time (barring artificial manipulation). We gain new skills as a population and lose old ones.
No! Definitely not! Really! :-)
Most faults are software problems, not hardware, so having different machines won't help. Further, interestingly, most major software faults (at least, of the sort that make it through serious testing) tend to be conceptual problems, not coding ones, and different people tend to make the same mistakes. This means in practice that even when you have completely independent software implementations (called n-version programming), they're frequently all wrong in the same way at the same times. See the famous Knight & Leveson paper.