This is a follow-on from this question, where I pondered the consistency strength of Coq. This was too broad a question, so here is one more focussed. Rather, two more focussed que …

The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$. According to Coq $$ a \mod 0 = 0$$ and Isabelle proves $$ a …

Damien Pous announced code for assumption-free proof of False in Coq which means inconsistency in Coq (without using exploits, lol). Damien is critical of "fully certified decisio …