The mention of the Russell-Whitehead proof brought back memories. It's from Principia Mathematica (same title as Newton's book, but it's a different work.) Here's a representative page:
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 :-)
In our actual, factual physical universe, the Continuum Hypothesis isn't so much "true" or "false" as "irrelevant". It's possible the universe is fundamentally discrete, in which case it just doesn't apply to anything physical, and even if it turns out to be continuous in some sense, it's likely to be some hybrid continuous/discrete combo where the hypothesis still doesn't apply to anything physical.
(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.
That makes sense, and it's likely that if I read through the entire book that you linked to, I'd grasp it pretty clearly. But it was certainly out of my mental reach as an 18-year old. And believe me, I tried.
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 :-)
Mathematical Platonism is dangerous for mental health. Cantor is a great example of someone who literally went crazy contemplating the meaning of uncountable infinites.
Set theorists, by the way, seem to be the most likely to go insane.
What are you basing this on? Mathematics may lead to highly surprising and nonintuitive answers, but that doesn't mean that mathematical ideas drive people crazy.
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.
"There is no permanent place for ugly mathematics"
-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) -
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.
you have strong point - i hadn't thought about it this way before. Just the other day someone called me out on a derivation and i spent a couple of hours writing out a very tedious proof. there were lots of special cases and i really resented the bastard when i was done. the experience was very much like filling out IRS forms. it would have been very nice to have a proof assistant to back up the points where i would have much preferred to handwave. I really like the comparison to manual memory management that's exactly what this proof felt like - freeing the mallocs.
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.
I actually suspect the second situation won't happen for a long time.
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.
Proofs are almost never "irreducibly ugly." What has generally happened in the past is that mathematicians have abstracted the "ugly" parts of a proof, so that one only has to refer to a mathematical object (object in the OO sense). Ugly proofs for basic theory are usually the primary motivation for mathematicians to invent new mathematical abstractions. In fact, when some mathematician is said to have "reinvented a field of mathematics," it usually means that he has found a particular abstraction or perspective that allows for a simplification of the given field.
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.
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.
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 :-)