How To (really) Trust A Mathematical Proof
sciencenews.org
sciencenews.org
http://quod.lib.umich.edu/cache/a/a/t/aat3201.0001.001/00000...
Look at the last line of 54:43. Then look at the page number. This isn't a joke. It's really how bad axiomatic mathematics is.
During my last year of high school and first year of college, I was fascinated by this stuff to the point that I couldn't think about anything else. After digesting Peano arithmetic, I moved on to Zermelo-Frenkel set theory (the "set theory" that we normally use is self-contradictory and therefore meaningless to a mathematician.) I worked through Godel's incompleteness theorem. I tried my best to understand non-Euclidean geometries. And a bunch of other stuff that I don't even care to remember now.
Soon, predictably, it started affecting my health. At that point, I broke down and gave up that shit for good. The stuff I do today is positively quotidian by comparison. But it makes me happy. Even now, I'm occasionally uneasy about living in a universe where we don't know (actually, can't know) if the continuum hypothesis is true or false. But I shove the thought quickly from my head.
The point of all this is to tell you guys that unless you really know what you're getting into, don't think too deeply about the meaning of proof :-)
(One of the points made in Reflections on Relativity ( http://www.mathpages.com/rr/rrtoc.htm ) is that both a continuous universe and a discrete universe, taking the traditional senses of the term, are logically contradictory things to build a universe out of, and Einsteinian relativity calls for an odd mixture of both. No clean link to a single page as, IIRC, the point is made over a series of sections, culminating in a unique (AFAIK) discussion of Zeno's Paradoxes, which I can link to: http://www.mathpages.com/rr/s3-07/3-07.htm although you really need to read the sections before that for full impact.)
So, sleep easy. It is nothing more and nothing less than a choice of axiom. The axiom of choice is similarly irrelevant in the real universe; since use of the axiom calls for the selection of an infinite set from another infinite set, possibly uncountable, it has no particular connection to the real, finite universe.
In general, it appears that our ability to ask philosophical questions, especially of the mathematical variety, far outpaces our ability to find answers or even comprehend answers that others have come up with. It is highly plausible that this is linked to the disturbingly high occurrence of depression, bordering on mental illness, among mathematicians. (I know enough mathematicians personally for that observation to have some statistical validity, but anyone who has read many biographies of mathematicians should get the sense of it.)
What I'm trying to say is that while many of the questions of mathematical philosophy pique our curiosity greatly, and it can certainly be a rewarding experience to get a taste of the beauty of the field, everyone should have a mental threshold for how much they are willing to get involved. Perhaps this is obvious to other people, but since it was a painful lesson for me, I feel obliged to share it :-)
Set theorists, by the way, seem to be the most likely to go insane.
While Cantor did take his work seriously and was said to have believed that he was indeed doing God's work, he was probably bipolar. Given the attitude toward mental health at the time, it seems that whether he was a mathematician, merchant, or mason, he would have become "mad."
While Cantor is the classic example of a mathematician gone insane, there was also a number of things besides grappling with concepts of infinity that could have also have been a factor, like always being passed over for professorships and many prominent mathematicians (like Henri Poincare) trying to keep his work out of the canon of mathematics.
It seemed more like a work in showing the use of symbolic logic, rather than a proof of math.
-G.H.Hardy
I loathe these automatic proof systems (at least the state of the art today) - I think they may be useful for verifying that a complex CPU correctly implements integer arithmetic - but these proofs have little to offer a human mathematician. Let's follow Paul Erdos who said "one need not believe in god, but a mathematician should believe in The Book" The Book is where god (the supreme fascist) has collected the shortest and most elegant proofs in mathematics. Here's a great book written in this spirit (dedicated to Erdos) -
http://books.google.com/books?id=KvQr9l0wgf8C
when a theorem prover can produce a proof as elegant as as the one given in this book of say sperner's lemma then I'll give them another look. (No disrespect to Russell or the creators of these programs is intended, of course)
Lots of proofs are irreducibly ugly, even when the idea behind them is simple. Just too many edge cases and details. Automatic proof systems can avoid this.
I think of it much like garbage collection and higher order functions. The machine code of a garbage collected program might be messier than a manually managed one. But python code is prettier than c code.
but think about the following two situations: (1) you have serious doubt as to whether a statement is true. presenting a proof removes all doubt. Computer proofs, no matter how ugly, are a win for this situation (2) you have overwhelming experimental evidence that something is true and you want a mathematical proof to help you understand why it is true. Computerized proofs are less helpful here - this is where you want an elegant and simple proof. it should be very intuitive how the result depends on the assumptions. it should be something you'll be able to remember when you're 70 years old.
My guess is that we will instead have proof assistants. Basically, what will happen is that a human will come up with the big idea which motivates the proof, and will direct the proof assistant through the details.
I'm thinking something along the lines of Isabelle or Coq + ProofGeneral, except of course much better.
A person assisted by a computer can play better chess than any human, and also better than any computer.
Maybe it will be the same here.
In fact it happens in much the same fashion as you described. It's like writing a python port of a C program. You can abstract out the details until you have essentially reduced the proof to a chain of concepts.
In mathematics, proofs really have two purposes. The foremost purpose is obviously to assert the logical necessity of the statement being proven. The second not so widely publicized purpose is to gain insight into mathematics. A proof is not just a way to prove that you are right. It is also a way to see what could be further explored. Thus the importance of elegance and insight in proofs.
Automatic proof systems are great for the first purpose but they detract from the second. That is why they should not be considered the begin-all-end-all for mathematics. That is not to say that they are not useful or not an advancement. They are certainly that. Just that they are not a replacement for elegance.
That explains a lot ....
Too bad no one told me that back when it mattered.
- Couldn't track the source. Shucks.
Computer proofs have their value, but so far it is mostly in determining whether a proposition is true or false. One still needs a mathematician-written proof to get insight into the problem. This is unlikely to go away anytime soon.
Furthermore, for most important unsettled problems in maths, we already have a very strong inkling that the statement will turn out true/false. Dramatic surprises in maths are very, very rare. Gödel's incompleteness theorem is the only one that comes to mind.