Timeline for Which mathematician sampled published proofs and found one third of them to have errors?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 21, 2021 at 18:52 | vote | accept | msouth | ||
| Oct 27, 2020 at 15:41 | comment | added | paul garrett | @lalala, these elementary things are well understood by serious people, I think, and the question of use-or-not of AxCh may not be the first issue I'd want beginners to worry about. But I'm not a formalist... | |
| Oct 27, 2020 at 15:28 | comment | added | lalala | @paulgarrett sometimes things are glossed over too much. I mean look at any introductory text (or ask yourself). How to prove that every surjective function has a right inverse. Easy isnt it? Did you use explicitly axiom of choice? no? | |
| Aug 22, 2019 at 3:01 | comment | added | msouth | @GerhardPaseman thank you, I ended up cutting that from the question text, because it can't do anything but misdirect. I have since found this reference that confirms your assertion. lamport.azurewebsites.net/pubs/pubs.html lists his employers as follows: Mitre Corporation ; Marlboro College ; Massachusetts Computer Associates ; SRI International ; Digital Equipment Corporation / Compaq ; Microsoft Research | |
| Aug 22, 2019 at 2:36 | comment | added | Gerhard Paseman | One problem is that Leslie Lamport did not work at Bell Labs. Gerhard "Been Reading Jon Bentley Lately" Paseman, 2019.08.21. | |
| Aug 22, 2019 at 0:50 | comment | added | Todd Trimble | I don't know that Lamport has done a careful study to justify the 33 percent. I sort of doubt it. This is not to deny that significant mistakes do slip by from time to time, and I think it's not a bad idea to secure prized results, such as those in say the theory of finite simple groups, by super-careful methodologies such as fully formalized proofs checked by computer-based proof assistants. This was done for example in the case of the Feit-Thompson theorem. | |
| Aug 22, 2019 at 0:41 | comment | added | msouth | @paulgarrett That's exactly what I find so interesting about it--it seems distinctly possible that there is a significant issue here that ought to be addressed. I would think someone of Lamport's stature (well, name recognition at least) could make a difference here, but, as the world of mathematics is populated by human beings, it's also believable that this concept presents the unpleasant prospect of doing a whole lot more work on your previous efforts to possibly find out that it's wrong, and that's not really the kind of thing that lends itself to enthusiastic voluntarily action. | |
| Aug 22, 2019 at 0:29 | comment | added | paul garrett | Based on various vague recollections, I think that it is indeed Leslie Lamport that you are thinking of. I do know that he does also have a notion of "structured proofs" or whatever words we might choose. For myself, though, I am a bit surprised that people would produce such fragile proofs (especially when they're not kids any more) that that a huge fraction would be "wrong". What about intuition? "Stability/robustness"? | |
| Aug 22, 2019 at 0:29 | comment | added | msouth | Knowing that Lamport was involved/interested/likely the author of the original, I will do a little more searching to see if that allows me to find the original document. Also, if someone is interested in tracking this down and giving me a better answer, please don't be discouraged by the fact that I posted an answer. I'll mark anything better that the above as accepted and/or incorporate comments if you'd rather. I just didn't want to launch people on a wild goose chase when I actually blundered into the answer myself in my pre-asking research and didn't realize it. | |
| Aug 22, 2019 at 0:26 | history | answered | msouth | CC BY-SA 4.0 |