[Paleopsych] NS: Computer generates verifiable mathematics proof

[Premise Checker]

These were left over from yesterday. Quite a trove from New Scientist. 
More later today. I hope you find these worthwhile and are not 
overburdened.

Frank

Computer generates verifiable mathematics proof
http://www.newscientist.com/article.ns?id=dn7286&print=true
      * 18:27 19 April 2005
      * Will Knight

    A computer-assisted proof of a 150-year-old mathematical conjecture
    can at last be checked by human mathematicians.

    The Four Colour Theorem, proposed by Francis Guthrie in 1852, states
    that any four colours are the minimum needed to fill in a flat map
    without any two regions of the same colour touching.

    A proof of the theorem was announced by two US mathematicians, Kenneth
    Appel and Wolfgang Haken, in 1976. But a crucial portion of their work
    involved checking many thousands of maps - a task that can only
    feasibly be done using a computer. So a long-standing concern has been
    that some hidden flaw in the computer code they used might undermine
    the overall logic of the proof.

    But now Georges Gonthier, at Microsoft's research laboratory in
    Cambridge, UK, and Benjamin Werner at INRIA in France have proven the
    theorem in a way that should remove such concerns.

    They translated the proof into a language used to represent logical
    propositions - called Coq - and created logic-checking software to
    confirm that the steps put forward in the proof make sense.

    "It is a landmark," says Randy Pollack, from Edinburgh University in
    Scotland, who wrote one of the first logic-checking programs using
    Coq. "Mainly because it is such well known theorem and because there
    was such a row in 1976."

Changing thought patterns

    Pollack says many other computer-assisted proofs could be made more
    credible using the approach. But he notes that it could take years to
    adapt very complicated proofs in this way. And he says those which
    require extremely intensive computation might take far too long to
    check logically.

    Gonthier says more mathematicians will be encouraged to use computers
    if they know they can demonstrate the logic behind their calculations.
    And he suggests this could eventually change the way many
    mathematicians think.

    "I've found instances where I'm doing things in a completely different
    way simply because I'm using a computer," he told New Scientist.

    But the research could also have an impact beyond mathematics.
    Microsoft hopes to develop a similar system for checking the logic
    used in computer programs, which could pre-empt some unforeseen bugs
    that cause programs to crash.

    "The discovery has great implications for the future of computing,"
    says Andrew Herbert, managing director at Microsoft Research
    Cambridge. "Advances we make into self-checking software have the
    potential be incorporated into software development tools to make
    computing in general more reliable and trustworthy."

Related Articles

      * [12]Taming the fourth dimension
      * [13]http://www.newscientist.com/article.ns?id=mg18324565.000
      * 17 July 2004
      * [14]Primal dream
      * [15]http://www.newscientist.com/article.ns?id=mg18024225.500
      * 22 November 2003
      * [16]Mathematics unravels optimum way of shoe lacing
      * [17]http://www.newscientist.com/article.ns?id=dn3136
      * 04 December 2002

Weblinks

      * [18]Microsoft Research Cambridge
      * [19]http://research.microsoft.com/aboutmsr/labs/cambridge/default.
        aspx
      * [20]INRIA
      * [21]http://www.inria.fr/index.en.html
      * [22]Laboratory for Foundations of Computer Science, Edinburgh
        University
      * [23]http://www.lfcs.inf.ed.ac.uk/index.html
      * [24]Coq
      * [25]http://pauillac.inria.fr/coq/

References

   12. http://www.newscientist.com/article.ns?id=mg18324565.000
   13. http://www.newscientist.com/article.ns?id=mg18324565.000
   14. http://www.newscientist.com/article.ns?id=mg18024225.500
   15. http://www.newscientist.com/article.ns?id=mg18024225.500
   16. http://www.newscientist.com/article.ns?id=dn3136
   17. http://www.newscientist.com/article.ns?id=dn3136
   18. http://research.microsoft.com/aboutmsr/labs/cambridge/default.aspx
   19. http://research.microsoft.com/aboutmsr/labs/cambridge/default.aspx
   20. http://www.inria.fr/index.en.html
   21. http://www.inria.fr/index.en.html
   22. http://www.lfcs.inf.ed.ac.uk/index.html
   23. http://www.lfcs.inf.ed.ac.uk/index.html
   24. http://pauillac.inria.fr/coq/
   25. http://pauillac.inria.fr/coq/

E-mail me if you have problems getting the referenced articles.