Science: Where computers prove incapable - Fermat's Last Theorem has been cracked, but Darrel Ince explains how researchers have shown that some problems cannot be solved

Earlier this year, the news came through that Professor Andrew Wiles of Princeton University had succeeded in proving Fermat's Last Theorem - a puzzle that had lain unresolved for three centuries.

Proving mathematical statements to be true (or false) is one of the activities mathematicians indulge in most frequently. Two features of the process often surprise the layman. First, how error-prone the business of proving things is. There are plenty of cases of a seemingly straightforward proof being published, only for it to be modified or even proved false a few months later. The second surprising fact about proofs is that they can be very long. The proof of Fermat's theorem should, in full, occupy hundreds of pages of text.

Now research scientists at the University of California, Stanford University and AT & T laboratories have startled the mathematical world by developing a technique capable of proving - or at least certificating - the correctness of a proof. Of obvious importance to mathematicians, this also has major ramifications for computer scientists.

In effect, the researchers have devised the mathematical version of ultrasonic testing, which highlights any flaws in a proof. A series of operations - transformations - are applied to the text of a proof and any errors become more visible.

There are two implications for computer scientists. The first concerns 'formal methods of software development'. This is the generic term used to describe methods that use mathematics both to draw up the specifications for what a piece of software should achieve and to design the software systems themselves to meet the specifications. Such methods are normally used to develop programs for ultra-reliable applications such as the control of nuclear power stations.

A major problem that has dogged this area is that the proof process is long and error-prone. One incorrect step could lead to a serious error - which could result in loss of life. Use of formal methods has been confined largely to projects where the economic loss due to an error would be so great as to justify employing large numbers of highly trained staff to develop the mathematical specifications and then to check the design and the proofs of the code. The new techniques for the certification of proofs promise to reduce substantially the amount of checking and validation needed.

The second effect of the research concerns a class of computer applications known as NP (non-polynomial)-complete problems. The time taken for a program to solve such a problem increases dramatically depending on its complexity, to the point where it would take longer than the life expectancy of the universe. These are not abstract academic problems, but occur, for example, in the design of telecommunications systems or the layout of computer circuits on silicon chips.

Until recently researchers have believed that although an exact solution to these NP-complete problems has not been possible, approximate ones can be found. An archetypal NP-complete problem might involve devising a layout of roads to connect all the cities in an area using the smallest amount of road material. Computer scientists believed that while an optimal solution would never be possible, there could be approximate solutions that came within 99 per cent of the minimum amount of material.

The research in the US has proved that such programs do not exist for large classes of NP-complete problems - and that such problems will almost certainly be incapable of being computerised. This spin-off alone is being claimed as the major computer science discovery of the past two decades.

The writer is professor of computer science at the Open University.

Start your day with The Independent, sign up for daily news emails
ebooksAn introduction to the ground rules of British democracy
Latest stories from i100
Have you tried new the Independent Digital Edition apps?
Independent Dating

By clicking 'Search' you
are agreeing to our
Terms of Use.

iJobs Job Widget
iJobs General

Recruitment Genius: Web Developer - Junior / Mid Weight

£15000 - £25000 per annum: Recruitment Genius: To support their continued grow...

Recruitment Genius: Marketing Data Specialist

£22000 - £25000 per annum: Recruitment Genius: They are the go-to company for ...

Recruitment Genius: Search Marketing Specialist - PPC / SEO

Negotiable: Recruitment Genius: This is an opportunity to join the UK's leadin...

Recruitment Genius: Sales Administrator

Negotiable: Recruitment Genius: This caravan dealership are currently recruiti...

Day In a Page

Greece debt crisis: What happened to democracy when it’s a case of 'Vote Yes or else'?

'The economic collapse has happened. What is at risk now is democracy...'

If it doesn’t work in Europe, how is it supposed to work in India or the Middle East, asks Robert Fisk
The science of swearing: What lies behind the use of four-letter words?

The science of swearing

What lies behind the use of four-letter words?
The Real Stories of Migrant Britain: Clive fled from Zimbabwe - now it won't have him back

The Real Stories of Migrant Britain

Clive fled from Zimbabwe - now it won’t have him back
Africa on the menu: Three foodie friends want to popularise dishes from the continent

Africa on the menu

Three foodie friends want to popularise dishes from the hot new continent
Donna Karan is stepping down after 30 years - so who will fill the DKNY creator's boots?

Who will fill Donna Karan's boots?

The designer is stepping down as Chief Designer of DKNY after 30 years. Alexander Fury looks back at the career of 'America's Chanel'
10 best statement lightbulbs

10 best statement lightbulbs

Dare to bare with some out-of-the-ordinary illumination
Wimbledon 2015: Heather Watson - 'I had Serena's poster on my wall – now I'm playing her'

Heather Watson: 'I had Serena's poster on my wall – now I'm playing her'

Briton pumped up for dream meeting with world No 1
Wimbledon 2015: Nick Bollettieri - It's time for big John Isner to produce the goods to go with his thumping serve

Nick Bollettieri's Wimbledon Files

It's time for big John Isner to produce the goods to go with his thumping serve
Dustin Brown: Who is the tennis player who knocked Rafael Nadal out of Wimbeldon 2015?

Dustin Brown

Who is the German player that knocked Nadal out of Wimbeldon 2015?
Ashes 2015: Damien Martyn - 'England are fired up again, just like in 2005...'

Damien Martyn: 'England are fired up again, just like in 2005...'

Australian veteran of that Ashes series, believes the hosts' may become unstoppable if they win the first Test
Tour de France 2015: Twins Simon and Adam Yates have a mountain to climb during Tour of duty

Twins have a mountain to climb during Tour of duty

Yates brothers will target the steepest sections in bid to win a stage in France
John Palmer: 'Goldfinger' of British crime was murdered, say police

Murder of the Brink’s-MAT mastermind

'Goldfinger' of British crime's life ended in a blaze of bullets, say police
Forget little green men - aliens will look like humans, says Cambridge University evolution expert

Forget little green men

Leading evolutionary biologist says aliens will look like humans
The Real Stories of Migrant Britain: An Algerian scientist adjusts to life working in a kebab shop

The Real Stories of Migrant Britain

An Algerian scientist struggles to adjust to her new life working in a Scottish kebab shop
Bodyworlds museum: Dr Gunther von Hagens has battled legal threats, Parkinson's disease, and the threat of bankruptcy

Dying dream of Doctor Death

Dr Gunther von Hagens has battled legal threats, Parkinson's disease, and the threat of bankruptcy