Feeds

Proof by self-checking software: the four colour problem

Colouring in maps

  • alert
  • submit to reddit

Secure remote control for conventional and virtual desktops

Computer scientists at Microsoft Research Cambridge (MSRC) have developed a self-checking software-based proof of the four colour theorem that they say sweeps away any remaining uncertainty surrounding earlier proofs.

MRSC researcher Georges Gonthier and Benjamin Werner, a researcher at INRIA, have devised a computer program that verifies the correctness of its own calculations, and applied it to the four colour problem. It constructs a precise mathematical proof and checks that it follows the strict rules of formal logic.

The theorem states that any geographical map may be drawn so that no two contiguous regions are filled in the same colour, provided a palette of four colours is available. It was proven, rather controversially, in 1976. As well as using formal logic, a pair of mathematicians from the University of Illinois, Kenneth Appel and Wolfgang Haken, used a computer to check the tenets of the theorem by brute force.

The controversy arose because the section of the proof that was worked on computer was too long for another mathematician to check. Although most people in the community were prepared to accept the proof, a lingering uncertainty bothered some - what if there had been an error in the software? Gonthier and Werner's work aims to remove that last doubt.

Andrew Herbert, managing director at MSRC said that the discovery had great implications for the future of computing. "Advances we make into self-checking software have the potential to be incorporated into software development tools to make computing in general more reliable and trustworthy," he said.

For more on the history of the Four Colour Theorem, click here. ®

Related stories

Maths boffins secure $750,000 Abel prize
Maths boffins topple Certicom crypto
Computers bad for kids

Secure remote control for conventional and virtual desktops

More from The Register

next story
SCREW YOU, Russia! NASA lobs $6.8bn at Boeing AND SpaceX to run space station taxis
Musk charging nearly half as much as Boeing for crew trips
Boffins say they've got Lithium batteries the wrong way around
Surprises at the nano-scale mean our ideas about how they charge could be all wrong
Thought that last dinosaur was BIG? This one's bloody ENORMOUS
Weighed several adult elephants, contend boffins
Europe prepares to INVADE comet: Rosetta landing site chosen
No word yet on whether backup site is labelled 'K'
India's MOM Mars mission makes final course correction
Mangalyaan probe will feel the burn of orbital insertion on September 24th
Cracked it - Vulture 2 power podule fires servos for 4 HOURS
Pixhawk avionics juice issue sorted, onwards to Spaceport America
City hidden beneath England's Stonehenge had HUMAN ABATTOIR. And a pub
Boozed-up ancients drank beer before tearing corpses apart
'Duck face' selfie in SPAAAACE: Rosetta's snap with bird comet
Probe prepares to make first landing on fast-moving rock
prev story

Whitepapers

Providing a secure and efficient Helpdesk
A single remote control platform for user support is be key to providing an efficient helpdesk. Retain full control over the way in which screen and keystroke data is transmitted.
Saudi Petroleum chooses Tegile storage solution
A storage solution that addresses company growth and performance for business-critical applications of caseware archive and search along with other key operational systems.
Security and trust: The backbone of doing business over the internet
Explores the current state of website security and the contributions Symantec is making to help organizations protect critical data and build trust with customers.
Reg Reader Research: SaaS based Email and Office Productivity Tools
Read this Reg reader report which provides advice and guidance for SMBs towards the use of SaaS based email and Office productivity tools.
Security for virtualized datacentres
Legacy security solutions are inefficient due to the architectural differences between physical and virtual environments.