My favourites are "close" to formal false proofs in Coq.
- 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. 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.
- Damien Pous announced and gave link to code
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).