Feeds

Proof by self-checking software: the four colour problem

Colouring in maps

  • alert
  • submit to reddit

Build a business case: developing custom apps

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

The Essential Guide to IT Transformation

More from The Register

next story
Just TWO climate committee MPs contradict IPCC: The two with SCIENCE degrees
'Greenhouse effect is real, but as for the rest of it ...'
Asteroid's DINO KILLING SPREE just bad luck – boffins
Sauricide WASN'T inevitable, reckon scientists
Flamewars in SPAAACE: cooler fires hint at energy efficiency
Experiment aboard ISS shows we should all chill out for cleaner engines
Boffins discuss AI space program at hush-hush IARPA confab
IBM, MIT, plenty of others invited to fill Uncle Sam's spy toolchest, but where's Google?
NASA Mars rover FINALLY equals 1973 Soviet benchmark
Yet to surpass ancient Greek one, however
Famous 'Dish' radio telescope to be emptied in budget crisis: CSIRO
Radio astronomy suffering to protect Square Kilometre Array
BEST BATTERY EVER: All lithium, all the time, plus a dash of carbon nano-stuff
We have found the Holy Grail (of batteries) - boffins
prev story

Whitepapers

Implementing global e-invoicing with guaranteed legal certainty
Explaining the role local tax compliance plays in successful supply chain management and e-business and how leading global brands are addressing this.
Consolidation: The Foundation for IT Business Transformation
In this whitepaper learn how effective consolidation of IT and business resources can enable multiple, meaningful business benefits.
Backing up Big Data
Solving backup challenges and “protect everything from everywhere,” as we move into the era of big data management and the adoption of BYOD.
Boost IT visibility and business value
How building a great service catalog relieves pressure points and demonstrates the value of IT service management.
Why and how to choose the right cloud vendor
The benefits of cloud-based storage in your processes. Eliminate onsite, disk-based backup and archiving in favor of cloud-based data protection.