Feeds

Proof by self-checking software: the four colour problem

Colouring in maps

  • alert
  • submit to reddit

Choosing a cloud hosting partner with confidence

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
GRAV WAVE DRAMA: 'Big Bang echo' may have been grit on the scanner – boffins
Exit Planet Dust on faster-than-light expansion of universe
Mine Bitcoins with PENCIL and PAPER
Forget Sudoku, crunch SHA-256 algos
SpaceX Dragon cargo truck flies 3D printer to ISS: Clawdown in 3, 2...
Craft berths at space station with supplies, experiments, toys
'This BITE MARK is a SMOKING GUN': Boffins probe ancient assault
Tooth embedded in thigh bone may tell who pulled the trigger
DOLPHINS SMELL MAGNETS – did we hear that right, boffins?
Xavier's School for Gifted Magnetotaceans
Big dinosaur wowed females with its ENORMOUS HOOTER
That's right, Doris, I've got biggest snout in the prehistoric world
Japanese volcano eruption reportedly leaves 31 people presumed dead
Hopes fade of finding survivors on Mount Ontake
That glass of water you just drank? It was OLDER than the SUN
One MEELLION years older. Some of it anyway
Canberra drone team dances a samba in Outback Challenge
CSIRO's 'missing bushwalker' found and watered
prev story

Whitepapers

Forging a new future with identity relationship management
Learn about ForgeRock's next generation IRM platform and how it is designed to empower CEOS's and enterprises to engage with consumers.
Storage capacity and performance optimization at Mizuno USA
Mizuno USA turn to Tegile storage technology to solve both their SAN and backup issues.
The next step in data security
With recent increased privacy concerns and computers becoming more powerful, the chance of hackers being able to crack smaller-sized RSA keys increases.
Security for virtualized datacentres
Legacy security solutions are inefficient due to the architectural differences between physical and virtual environments.
A strategic approach to identity relationship management
ForgeRock commissioned Forrester to evaluate companies’ IAM practices and requirements when it comes to customer-facing scenarios versus employee-facing ones.