A Computer Scientist Tells Mathematicians How to Write Proofs
blogs.scientificamerican.com
blogs.scientificamerican.com
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.
Sure, but I guess he is also really far from what most mathematicians imagine to be mathematicians.
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 course the point is also to be correct, but somehow communicating insight takes priority. Relying on large bodies of latent knowledge, and omitting details, is an effective way to do that. Allowing for occasional mistakes is okay, because mathematics as a whole is fault tolerant (or at least, history gives evidence to that claim).
Lamport's field is a bit different, because there they study distributed protocols with the intent of creating value in the real world. So when they prove a theorem, they're not just proving a theorem to gain understanding about something, they're proving a theorem so they can improve the security or fault-tolerance (or whatever else) of some real system. Writing down a 200+ page TLA proof is measurably worth the investment because the users of their work (applied computer scientists and engineers) want error-free theorems and a clean CS literature much more than they want insight.
For mathematicians communicating to other mathematicians, a two-paragraph argument that is convincing and omits the details (that one can verify on their own) is much more valuable. I'm not trying to make a value judgement either way, just trying to explain the culture of math proofs and why I think something like TLA+ will never catch on among mainstream mathematicians. You might say it's mathematicians defending their job security, but it's also simply that mathematicians like exploring and inventing and hearing creative proofs and perspectives. Deferring things to computers removes the a-ha moment.
[Edit] And the idea that somehow high school students and undergraduates will magically start reading and understanding proofs because we write them using TLA+ is a joke.
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.
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.
I've been toying with idea of trying this for a not-quite-trivial (programming!) project I'm working on, but the documentation and UX have so far kept me quite skeptical of using this "for real". The fact that I also can't turn the proof into a program in a semi-automated fashion also seems to indicate that there's at least some barrier where the "doubled" amount of work would be justified. (I'm more inclined towards something like Idris or LiquidHaskell which seem to support practical programming better and will probably let you get arbitrarily close to "proof" in any practical sense where proof will matter.)
I take it that this was mostly about mathematics and not implementations of programs, which may not quite have the same trade-offs. I still would like to hear from anyone with direct experience :).
http://research.microsoft.com/pubs/183826/paper.pdf
A short publication about it, with some reflective discussion of why it was hard to write down, is at
http://research.microsoft.com/pubs/199767/clock-verif2.pdf
My understanding is that part of the problem was that Tom needed to explain (re-prove) many meta-facts we take for granted.
> 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 by computer-based proof assistants, but I digress...
One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.)
Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?
EDIT: Russel & Whitehead
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)
(Sorry if this already exists; I'm just an interested layman.)
TLA+ isn't only a model checker & theorem prover, though. The language itself is an excellent high-level way of expressing system design. Recently I've been applying it to eventually consistent systems, and writing an idea in TLA+ is a great way to flesh out the concept and spot hidden assumptions or edge cases. Lamport knows this; in the introduction to his TLA+ book, he quotes:
"Writing is nature's way of letting you know how sloppy your thinking is."
Followed by his own expansion on the concept:
"Our basic tool for writing specifications is mathematics. Mathematics is nature's way of letting you know how sloppy your writing is. ... The mathematics we use is more formal than the math you've grown up with. Formal mathematics is nature's way of letting you know how sloppy your mathematics is. The mathematics written by most mathematicians and scientists is not really precise. It's precise in the small, but imprecise in the large. Each equation is a precise assertion, but you have to read the accompanying words to understand how the equations relate to one another and exactly what the theorems mean. Logicians have developed ways of eliminating those words and making the mathematics completely formal and, hence, completely precise."
Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in.
You may also be interested in the AWS paper, which had excellent results.[2]
[1] https://plang.codeplex.com
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/am...
This sounds very intriguing. It guess there's at least some learning curve, but maybe it'll be a fun experiment vs. P&P in future. ;)
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.
But al-Khwarizmi was presumably writing in the context of familiar quantities >= 0, which is a perfectly fine thing to do.
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.
If x is a 2x2 matrix, how can the left side be equal to 39 (a scalar)?
“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.
"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.
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.
As a teaching tool it would be equally useful, even from the first year of university.
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.
Especially in computer science papers I tend to see extensive use of formulas over prose or - preferably - code or pseudo-code as big warning signs: Often it turns out to mean the author is glossing over a massive amount of hugely important details. E.g. a common problem I saw when studying was papers that would describe processes, but omit any indications of sensible ranges for parameters that were essential to getting good results (I was working on techniques for image processing to improve OCR results), or greatly obscure details of algorithms that would have taken no more lines to write out in working code.
Maybe there's a sort of golden middle way here where all mathematical prose-proofs should be annotated[1] by the associated computer-checked proof. The trustworthiness of a particular proof could be assessed by the number of such references and how much coverage (of the prose) they provide...?
[1] Perhaps only by reference, as here. :)
EDIT: Quick edit, I say this as someone who -- earlier in xir career -- probably subjected a lot of people to somewhat verbose comments. In practice, my comments were usually right and the programming language wasn't powerful enough to capture the semantics of what I was doing. One hopes this is the distinction between good and bad comments. Sorry for veering off-topic.
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...?
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! ;))
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, and recycle.
Math is what it is, designed for a pre-computer world, but what really kills me is when programmers use untypeable symbols like α (alpha), which at least is an actual letter in one language, or worse yet random unicode like · ("middle dot") or ∕ (division sign, not /). There's just no excuse for that.
Programming is much less fun, and harder to follow, without syntax highlighting. But it doesn't follow that we should manually be color coding syntax and variables, or that integers should always be blue. That's essentially the case with the "readability" of mathematics.
That's your opinion.
Would you ask a poet to make the same sacrifice for machine comprehension?
Maybe? Penelope Maddy, et al, have convinced me that this isn’t as clear as we’d like:
http://www.socsci.uci.edu/~pjmaddy/bio/DualistVol15_Maddy.pd...
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.
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.
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).
The best feature of mathematical notation is its ambiguity. It needs to be parsed by a human, not a machine. Poetry is similar. There’s tradition, but few rules.
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.
http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
[0] https://en.wikipedia.org/wiki/Outliner
[1] Not really surprising. Lamport invented LaTeX.
If you are interested in computational logic you might enjoy Aaron Stump from UIowa's work: https://queuea9.wordpress.com/
> 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.
So, one layer deeper they're dramatically different beasts.
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.
http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
Thankfully, his view underpins elite mathematics programs, e.g.
> Math 55 assumes students can write a tolerable prose proof.
If only that were true of a piece of LaTeX moved from one place to another, haha!
http://i.imgur.com/omXqvos.png
Well, technically I learned proofs from Euclid first. But this book followed close behind.
Clear and comprehensible (once you learn the basic symbols). Very much structured. There's hardly any prose in the whole two volumes.
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).
Of topic but in a similar vain: in a completely different field I dabble in reconstructing existing theories in structuralism. There's some very valid criticism of the method and yet it still unearths issues with theories every now and then.
http://en.wikipedia.org/wiki/Structuralism_%28philosophy_of_...
Does anyone know of interesting initiatives out there to build an open repository of mathematical proofs?