But in general it’s reasonably common for a proof to have been written up to the best of the author’s ability, and for it still to be impossible for anyone else to understand it well enough to be confident in its correctness.
Formal logic was no help, for two reasons. First of all the formal logical systems of the early 20th century were really a sort of existence proof, to show that a formal logical system can in principle be defined, and were too unwieldy and verbose for practical use in non-trivial situations. Secondly, it would then become necessary for the reader to check the correctness of a proof in formal logic, which is an even more difficult task than checking a well-written informal proof.
But this is changing: modern formal proof systems are designed with user-friendliness in mind, and produce proofs that can be verified by computer. It’s now starting to happen that formalisation can be used as a way out of the impasse where a proof is too complicated for anyone but the author to understand. I can think of two examples of this: Thomas Hales’s Flyspeck project [1] was the first such case, and required a monumental effort from Hales and his collaborators. Much more recently, Randall Holmes’s proof that NF is consistent was formalised [2], finally putting to rest a very old question in the foundations of logic.
1. https://arxiv.org/abs/1501.02155
2. https://www.logicmatters.net/2024/04/21/nf-really-is-consist...