Feeds

Proof by self-checking software: the four colour problem

Colouring in maps

  • alert
  • submit to reddit

The Power of One Infographic

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

Eight steps to building an HP BladeSystem

More from The Register

next story
Malaysian Airlines flight MH17 claimed lives of HIV/AIDS cure scientists
Researchers, advocates, health workers among those on shot-down plane
The Sun took a day off last week and made NO sunspots
Someone needs to get that lazy star cooking again before things get cold around here
Mwa-ha-ha-ha! Eccentric billionaire Musk gets his PRIVATE SPACEPORT
In the Lone Star State, perhaps appropriately enough
MARS NEEDS OCEANS to support life - and so do exoplanets
Just being in the Goldilocks zone doesn't mean there'll be anyone to eat the porridge
Diary note: Pluto's close-up is a year from … now!
New Horizons is less than a year from the dwarf planet
Forty-five years ago: FOOTPRINTS FOUND ON MOON
NASA won't be back any time soon, sadly
prev story

Whitepapers

Reducing security risks from open source software
Follow a few strategies and your organization can gain the full benefits of open source and the cloud without compromising the security of your applications.
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.
Application security programs and practises
Follow a few strategies and your organization can gain the full benefits of open source and the cloud without compromising the security of your applications.
Boost IT visibility and business value
How building a great service catalog relieves pressure points and demonstrates the value of IT service management.
Consolidation: the foundation for IT and business transformation
In this whitepaper learn how effective consolidation of IT and business resources can enable multiple, meaningful business benefits.