19 ms·
Leslie Lamport Tells Mathematicians How to Write Proofs (2014)
- cheez 8y agoGood software engineers reduce until everything unnecessary is gone. Same idea, nice to hear people talking about it.
- lixtra 8y agoHere is the description of hierarchical proofs: https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf
- geoalchimista 8y agoThis is a pure gem. It's like turning a prose into an abstract syntax tree for a human parser. :) I do think it adds to the clarity for the examples presented in it. But whether it applies well to more complicated proofs (those spanning hundreds of pages in a math paper) remains to be seen. I think at least writers of introductory textbook could adopt the style to benefit beginner students.
- j2kun 8y agoShould tag with 2014
- davnn 8y agoThe relevant paper is actually from 2011.
- j2kun 8y agoSince the article provides information and context, its date is probably the right one to use.
- davnn 8y agoYou‘re right.. my comment was thought of as a note for people skimming over the comments, sorry.
- bonzini 8y agoHe has been talking about hierarchical proofs for longer than that. I saw Lamport talking about "how to write a proof" in March 2006 (press release here, in Italian: https://www.usi.ch/it/comunicati-stampa/2991 https://www.usi.ch/it/comunicati-stampa/2991).
- dang 8y agoDone now.
- aoki 8y agomathematicians writing for peers don’t aim for the maximally explicit proof. details are frequently left out as obvious to the knowledgeable reader. leaving out tedious matter is a matter of professional style, like tightening regular prose so it doesn’t club the reader over the head with every detail. (my instructor in Fourier analysis would subtly grimace at my very explicit proofs in office hours, but he knew i was a computer scientist so he politely said nothing because he knew it would do no good ;-)
- throwaway080383 8y agoI would also add that by and large this isn't done because of ego, but simply brevity. Seminal papers are often already hundreds of pages long, so to add every detail would bloat them to thousands of pages. And in any case, "skipping steps" is exactly how the top mathematicians think about the proofs when creating them.
- loup-vaillant 8y agoYeah, well, paper sucks. http://worrydream.com/#!/ScientificCommunicationAsSequentialArt http://worrydream.com/#!/ScientificCommunicationAsSequential... No mathematician today doesn't have access to a computer. Just fold the proof to some appropriate coarse level by default, and let the reader expand any part they want to read. It's not like our computers had any meaningful limit on how big a mathematical proof could be.
- AnimalMuppet 8y agoI think the limit may be the author, not the tool the author writes with.
- loup-vaillant 8y agoHistorically, there was always a limit to how big a paper could be to make it into a journal. Papers that aren't meant to make it into a journal are often way bigger.
- allenz 8y agoLamport advocates for more rigorous proofs with a justification for every line, and lines arranged in a hierarchy based on assumption contexts. He is also the author of TLA+, a formal proof checker: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B Fully-justified proofs are frequently used to teach geometry and abstract algebra, and are also needed for machine-checked proofs. Outside these contexts, I agree with Lamport that they are useful to catch mistakes, but I wouldn't write them myself because they are incredibly tedious. For communication in papers, narrative proofs can convey ideas and intuition at a much higher bandwidth.
- repolfx 8y agoHigher bandwidth but also greater risk of mistakes? If the article is true that 1/3rd of papers have false theorems in them, that seems like a problem severe enough to justify slowing down and being more methodical.
- archgoon 8y ago> 1/3rd of papers have false theorems in them Despite the wording in the article, this is false. A theorem is not false if there is an error in a proof for it. They only showed that 1/3 proofs of theorems had an error. It doesn't say if these were minor errors (omitting an edge case where it's still true, but not handled in the proof, but easily covered), or major (the theorem is actually false). Quoting the article: > Some of them were false because the proofs were wrong, and some were false because they relied on wrong proofs. This is not what 'false theorem' means. This might be pendantic, but isn't that kind of the point here?
- loup-vaillant 8y agoRegardless, unproven theorems should not make it to publish papers. At the very least, they should be marked as "conjectures".
- gizmo686 8y ago
- adamnemecek 8y agoMore mathematicians need to know about constructive mathematics https://en.m.wikipedia.org/wiki/Constructivism_(mathematics) https://en.m.wikipedia.org/wiki/Constructivism_(mathematics) Basically, proof by contradiction is not a good idea.
- Yajirobe 8y agoAlso, lets throw out the law of excluded middle and axiom of choice!
- adamnemecek 8y agoNo, let’s replace law of excluded middle with axiom of adversarial choice.
- JadeNB 8y ago> lets throw out the law of excluded middle I don't think that we should throw it out, but neither do I think that we shouldn't do so.
- stan_rogers 8y agoThat is the mechanism by which junk drawers and attics are filled.
- archgoon 8y agoI believe most mathematicians are well aware of constructive mathematics. What makes you think that they aren't? > Basically, proof by contradiction is not a good idea. Based on what?
- adamnemecek 8y agoThat most math books I read don’t discuss it.
- AnimalMuppet 8y ago
- User23 8y agoDijkstra also challenged the sloppiness of traditional mathematicians frequently in his EWDs. His proof format is extremely readable, and each proof is a complete manipulable mathematical object, with the steps tied together by implication, consequence, or equivalence and the validity of the step documented.
- zeth___ 8y agoCould you provide a link or citation where he does an expose no it? I am interested.
- User23 8y agohttps://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1073.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E... is an example. That site has many others. Predicate Calculus and Program Semantics is a book that is based on the technique.
- geoalchimista 8y agoI found one more example in this TeX StackExchange question [1]. It's incredibly elegant. But the problem is that it does not seem to be easily reproducible in LaTeX because writing nested lists is such an unnecessary pain (take a look at the adopted answer). Need a package to popularize this style. [1] https://tex.stackexchange.com/questions/49416/which-packages-practices-are-relevant-for-writing-structured-derivations-simil/438750 https://tex.stackexchange.com/questions/49416/which-packages...
- urmish 8y agoFor some reason this seems incredibly funny to me. I can imagine mathematicians laughing at this too.
- s-shellfish 8y agoComputer science is more rigorous than mathematics. The proofs written for computers have to actually work in computer, which is a collection of mathematics that have provably been demostrated to retain their fundamental basic properties that allow computation to both define and test the validity of statements.
- blattimwind 8y agoIf so, then that's because traditional mathematical proofs are arguments meant to convince humans of the validity of a claim. They are formal only insofar as e.g. law is formal.
- s-shellfish 8y agoPeople's minds have a limit to how much information they can retain. Pushing new information in comes at the expense of pushing other information out. Computer science isn't limited this way because every simplified property of mathematics is retained mechanically. If a property is created that is invalid, computation ceases to be computation. Minds on the other hand, aren't so limited, but that doesn't mean that what they produce is rigorous (or correct, with respect to the context they've been defined in). I agree with you, if that's not clear. I don't understand your law analogy precisely, but I'm assuming in a general sense you mean 'human defines rule set, rule set retains it's properties provided that humans continue to enforce rule set'. To my mind, that is so open to variation, my brain may begin to attack itself. Humans can 'make sense' of anything. Computation needs to be able to do what it does regardless of whether a human is there to provide input and verify it 'makes sense' to the mind that defined it. Universe turning into paperclips, sure, but the fact that a set of properties can be used to recreate themselves through their own definitions, that's beautiful, that's computation, rigor. These are things I used to love about math, but computer science just does math better than math does.
- fizixer 8y agoThat's a rubbish title. (edit: the original title was 'Computer scientist tells mathematicians how to write proofs') Leslie Lamport is a mathematician by education. And I have a good idea he'd prefer to be called a mathematician if he had to choose between the two labels (mathematician and computer scientist). That's not to say CS, and programming, doesn't contribute to the process of rigor. In fact, I had a realization that a program is a form of constructive mathematics, and hence a program is more rigorous than a proof on paper in the following sense: a single typo in a math proof would be overlooked by the reader, but a single typo in a program could make it fail. Still, in order to make connections between programming and mathematical rigor, you have be trained in mathematics, not just computer science.
- deleted 8y ago[deleted]
- tuukkah 8y agoThere's a recent example of programmers publishing a paper on how to better prove some mathematics by implementing and discussing the phenomenon in a programming language: What’s the Difference? A Functional Pearl on Subtracting Bijections https://byorgey.wordpress.com/2018/06/23/new-icfp-functional-pearl-on-subtracting-bijections/ https://byorgey.wordpress.com/2018/06/23/new-icfp-functional...
- kleiba 8y agoFunny how the blog is trying to use the x^2 + 10x = 39 example to illustrate that modern notation helps understanding and reducing errors, but then forgets the second solution for the equation (x = -13). In all fairness, though, it's is just meant as a translation of al-Khwarizmi's text into modern notation where only one solution is given.
- saagarjha 8y ago> In all fairness, though, it's is just meant as a translation of al-Khwarizmi's text into modern notation where only one solution is given. Probably because negative solutions were not recognized as valid at the time.
- _Microft 8y agoThe backlash he experienced might be due to the style in which he introduces his interesting work. While not quite obvious, he could be seen as adverserial by labelling hierachical structured proofs as "proofs of the 21st century" and the ones other mathematicians use as "17th century proofs". Promoting them as a thorough way to write proofs with additional advantage for the reader to adjust the level of detail of the explanation to their respective level of knowledge might have been a way to get people involved. He's even asking for feedback [1], unfortunately only to denigrate the adressed people in the next sentence [2]. It reminds a bit of Ignaz Semmelweis who managed to do good by reducing mortality of women in childbed by requiring desinfection before examinations but failed to spread the idea by being adverserial to his colleagues [3]. [1] "I am sure my way of writing proofs can be improved, and I encourage mathematicians to improve it", How to Write a 21st Century Proof, p. 5 [2] "They will not do it by remaining stuck in the 17th century.", How to Write a 21st Century Proof, p. 5 [3] https://en.wikipedia.org/wiki/Ignaz_Semmelweis https://en.wikipedia.org/wiki/Ignaz_Semmelweis
- stevesimmons 8y agoI feel you do Leslie Lamport a disservice here. I read the SciAm article and the full "How to Write a 21st Century Proof" and did not get any sense of denigrating people or being adversarial. Sure, he is concerned about clarity and correctness, but that is the exact point of mathematical proofs. So everyone else, please skim the SciAm article and then take 15 minutes to enjoy reading the paper [1] in Lamport's own words. [1] https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf
- _Microft 8y agoIt's not clarity or correctness but how it is said. See page 2 of the paper (page 5 of the PDF) for example. That is where he is talking about people being stuck in the 17th century and "how sloppy their proofs are" [1]. I am not arguing that this might not be true! - I argue that it is not helpful to approach introducing and advertising the idea in this way. I'm not a mathematician but I'd understand if someone reacted with defiance to wording like this. [1] https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf, p.2 (PDF page 5)