Hacker News Reader

Comment by 10ren | Hacker News Reader

When I work on a proof, I worry about whether I've really proven it. How can I prove the proof? Yes, there are automatic theorem verifiers/provers (things like COQ), that guarantee correctness... provided you haven't introduced any other errors in the transcription, and the theorem verifier itself is perfectly bug-free...

It makes me think that an obsession with absolute truth is a misplaced priority, and perhaps a better view is that mathematics does not provide absolute proofs, but just a measure of certainty - like any other field, just much higher. And the real point of mathematics is something that you can sense is true, that is beautiful, and works correctly whenever you try it out.

I would be interested to know how any professional mathematicians here see it.

View on HN

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.

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. :)

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.

I think the 'Incompleteness Theorem'

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

might address what you're describing.

No, 10ren is merely talking about correctness within the given system.

Reply on news.ycombinator.com