Feeds

Proof by self-checking software: the four colour problem

Colouring in maps

  • alert
  • submit to reddit

Top three mobile application threats

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

High performance access to file storage

More from The Register

next story
Most Americans doubt Big Bang, not too sure about evolution, climate change – survey
Science no match for religion, politics, business interests
KILLER SPONGES menacing California coastline
Surfers are safe, crustaceans less so
Discovery time for 200m WONDER MATERIALS shaved from 4 MILLENNIA... to 4 years
Alloy, Alloy: Boffins in speed-classification breakthrough
LOHAN and the amazing technicolor spaceplane
Our Vulture 2 livery is wrapped, and it's les noix du mutt
Liftoff! SpaceX Falcon 9 lifts Dragon on third resupply mission to ISS
SpaceX snaps smartly into one-second launch window
R.I.P. LADEE: Probe smashes into lunar surface at 3,600mph
Swan dive signs off successful science mission
Opportunity selfie: Martian winds have given the spunky ol' rover a spring cleaning
Power levels up 70 per cent as the rover keeps on truckin'
Elon Musk's LEAKY THRUSTER gas stalls Space Station supply run
Helium seeps from Falcon 9 first stage, delays new legs for NASA robonaut
prev story

Whitepapers

Mainstay ROI - Does application security pay?
In this whitepaper learn how you and your enterprise might benefit from better software security.
Combat fraud and increase customer satisfaction
Based on their experience using HP ArcSight Enterprise Security Manager for IT security operations, Finansbank moved to HP ArcSight ESM for fraud management.
The benefits of software based PBX
Why you should break free from your proprietary PBX and how to leverage your existing server hardware.
Top three mobile application threats
Learn about three of the top mobile application security threats facing businesses today and recommendations on how to mitigate the risk.
3 Big data security analytics techniques
Applying these Big Data security analytics techniques can help you make your business safer by detecting attacks early, before significant damage is done.