[FOM] Formally verifying "checkers is a draw"

[Rob Arthan]

On 11 Aug 2014, at 15:24, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Right.  I wonder, though, whether the frequency of errors in the mathematical literature (paper or electronic) is limited less by physical errors of the type you mentioned than by "risk compensation."
> 
> http://en.wikipedia.org/wiki/Risk_compensation
> 
> After all, if mathematicians really cared enough, then the error rate in the conventional literature could presumably be driven down significantly below its current value, even without machine assistance.  I don't think we're at the limit of human capability to keep errors out of published journal articles.  The reality is that we don't care *that* much about an error-free corpus of mathematics.  We have a certain risk tolerance, and under certain circumstances prefer to tolerate a certain probability of error than to invest herculean amounts of labor to drive that probability down.

I think fault tolerance (http://en.wikipedia.org/wiki/Fault_tolerance) rather than risk tolerance is what is relevant in the pure mathematics research process. Knowing that people make mistakes and that standard definitions change, good mathematicians check the proofs in their references, expecting to find and fix mistakes or to find an alternative reference or a proof of their own if there is a mistake they can’t fix. This isn’t risk tolerance, because risk tolerance would involve assigning a probability to the correctness of your references,
deriving from that a probability of the correctness of the claims you base on those references and then
coming to a judgment about the acceptability of that risk. Good engineers (should) do this kind of assessment all the time, but mathematicians should not need to.

Regards,

Rob.