[FOM] Formally verifying "checkers is a draw"

[Josef Urban]

On Mon, Aug 11, 2014 at 4:24 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> 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.

Sure. But we are trying to make this amount of labor smaller and
smaller. And for me the goal is not just to have "error-free" math (or
software, etc.). It is also to automatically understand and assist
(using completely formal semantics as the secure bottom layer) the
human (math) reasoning and disambiguate the human-level (math)
concepts and language.

>
> 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.)

I think as long as (some form of) the Moore's law holds, this might
not be a serious issue. Compared to ten years ago, working with the
largest formal math libraries has become very easy - practically all
of it fits today in a notebook's RAM. Re-checking Flyspeck ten years
from now will probably cost very little.

Josef