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

Top 5 reasons to deploy VMware with Tegile

More from The Register

next story
Bond villains lament as Wicked Lasers withdraw death ray
Want to arm that shark? Better get in there quick
Antarctic ice THICKER than first feared – penguin-bot boffins
Robo-sub scans freezing waters, rocks warming models
Your PHONE is slowly KILLING YOU
Doctors find new Digitillnesses - 'text neck' and 'telepressure'
SEX BEAST SEALS may be egging each other on to ATTACK PENGUINS
Boffin: 'I think the behaviour is increasing in frequency'
Reuse the Force, Luke: SpaceX's Elon Musk reveals X-WING designs
And a floating carrier for recyclable rockets
The next big thing in medical science: POO TRANSPLANTS
Your brother's gonna die, kid, unless we can give him your, well ...
NASA launches new climate model at SC14
75 days of supercomputing later ...
Renewable energy 'simply WON'T WORK': Top Google engineers
Windmills, solar, tidal - all a 'false hope', say Stanford PhDs
Britain's HUMAN DNA-strewing Moon mission rakes in £200k
3 days, and Kickstarter moves lander 37% nearer takeoff
prev story

Whitepapers

Why cloud backup?
Combining the latest advancements in disk-based backup with secure, integrated, cloud technologies offer organizations fast and assured recovery of their critical enterprise data.
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.
Designing and building an open ITOA architecture
Learn about a new IT data taxonomy defined by the four data sources of IT visibility: wire, machine, agent, and synthetic data sets.
How to determine if cloud backup is right for your servers
Two key factors, technical feasibility and TCO economics, that backup and IT operations managers should consider when assessing cloud backup.
High Performance for All
While HPC is not new, it has traditionally been seen as a specialist area – is it now geared up to meet more mainstream requirements?