4 ms·
Lamport 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 a
by allenz 8y ago
Lamport 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 agoThere is a difference between unproven, and the published proof contains a mistake.
- loup-vaillant 8y agoSeriously, who cares? When you publish the proof for a theorem, you're generally the first to do so. Aren't you? If there is an error in the only published proof ever, your theorem is unproven. QED. Edit: to downvoters: please explain my error. I thought I was only telling the obvious here.
- cma 8y agoMaybe they feel you didn't rigorously prove your case.
- loup-vaillant 8y agoThey more likely didn't read past the first sentence. I suspect a very thin skin. Seriously though, I don't know what makes this forum tick. Someone's gotta explain what is socially acceptable around here. I know we're not supposed to complain about votes here, but I genuinely don't understand what happened. (Or rather, what is happening, the votes seem to flow up and down for no discernible reason.)
- pvg 8y agoWhining about downvotes and then trying to goad other users is bad and you shouldn't do it.
- loup-vaillant 8y agoPerhaps, but it looked like it worked. Somehow. For now. At the time I write this, the comment you are replying to is still positive (edit: oops, no longer), while it clearly breaks the stated rules of this forum (sated both officially and by you just now). And I'm pretty sure that if I didn't do it, my "who cares" comment above would have been further downvoted. I observed this several times on several forums, sometimes votes have a momentum, and breaking the rules like I did can sometimes stop that momentum. (This works the other way too: popular comments often stop having further upvotes after the first reply that disagrees.) Incidentally, I really think a good proportion of downvoters hit the button before reaching the end of the comment. Not because they're personally offended, but because their troll filter judge quickly, from the very first words (thinking back with a cooler head, I can't blame them). Starting a comment by something that looks offensive if taken out of context is a pretty sure way to get it downvoted to oblivion. Still, the threshold looks pretty damn low.
- allenz 8y agoFully justified proofs certainly don't belong in the main text of a paper, but they could be included as an appendix along with all the other uninteresting proofs. In theory there is a greater risk of mistakes, but I don't think that it's enough to justify that much extra work. A small study is not enough evidence.
- ISL 8y agoJust as with email threading, one could reasonably collapse steps that are tedious/trivial without removing them entirely from a digitally-documented proof. Completeness and brevity are not entirely at odds.
- deleted 8y ago[deleted]