If there were no computers, this task would have required 10 billion years of a mathematician’s waking time. Luckily, however, there is a supercomputer at SDU and the task is therefore solved. The results have significance for our confidence in all the large and small electronic devices which control our everyday lives.
By Birgitte Svennevig, birs@sdu.dk
Earlier this year, a research team from the University of Texas in Austin proudly announced that they had succeeded in solving a mathematical problem that had been open in the field for more than 30 years.
The researchers had applied the supercomputer, Stampede, from the Texas Advanced Computing Centre, to the problem – but when the computer output its result, they were left with a new problem: They were unable to check the resulting proof mathematically. It was simply too big.
Furthermore, since almost all computer programs contain errors to a greater or lesser degree – something we have all experienced in our daily lives – it would have been too uncertain to rely on Stampede’s calculation.
Reading 1,800 million e-books
The Texas researchers therefore immediately launched a request for a mathematical verification of the resulting mathematical proof (which, by the way, took up 200 terabytes of data, corresponding to approx. 1,800 million e-books).
– This is the biggest mathematical proof ever, and to verify such a large proof would require an enormous effort. It would require 10 billion years of concentrated reading to go through it searching for whatever errors that were present, explains Peter Schneider-Kamp, Professor at the Department of Mathematics and Computer Science at SDU.
Together with his colleague Luís Cruz-Filipe, also from SDU, and Professor Joao Marques-Silva from the University of Lisbon, he decided to make an attempt regardless – with help from the National Danish High Performance Computing centre’s supercomputer, ABACUS 2.0. Find the results here.
Bring down the time, please
– We trained ABACUS to be an army of 448 artificial mathematicians, each with a very high level of efficiency. Thus we were able to reduce the task to a few days of work instead of 10 billion years!
The SDU researchers did NOT recreate the proof independently, but instead, they created a program, which is “correct by construction”, since it was made based on a formalization of the mathematical theory behind the proof.
– It is therefore guaranteed that our program does not contain any bugs, and when it had gone through all 200 TB of the proof, it is also guaranteed that the Texas proof is correct, mathematically speaking.
Huge implications for the safety and security of computer systems
In other words: The Texas proposal for a solution of the mathematical problem is sufficiently correct.
– I am excited that Luís, Peter, and Joao were able to validate the ’largest math proof ever’ with a formally verified checker written in Coq. Their results show that theorem proving is now capable of dealing with huge files and doing so efficiently. This significantly increases the trust in the correctness of the results”, concludes Marijn Heule from the University of Texas, who was involved in solving the mathematical problem.
– The most significant part, however, is not so much that we have validated the results of other researchers. The important point here is that we have demonstrated that large-scale computer calculations can be verified mathematically and we can use this to strengthen our confidence in all the computers that control our everyday lives. If we can prove mathematically that a hard- or software system is working correctly, then we can have a greater level of confidence in the relevant hard- or software devices. Furthermore, I personally feel that that is very comforting, should I decide, for example, to take a ride in a self-driving car or fly in an airplane controlled by an autopilot software, states Peter Schneider-Kamp.
For more information see:
http://www.sdu.dk/en/om_sdu/fakulteterne/naturvidenskab/aktuelt/2016_11_…
