[FOM] Formally verifying "checkers is a draw"

[Timothy Y. Chow]

On Mon, 11 Aug 2014, Josef Urban wrote:
> I do not think anybody argues that computer verification gives a 100% 
> certainty.

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 speculate that a similar effect will come into play after formally 
verified mathematics becomes commonplace.  The cost of re-verification 
will gradually rise to the point where people will prefer to accept the 
risk of an error, rather than expend the necessary computer time.  So the 
eventual limiting factor will not be technological but sociological---just 
as it is now.  (This is not to say that formal verification won't drive 
down the error rate, just that it won't be driven down as low as a 
calculation of hardware error rates might naively suggest.)

Tim