[cap-talk] theory and practice

[David Hopwood]

David Hopwood wrote:
> Jed at Webstart wrote:
>> David Hopwood wrote:
>>
>>>I hope and expect that at some point in the near future (< 10 years),
>>>progress in computer-assisted reasoning will make it feasible to produce
>>>strictly formal proofs (that can be checked by very simple theorem
>>>checkers) with a similar investment of effort as is currently the case
>>>for semi-formal reasoning.
>>
>>I find the above delightful.  I've long argued that it's important to place
>>mathematics on a more formal footing by using computers to check proofs.
>>Many people don't seem to appreciate that while it's indeed impossible to
>>develop an algorithm that will prove all possible "true" statements in
>>adequately rich theories (Gödel, etc.), it's still straight forward (if not
>>necessarily simple) to
>>have computer algorithms check the correctness of any proof.  By having
>>computers do such checking it seems to me that we could avoid some
>>problems like the questions about whether quite complex proofs (e.g.
>>for the Four Color Problem, or Fermat's so-called 'last theorem' or others)
>>are correct.
> 
> Actually, precisely this process has recently (2005) been applied by Georges
> Gonthier and Benjamin Werner to one of the proofs of the four colour theorem,
> using the Coq theorem prover:
> 
[...]
>   Georges Gonthier's home page at Microsoft Research, from which the Coq proof
>   can be downloaded: <http://research.microsoft.com/~gonthier/>

BTW, <http://research.microsoft.com/~gonthier/4colnotations.pdf> is worth reading
even if you don't have any background in Coq or the maths necessary to understand
the proof. It seems that a lot of that 2.6 Mbytes is general-purpose libraries,
and to some extent workarounds for current limitations of Coq (for example its
treatment of equality).

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>