5 ms·

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 a

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.

taeric 12y ago
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 that? I will say that this really looks like a way to write proofs for computers to read, moreso than a way to write them for other people. Probably has great value, but not too surprising that it isn't widespread.
- TylerJay 12y ago
  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/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
- j2kun 12y ago
  I also read through Lamport's critique and I'm not convinced by it. The 'errors' he points out are trivial, and the cultural assumption is that an active reader will fill in the omitted details.
Q6T46nT668w6i3m 12y ago
Hear, hear. Spivak motivated me to emphasize the humanistic features of mathematics. Thankfully, his view underpins elite mathematics programs, e.g. http://www.hcssim.org http://www.hcssim.org http://en.wikipedia.org/wiki/Math_55 http://en.wikipedia.org/wiki/Math_55
- sukilot 12y ago
  What does spivak have to do with Math 55? Math 55 assumes students can write a tolerable prose proof, it doesn't teach any particular style. Unless it changed in recent years.
  - Q6T46nT668w6i3m 12y ago
    > What does spivak have to do with Math 55? > Math 55 assumes students can write a tolerable prose proof.

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.

taeric 12y ago

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 that? I will say that this really looks like a way to write proofs for computers to read, moreso than a way to write them for other people. Probably has great value, but not too surprising that it isn't widespread.

TylerJay 12y ago
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/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
j2kun 12y ago
I also read through Lamport's critique and I'm not convinced by it. The 'errors' he points out are trivial, and the cultural assumption is that an active reader will fill in the omitted details.

Q6T46nT668w6i3m 12y ago

Hear, hear. Spivak motivated me to emphasize the humanistic features of mathematics. Thankfully, his view underpins elite mathematics programs, e.g. http://www.hcssim.org http://www.hcssim.org http://en.wikipedia.org/wiki/Math_55 http://en.wikipedia.org/wiki/Math_55

sukilot 12y ago
What does spivak have to do with Math 55? Math 55 assumes students can write a tolerable prose proof, it doesn't teach any particular style. Unless it changed in recent years.
- Q6T46nT668w6i3m 12y ago
  > What does spivak have to do with Math 55? > Math 55 assumes students can write a tolerable prose proof.