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

61–70 of 103 posts

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#61

Post by Chinjut »

mitko wrote: post #53

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…

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.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#62

Post by tr352 »

"His method, which you can read about in more detail on his website (pdf), is a hierarchical structure that doesn’t seem entirely dissimilar from the two-column proofs that most of us learned in middle school or high school geometry class, although he points out that it can handle complex problems that would be unwieldy in that two-column format. Each line is numbered, and each assertion is justified with numbers referring to previous lines and assertions."

This is just too obvious. Every proof has this structure, though sometimes this structure is left implicit (which may or may not be a good ting).

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#63

Post by chongli »

mitko wrote: post #53

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…

Read al-Khwarizmi's writing again:

“A square and 10 roots are equal to 39 units. The question therefore in this type of equation is about as follows: what is the square which combined with ten of its roots will give a sum total of 39? The manner of solving this type of equation is to take one-half of the roots just mentioned. Now the roots in the problem before us are 10. Therefore take 5, which multiplied by itself gives 25, an amount which you add to 39 giving 64. Having taken then the square root of this which is 8, subtract from it half the roots, 5 leaving 3. The number three therefore represents one root of this square, which itself, of course is 9. Nine therefore gives the square.”

If you interpret square to mean a literal square, then x can't be -13 as that would give a square whose sides are negative in length.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#64

Post by threatofrain »

_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.

Well I think you are talking about actual source code, and not the context of expository or academic writing. In that context, I would not trust comments even if companies had a strict policy of updating comments, because personally I just don't want to be susceptible to that.

It does make me wonder, though, about those computer-generated proofs which are so massive that no human can understand it. If you can run it...?

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#65

Post by spc476 »

SixSigma wrote: post #47
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…

> Programming is much less fun, and harder to follow, without syntax highlighting. That's your opinion.

Then there's Color Forth, where color is used as syntax (http://www.colorforth.com/cf.htm).

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#66

Post by gone35 »

qznc wrote: post #51
gone35 wrote: post #23

Earlier quoted context omitted.

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/

Damn; this is amazing stuff... I had no idea: (from [1]) so just get a local copy, set the path, and voila you can import... Wonderful. Thank you for sharing this!

http://afp.sourceforge.net/using.shtml

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#67

Post by fsk »

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 my progress with others. Someone else reading the same paper (other than the author or a couple of other experts) would have to do the same thing as I did.

I thought it would be a neat project, but my advisor said it would be bad for my career if I spent time on it, so didn't pursue it. To find a job, it would be based on the papers I published, and not based on making other people's research easier to read.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#68

Post by douche »

lmm wrote: post #58
bsdetector wrote: post #18

Earlier quoted context omitted.

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.

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

This is largely incorrect. Outside of Han China and a few other areas in its historical cultural area of influence, alphabetic scripts won over ideographs, and won big time. The Egyptians developed paper-like papyrus thousands of years before the first uses of "paper" paper, and they largely abandoned their ideographic hieroglypics in favor of the Heiratic and Demotic scripts, which are syllabaries, for all but formal usages.

Now if the Mongols or the Khitans or the Uygher steppe empires had been able to impose their scripts on the Chinese after conquering them, instead the assimilation going the other way, Unicode might be a considerably smaller clusterfuck today.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#69

Post by zhte415 »

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…

Like a RapGenius of mathematical (or other rigorous) proofs? I think this would be amazing, especially for academics in fields related to the topic at hand but not deeply involved, or interested laymen.

As a teaching tool it would be equally useful, even from the first year of university.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#70

Post by throwaway000002 »

Chinjut wrote: post #61
mitko wrote: post #53

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…

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.

I haven't checked your work, except over Z/36Z, but you made me :)
Post reply on HN