Expressing proofs as formal logic is a great tool to make them more rigorous. Formal proofs are easier to check with a computer, provided that all the cases have been fleshed out, and that it has been written in a proof-assistant language. However those proofs are tedious to write, and a human reader has a limited capacity for handling high number of cases. Omitting cases and writing out informally why those cases can be omitted is crucial to help the reader to follow the proof. That is a step where errors can arise.

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

[3]: https://en.wikipedia.org/wiki/Sphere_eversion

[4]: https://leanprover-community.github.io/sphere-eversion