Computer generates verifiable mathematics proof
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."
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."
Google for Related Stuff:
posted by sikandar at 11:28 AM
0 Comments:
Post a Comment
<< Home