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

91–100 of 103 posts

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#91

Post by j2kun »

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,…

> what really kills me is when programmers use untypeable symbols

Maybe the problem is that "untypeable" symbols should be easier to type. Mathematicians get by just fine with their typesetting system. Maybe the problem is that programmers are constrained by ASCII, and mathematicians have the upper hand because they have the freedom to define their own notation.

Maybe the "problem" is a matter of perspective.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#92

Post by vilhelm_s »

kiyoto wrote: post #72

As a math major who went to grad school in CS theory, I find the article's title vexing. It projects a faux dichotomy of computer scientists v. mathematicians when, in reality, it's mathematicians v. mathematicians. Many areas of computer science, at least the areas in which Leslie Lamport is best known, is a strongly mathematical discipline inspired by models of computing. Dr. Lamport probably considers himself as a…

> Dr. Lamport probably considers himself as a "computer scientist", but I bet it is really far from what many laypeople (even the HN crowd) imagine to be computer scientists.

Sure, but I guess he is also really far from what most mathematicians imagine to be mathematicians.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#93

Post by noahl »

j2kun wrote: post #83

I agree with the concerns on the false dichotomy between theoretical computer science and mathematics, but from the mathematician's perspective I think there's another issue not being discussed due to the typical CS obsession over automated proof systems. Mathematics is a social subject, invented by humans largely for their own amusement. The goal of a mathematical proof is to communicate insight to other humans. Of…

What do you think of the idea of writing proofs in the hierarchical style in Lamport's section 3, but not using TLA? To me, the hierarchical proofs seemed very clear and easy to understand, but the TLA (although I only skimmed it) seemed to introduce too much formalism and thereby hurt readability.

Also, it would be easy to put paragraphs of text in between hierarchical proof statements, which would preserve the ability to give intuition and proof sketches. Here I'm thinking of things like analysis, where (at least in my experience) what you really want to do is see the picture of the proof in your head and understand it that way, and the written proof is always just a way of checking it.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#94

Post by scrumper »

fsk wrote: post #67

The problem is that, in Math papers in journals, there's charges based on the number of pages used. You really would need an electronic format, and a wiki-style format that graduate students can use, to fill in the details of all the proofs. When I was a grad student reading papers, it would sometimes take me a day or two to read a sentence, filling in all the details. I felt bad that there was no way for me to share…

This is a fantastic idea, something I'd use as a consumer. It dovetails nicely into the growing movement around democratizing access to scientific research as well.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#95

Post by bshanks »

Xophmeister wrote: post #76
Chinjut wrote: post #61

Earlier quoted context omitted.

There are more solutions than just that; for example, we could take x to be the matrix [[387, 320], [-480, -397]] (so x^2 = [[-3831, -3200], [4800, 4009]]), or the split-complex number 8j - 5 (so x^2 = 89 - 80j), or 5 in the ring of integers modulo 36 (so x^2 = -11). But al-Khwarizmi was presumably writing in the context of familiar quantities >= 0, which is a perfectly fine thing to do.

j? Electrical engineer?

In the context of electrical engineering, j is often used to denote the imaginary unit, that is, something such that j^2 = -1; in other words it's the same as what is usually called 'i'.

But, in the context of the split-complex numbers, j is something such that j^2 = 1, and i suppose it is writen as 'j' to distinguish it from 'i'.

So, the 'j' used here is different from the 'j' used in electrical engineering.

( https://en.wikipedia.org/wiki/Split-complex_number )

For example, if j were the square root of -1, as in electrical engineering, then (8j - 5)^2 would equal -39 - 80j: 64j^2 - 80j + 25 = -64 -80j + 25 = -39 - 80j; but here, in the split-complex numbers, (8j - 5)^2 = 64j^2 -80j + 25 = 64 - 80j + 25 = 89 - 80j.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#96

Post by j2kun »

noahl wrote: post #93
j2kun wrote: post #83

I agree with the concerns on the false dichotomy between theoretical computer science and mathematics, but from the mathematician's perspective I think there's another issue not being discussed due to the typical CS obsession over automated proof systems. Mathematics is a social subject, invented by humans largely for their own amusement. The goal of a mathematical proof is to communicate insight to other humans. Of…

What do you think of the idea of writing proofs in the hierarchical style in Lamport's section 3, but not using TLA? To me, the hierarchical proofs seemed very clear and easy to understand, but the TLA (although I only skimmed it) seemed to introduce too much formalism and thereby hurt readability. Also, it would be easy to put paragraphs of text in between hierarchical proof statements, which would preserve the abil…

I think people already do write things in a hierarchical way. They have one main theorem which is supported by multiple propositions and lemmas and corollaries. At least, this is how all good papers I read are organized.

I think Lamport's vision is that the hierarchy extends down to the very last detail. This is what I'm skeptical of, because no mathematician has time to do this. To paraphrase Newton, you need to stand on the shoulders of giants to make progress.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#97

Post by sukilot »

Q6T46nT668w6i3m wrote: post #82
bsdetector wrote: post #28

Earlier quoted context omitted.

Yes that's the pre-computer I was talking about. Sophisticated mathematicians should be concerned about if it is machine readable or not. If it's machine readable then you can use whatever font, color, or any other style you want that helps you to read it. The viewer can abbreviate descriptive names to single glyphs if you want. Programming is much less fun, and harder to follow, without syntax highlighting. But it d…

Why? I write mathematics to share with mathematicians, not machines. Would you ask a poet to make the same sacrifice for machine comprehension?

A poem can mean whatever any reader wants it to. In math objective truth matters.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#98

Post by sukilot »

Q6T46nT668w6i3m wrote: post #85
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.

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://en.wikipedia.org/wiki/Math_55

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.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#99

Post by sukilot »

gnaritas wrote: post #59
AnimalMuppet wrote: post #33

Earlier quoted context omitted.

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.

Words are less precise, so they can be used to approximate ideas we don't clearly understand.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#100

Post by Q6T46nT668w6i3m »

sukilot wrote: post #98
Q6T46nT668w6i3m wrote: post #85

Earlier quoted context omitted.

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://en.wikipedia.org/wiki/Math_55

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.

> What does spivak have to do with Math 55?

> Math 55 assumes students can write a tolerable prose proof.

Post reply on HN