Necessity of some means to find bugs in proofs (1)
lThis kind of situations happen in developments of formal proofs.
lSometimes, we cannot even the theorem is wrong, when we are not very familiar with concepts we
a particular software and hardware systems. (Your formal definitions may not represent your informal