Coq is a proof assistant. It helps you to prove things, or at least check that your proofs are correct. For instance, people use it to prove mathematical theore

Coq is a proof assistant. It helps you to prove things, or at least check that your proofs are correct. For instance, people use it to prove mathematical theorems, or correctness of critical software. But apparently, there's a bug in the system that allows you to prove any properties, even invalid ones. So suppose that you proved Fermat last theorem in Coq, now you're not sure your proof is correct anymore since the deduction system is flawed! In theory, it invalidates all the proofs written in Coq. In practice, I don't think it's a big deal because it's unlikely that those proofs rely on this bug. But it's pretty funny to see that a system designed to be the ultimate verification tool is bugged.