Will computers ever be able to do mathematical research? Automatic computers have amazing power to analyze huge data bases and carry out extensive searches far beyond human capabilities. They can assist mathematicians in checking cases and evaluating functions at lightning speed, and they have been essential in producing proofs that depend on exhaustive searches.
The That’s Maths column in this week’s Irish Times ( TM014 ) is about the use of computers for proving mathematical theorems, and also for simulating physical systems.
Astronomy was revolutionized with the invention of the telescope, and biology with the microscope. In a similar manner, computers allow mathematicians to perform analyses and computations that were previously impracticable. High-power computing has resulted in an active field called experimental mathematics, in which computation is used to study mathematical objects and to recognize patterns.
A computer-assisted proof is a mathematical proof generated, in whole or in part, by a computer. The proof of the four-colour theorem, which states that four colours suffice to colour any map with neighbouring regions having distinct colours, is a notable example of a result that could not have been proven without computer assistance.
Automatic Theorem Proving (ATP) is a developing branch of computer science. With the blistering pace of technological advances, the goal of generating proofs using computers looks increasingly realistic. In 1950, the early computer called ENIAC (Electronic Numerical Integrator and Computer) was five orders of magnitude faster than a human: that is, it could calculate as fast as one hundred thousand people.
Today, supercomputer speeds are measured in Petaflops – one thousand million million calculations per second. That is five orders of magnitude faster than Earth’s entire human population. These supercomputers can do in one hour what would take ten billion people, calculating day and night, about ten years.
ICHEC & PRACE
The Irish Centre for High-End Computing (www.ichec.ie) is Ireland’s national high-performance computer service-provider. Many researchers in Irish academic institutions are benefiting from computational time at ICHEC, producing significant scientific breakthroughs and articles in leading journals. In addition, Met Eireann’s weather forecasts are run on ICHEC computers.
But some research requires computer power greater than anything available in Ireland. ICHEC is a member of PRACE, the Partnership for Advanced Computing in Europe (www.prace-ri.eu), and Irish researchers are gaining benefits from PRACE through access to Europe’s fastest computers. This is enabling them to carry out world-class science and engineering research.
Although computer proofs are scorned by some mathematicians, it seems to me that computers will ultimately be better than humans at generating and solving mathematics problems. Progress in Automatic Theorem Proving software over recent decades has been impressive.
But although mathematics comprises drawing logical conclusions from stated axioms, which can be mechanised, aesthetics plays a central, and indeed essential, role. Mathematicians are motivated by curiosity, and seek results that are interesting, elegant and beautiful. How will computers do this? Watch this space!