# Which mathematician sampled published proofs and found one third of them to have errors?

A recent question about whether/how we can trust mathematics in the face of human fallibility reminded me of a paper or article I read probably more than twenty years ago about a mathematician who was working at Bell Labs (I think) that had developed a novel proof mechanism. (He might have called it a "lucid proof"?) As I recall, it consisted of taking every single concept in the proof that wasn't blindingly obvious and giving it its own "appendix" where the proof of that bit was expanded until it was blindingly obvious that said part was true, possibly with its own appendices, etc, until every claim of the proof was fully exhausted in that manner.

Once he had the mechanism working, he tested it against some of his previous papers. To his horror, he found out that a bunch of his previous results were wrong. When he forced himself to eliminate every last shred of doubt about every claim, it turned out that many of his papers had claims--which had seemed obvious enough to not go through in excruciating detail at the time of writing the paper--which were, in fact, actually incorrect. The way I remember it was that his initial reaction was something along the lines of "holy crap, I'm an awful mathematician!".

Then it occurred to him to check the published work of other authors. From a random sampling (I doubt this was a statistically rigorous sample, I don't think that was the point) of published works, he found that a third of the results he tested failed to prove out when attacked with this method.

I have occasionally tried searching for this article to no avail, although in preparation for asking this question I tried again, and found this from Leslie Lamport which might refer to it:

Anecdotal evidence suggests that as many as a third of all papers published in mathematical journals contain mistakes—not just minor errors, but incorrect theorems and proofs.
How to Write a Proof (1993)

[EDIT: Maybe Lamport is the person, this paper describes the proof mechanism, and that "anecdotal evidence" he cited was from his own investigation. If you read the linked PDF, you will see that many of the parts of the story are there. It might well be that I mixed up Bell Labs with DEC, for example...]

The copy of the paper that I read was downloaded as a .ps file from some website in the 90s if I remember correctly.

I remember wondering if anyone paid attention to this result, if not, why not, etc, but I have not been able to locate it since. Does anyone know who the mathematician was, or where I can find the paper?

I would also be happy to find out what Lamport is referring to in the quoted section of the linked paper, if it isn't this. Or anything that will help me pick up this trail.

• @GHfromMO What are you basing those numbers on? Aug 21, 2019 at 23:16
• My own experience. I have read (refereed, reviewed etc.) a lot of papers. I also talk to my colleagues regularly, and I have not heard about any serious anomaly. The published literature (in decent journals) is very trustworthy. Are you a research mathematician? I am. Aug 21, 2019 at 23:25
• The 1% estimate is very close to the official 0% figure, put forward by math hardliners, and which is something toxic. From my own experience (I'm a professional mathematician too) around 70% papers are in need of at least a small fix. This is of course not a problem, math is wonderful as it is, and it always goes forward, one way or another. Aug 22, 2019 at 1:22
• Depending on the definition of the adjective "significant" in the phrase "significant error," I'm sure one could get almost any error rate in the range $[\epsilon,1-\epsilon]$. To get $1-\epsilon$, define an error to be significant if a computer proof assistant would notice something imperfect. To get $\epsilon$, define an error to be significant if the whole idea of the proof is completely wrong. Aug 22, 2019 at 3:00
• @GHfromMO : Experts certainly found that Perelman's arguments were "incomplete" in the sense that it took years to flesh them out. Even today, S.-T. Yau has gone on record (e.g., in his memoir "The Shape of a Life") as saying that he's worried about whether Perelman's argument is really complete. For a different kind of example, did the original (pre-Flyspeck) Hales-Ferguson proof of the Kepler conjecture contain "significant errors"? See Part 2 of arxiv.org/abs/0902.0350 Aug 22, 2019 at 3:22

I don't want anyone wasting time chasing this down for me, now that I've actually read the rest of the document I linked to in the question, I'm just going to assume that the mathematician I'm looking for is in fact Leslie Lamport or one of the people he mentions collaborating with.

He refers to this proof mechanism by the term "structured proof". The assertions or guesses about how much published literature might be incorrectly proven, in addition to the one-third number quoted above (and which @ToddTrimble mentions having heard from Lamport in a comment) are alluded to here (references in the original, emphasis mine):

The style was first applied to proofs of ordinary theorems in a paper I wrote with Martín Abadi 1. He had already written conventional proofs—proofs that were good enough to convince us and, presumably, the referees. Rewriting the proofs in a structured style, we discovered that almost every one had serious mistakes, though the theorems were correct. Any hope that incorrect proofs might not lead to incorrect theorems was destroyed in our next collaboration [3]. Time and again, we would make a conjecture and write a proof sketch on the blackboard—a sketch that could easily have been turned into a convincing conventional proof—only to discover, by trying to write a structured proof, that the conjecture was false. Since then, I have never believed a result without a careful, structured proof. My skepticism has helped avoid numerous errors.

I'm not sure if this document is the exact one that I read, but it's certainly close enough.

• 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:29
• 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
• @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:41
• 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:50
• 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 2:36