My favourites are "close" to _formal_ false proofs in Coq.

1) In reply to a challenge by coq developer
>Who can address this challenge: find a "simple" statement $T$ (simple in the sense that anyone with a minimal background in logics can understand) such that you can prove both $T$ and $\neg T$ in Coq.

Daniel Schepler solved it [here](https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html?checked_cas=2). Daniel's proof was valid and passed coqchk, though it was not enough to prove False in Coq - Coq gave an "Universe inconsistency".
AFAICT the proof encoded a paradox.

2) Damien Pous [announced and gave link to code](https://sympa-roc.inria.fr/wws/arc/coqdev/2011-07/msg00018.html)
>There is a bug with vm_compute and values obtained from functors applications:
using the attached code, I can produce an assumption-free proof of False, or Bus errors.

False proofs in Coq are difficult because Coq produces a "certificate" that can be checked for validity (if one doesn't check the certificate and is happy with the compiler as most people do, it is much easier).