Finally, the 10 billion-year mathematical brain teaser has been solved
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.
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 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.
What was the problem?
What mathematician Ronald Graham could not come up with an answer for was this: Is it possible to colour each positive integer either red or blue in such a way that no triple of the integers, a, b, and c, that satisfies Pythagoras' popular relationship, a2+b2=c2, would have the same colour? Graham promised a prize of $100 to the person who could solve the problem, dubbed Boolean Pythagorean Triples Problem.
Supercomputer ABACUS 2.0
Abacus 2.0 is able to perform 766 trillion operations per second. Current applications cover advanced modeling and simulations in chemistry, material science, biophysics, high-energy physics, engineering, computational medicine, archaeology as well as scientific data visualization.
Professor Peter Schneider-Kamp, Department of Mathematics and Computer Science. firstname.lastname@example.org. Tel +45 6550 2327.
Improves confidence in everyday computers
Computers pervade our everyday life and it is important for us to be able to depend on them working reliably. They are in charge of, for example, delivering petrol to your car’s engine, securing the transfer of data on the Internet, letting us withdraw money, ensuring that pharmacists to give out the proper medications, allowing airplanes to maintain the proper altitude, and support doctors in obtaining the proper diagnosis, etc. According to Professor Peter Schneider-Kamp, the new work will contribute to enhancing our confidence in these systems.