Surprises in Mathematics and Theory

For the High Crime of the Heresy of Doubt against the Mathematics, I do hereby Sentence 10ren to a reading of the Principia Mathematica until such time as he reads the Proof of 1 + 1 = 2.

Which, according to the great Wikipedia (against which no Doubt is permitted either), occurs first in Volume 2, page 86, which comes after the nearly 700 page Volume 1, which does mention the Issue on page 379 of volume one but quickly moves on to more Important Things.

...

Anyhow, I'm not merely being sarcastic, although I couldn't resist the above. My point is rather that this is a deep question that mathematics has pondered itself, and learning about the history of the Principia Mathematica and the early 20th century of mathematics in general can be very interesting. How modern mathematicians see it, I don't know, I'm just saying the history is also very interesting.

Yes this is a problem. Worry about whether or not I've proved something is strongly related to by understanding of the solution.

If the proof is ad-hoc, and cannot be related to existing theory then I am concerned. If I can rephrase my results in terms of existing accepted theory this both makes the work easier to understand, and "more likely" to be correct.

I think the 'Incompleteness Theorem'

http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_t...

might address what you're describing.

First, Coq isn't an automatic theorem prover, it's a proof assistant. Adequacy is an issue, but (particularly) for computer-science applications it's sometimes possible to use the Coq artifact as the implementation directly. Adam Chilpala's recent work has made some pretty impressive advances in verifying working code.

I think you misunderstand, though: there's no obsession with absolute truth, at least not in the mathematical world I live in. I'm a PL researcher; we don't pretend to absolute truth, but formality and correctness are our cardinal virtues. (Take Coq as an apropos example.) Our proofs are (a) by induction, (b) long, and (c) can involve subtle and fussy steps. And (d), in an ideal our world, our proofs are also the bedrock of high-assurance systems. Proofs with different qualities may be better candidates for a more intuitive approach. In particular, actual mathematicians are probably more interested in the intuitive side of proof than we are. The article is in fact interested in that more intuitive mathematics; Lipton points out that this intuitive mathematics---whether as formal as 4CT or as informal as the vision conjecture he describes---is full of fun surprises. I'm not sure he's worried about the sort of nitpicking formality that I'm into. :)