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...
An example of wrong proof due to sketching quickly some cases is the proof that all triangles are isosceles [1].
Here is also an example of an apparently obvious result with a non-trivial proof, were all the cases are written out formally in the proof-assistant language Coq [2]. It is the proof that if we compute the multiplications and the square roots with floating-point arithmetic in base 2, then sqrt(a*a) is actually |a|. This was assumed without proof in some previous papers, and it is easy to understand how the authors may have missed it. Note that this result is not true in base 10.
Finally, sometimes non-formal proof can actually be more convincing than formal proof. For example, it was proven formally in 1957 that it is possible to turn a sphere inside out continuously, without cutting it, tearing it or creating any crease [3]. With more work, this result was later proven with a video. The video proof is arguably easier to follow and more convincing for a human. The formal proof has not yet been formally checked by a proof assistant, although work in this direction is on the way [4].
[1]: https://www.themathdoctors.org/false-proofs-geometry/
[2]: https://inria.hal.science/hal-01148409v1/document
For one thing, they'd be much longer, and likely not human-readable.
Formal verification is getting more mainstream, but it's not there yet.
Come to think of it, imagine a mathematition going 'trust me bro, I've proved this'