[Paleopsych] NS: Computer generates verifiable mathematics proof
checker at panix.com
Sat Apr 23 09:05:15 UTC 2005
These were left over from yesterday. Quite a trove from New Scientist.
More later today. I hope you find these worthwhile and are not
Computer generates verifiable mathematics proof
* 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
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
"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."
* Taming the fourth dimension
* 17 July 2004
* Primal dream
* 22 November 2003
* Mathematics unravels optimum way of shoe lacing
* 04 December 2002
* Microsoft Research Cambridge
* Laboratory for Foundations of Computer Science, Edinburgh
E-mail me if you have problems getting the referenced articles.
More information about the paleopsych