[Math] Which mathematician sampled published proofs and found one third of them to have errors

Question

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.

Answer 1

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.