Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A Computer Scientist Tells Mathematicians How to Write Proofs

blogs.scientificamerican.com

Post reply on HN
Print view View original

51–60 of 103 posts

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#51

Post by qznc »

gone35 wrote: post #23
frankmcsherry wrote: post #8

Earlier quoted context omitted.

I was formerly in the same lab as Leslie. As a side project, we (Tom Rodeheffer, mainly) used TLA to verify the correctness of Naiad's coordination protocol. The protocol is very simple (distributed reference counting), and my initial "proof sketch" was about two paragraphs long (and very unconvincing, apparently :). Tom's TLA+ version was closing in on 200 pages, available at http://research.microsoft.com/pubs/18382…

Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to already-established proofs from some common repository? Maybe future versions of TLAPS would benefit from such a thing? (Sorry if this already exists; I'm just an interested layman.)

For the Isabelle theorem prover I know the Archive of Formal Proofs [0].

[0] http://afp.sourceforge.net/

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#52

Post by TylerJay »

taeric wrote: post #7
Tloewald wrote: post #4

Basically, do it the way Spivak does. Funny thing is in freshman year we were taught to do just that, but then abandoned the formality pretty much immediately after.

My understanding from the linked paper in another thread, is not to do it the way Spivak does. That is, the article says Lamport "walked us through a proof of a corollary to the mean value theorem from that textbook, pointing out statements that he felt were not precise or rigorous enough and rewriting the proof using his technique." My reading of that is that Lamport found faults in Spivak's approach. Did I missread…

No, you didn't misread it. You can see the example for yourself in the paper. It's Section 2 here:

http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#53

Post by mitko »

Pretty good read, but the OCD in me could avoid pointing out that the example they give has a wrong solution:

x2+10x=39. Find x2.

This actually has two solutions for x: 3 and -13, so x^2 is 9 or 169.

It is probably a good example of how referring to preconditions at every step of the proof would help catch errors. From my experience writing code, I'd also argue that this would also make proofs more beautiful, because discovering that some steps require a lot of previous references might prompt the mathematician to restructure/refactor the proof to make it simpler to write, thus making it simpler overall.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#54

Post by Enzolangellotti »

seanstickle wrote: post #50
Enzolangellotti wrote: post #43

Earlier quoted context omitted.

Care to share the title?

Principia Mathematica http://en.wikipedia.org/wiki/Principia_Mathematica

Ah, Russell. I've always been put off by people complaining about his somewhat pedantic approach. I guess I'll give it a try. Thank you.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#55

Post by navait »

_ikke_ wrote: post #32
threatofrain wrote: post #27

Earlier quoted context omitted.

I think the solution is probably to have it all, according to your taste: code because you can run it as a working proof, and explanations in both comments and prose.

How do you prevent discrapencies between those? You already see it with comments on source code, which eventually get outdated.

Hopefully, that won't be a problem with code written for a paper. You can freeze it then(for that version), unless errata is required.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#56

Post by tel »

madsravn wrote: post #34
ipsum2 wrote: post #16

Earlier quoted context omitted.

The article has nothing to do with Coq: > When I saw the title of the talk, I assumed Lamport would be talking about computer proof checking programs or even a proof creating program like the one Timothy Gowers has worked on and written about. But Lamport’s advice was much more down-to-earth.

I'm a referring the guys paper, which is linked here in the comments somewhere. There TLA+ is mentioned which is a tool to formally prove something. The same can be done in Coq - which is why I'm drawing a parallel.

While that parallel is genuine, it's hard to compare Coq and TLA+ since the mechanism and style of proof they embody is very different. TLA+ tries to ensure that you can exhaustively check implied models as its basis of proof (I believe) while Coq recognizes that types syntactically represent logics and we can thus construct programs in those logics to represent proofs.

So, one layer deeper they're dramatically different beasts.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#57

Post by SEMW »

lomnakkus wrote: post #15
frankmcsherry wrote: post #8

Earlier quoted context omitted.

I was formerly in the same lab as Leslie. As a side project, we (Tom Rodeheffer, mainly) used TLA to verify the correctness of Naiad's coordination protocol. The protocol is very simple (distributed reference counting), and my initial "proof sketch" was about two paragraphs long (and very unconvincing, apparently :). Tom's TLA+ version was closing in on 200 pages, available at http://research.microsoft.com/pubs/18382…

Very interesting, thanks (and to the other sibling poster). > Tom's TLA+ version was closing in on 200 pages, available at [snip] This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking b…

> I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?

http://us.metamath.org/mpegif/pm54.43.html (though using a slightly different set of axioms to R&W: http://us.metamath.org/mpegif/mmset.html#axioms)

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#58

Post by lmm »

bsdetector wrote: post #18
putzdown wrote: post #6

"I think most of us, including my math-phobic Facebook friends, would find the second version easier to follow and understand." I guess I'm in the minority. I preferred the words (though the translation was a bit ungainly).

I'd say the problem with math notation is that it simply has too many symbols. It has a different symbol for everything because it was designed as a handwritten system. For you mathematicians, think what you would do if you woke up tomorrow and all the math symbols had been replaced with emoji? I think most normal people would just learn the four operators and that's all... you know: megaphone, pizza slice, backpack,…

In many languages it's normal for a single symbol to encode a whole concept. Alphabetic scripts are artefacts of cultures that didn't have access to decent paper, and had to use a small number of simple forms that could be scratched / carved / etc. and remain recognizable.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#59

Post by gnaritas »

AnimalMuppet wrote: post #33
tormeh wrote: post #14

The problem isn't notation in itself; it's rarely used and non-self-explanatory notation that's a problem. You can achieve the same with words by inventing your own words and demanding that everyone learn them to understand you.

Which is just about the same as using a notation and demanding that everyone use the notation to understand you - except that a large number of people already know the notation.

No, words are better than notation, they're self descriptive; there's a reason we communicate with words instead of pictographs; words are more flexible and easier to create abstractions with than symbols.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#60

Post by swatow »

tel wrote: post #56
madsravn wrote: post #34

Earlier quoted context omitted.

I'm a referring the guys paper, which is linked here in the comments somewhere. There TLA+ is mentioned which is a tool to formally prove something. The same can be done in Coq - which is why I'm drawing a parallel.

While that parallel is genuine, it's hard to compare Coq and TLA+ since the mechanism and style of proof they embody is very different. TLA+ tries to ensure that you can exhaustively check implied models as its basis of proof (I believe) while Coq recognizes that types syntactically represent logics and we can thus construct programs in those logics to represent proofs. So, one layer deeper they're dramatically diffe…

you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summary of their structure.
Post reply on HN