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

71–80 of 103 posts

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#71

Post by im3w1l »

xamuel wrote: post #20
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,…

The reason for using different scripts (Greek etc.) is to sort symbols by broad categories. Done right, it actually makes things more readable (to the sophisticated reader, which is the mathematician's target audience anyway). It's almost like an implicit type system: (within a particular context) Greek letters mean ordinals, lowercase Roman letters mean predicate logic variables, uppercase German letters mean univer…

>Greek letters mean ordinals... mean universes

Maybe in your particular subfield.

When I think of epsilon or delta I think of a small number. Capital Delta is a difference. Capital Gamma is the gamma function. lambda is a wavelength. pi is a constant. theta is an angle.

a,b,c denote known constants. x,y,z denote variables to solve for. k,n,m denotes integers. i is the imaginary unit. f is a function. y is a function depending on x. Y is the integral(which in this context has nothing to do with integers)/laplace transform/fourier transform of y.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#72

Post by kiyoto »

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 "computer scientist", but I bet it is really far from what many laypeople (even the HN crowd) imagine to be computer scientists.

Another issue is, mathematicians have as much to do with mathematical pedagogy in secondary education as computer scientists have to do with science experiments in high school. Again, the title is really misleading in this regard.

Anyway, I am glad that a great mind like Leslie Lamport and David Mumford (definitely a mathematician) are thinking hard about how to make math education better.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#73

Post by grogers »

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…

The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#74

Post by tel »

grogers wrote: post #73
tel wrote: post #56

Earlier quoted context omitted.

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…

The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.

SMT is still a pretty far cry from type theoretic proof. At the end of the day it's just another kind of exhaustiveness checker.

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#75

Post by ajuc »

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

Math notation is OK, our ways to represent it digitaly are bad (because math notation isn't 1-dimensional string of symbols, it's actually 2-dimensional).

The solution is to make a way to represent it properly, not to throw it away (because we don't have a better 1-dimensional alternative).

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#76

Post by Xophmeister »

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.

j? Electrical engineer?

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#77

Post by Xophmeister »

chongli wrote: post #63
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…

From Wikipedia[1]:

"In the 9th and 10th century AD, Islamic mathematicians were familiar with negative numbers from the works of Indian mathematicians, but the recognition and use of negative numbers during this period remained timid. Al-Khwarizmi in his Al-jabr wa'l-muqabala (from which we get the word "algebra") did not use negative numbers or negative coefficients, although al-Karaji wrote in his al-Fakhrī that "negative quantities must be counted as terms"."

So it would indeed seem that your interpretation is what al-Khwarizmi meant.

[1] http://en.wikipedia.org/wiki/Negative_number#History

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#78

Post by adwn »

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.

> we could take x to be the matrix [[387, 320], [-480, -397]]

If x is a 2x2 matrix, how can the left side be equal to 39 (a scalar)?

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#79

Post by vlasev »

adwn wrote: post #78
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.

> we could take x to be the matrix [[387, 320], [-480, -397]] If x is a 2x2 matrix, how can the left side be equal to 39 (a scalar)?

It's 39 x^0 = 39 I

Re: A Computer Scientist Tells Mathematicians How to Write Proofs

#80

Post by Q6T46nT668w6i3m »

Chinjut wrote: post #25
vidarh wrote: post #22

The article starts with a false equivalence between archaic verbose language and mathematical notation. For my part, I usually prefer the prose. Formulas are easier to read for people who are used to and have practice with mathematical notation , but even then they are easier to read for those people when they are sufficiently complete , and formulas seem to often come with huge leaps and unstated assumptions. Especi…

Does prose not also often come with huge leaps and unstated assumptions?

It does! And that’s OK!

A proof is a proof if you’re convinced. Ideally, a proof is correct, but that’s not always the case.

(Except for undergraduates! Show your work! ;))

Post reply on HN