[A recent question][1] 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.][2]

[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.

  [1]: https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-even-though-humans-quite-often-make-mistakes-in
  [2]: https://lamport.azurewebsites.net/pubs/lamport-how-to-write.pdf