August 7, 2018, 7:23 pm
Machine-assisted proofs have come a long way and offer tremendous potential for the future of mathematics, a panel of academics said this afternoon at the 2018 International Congress of Mathematicians.
Thought to have first been used in the late 1970s, computer-assisted proofs provide mathematicians with a way to check and test their theorems which is far more rapid than traditional methods, which often involve pencil, paper and a long stretch of time. Computers allow mathematicians to verify if their theorems are correct in a far shorter amount of time.
Read more:
“One thing that’s changed recently is the availability of cloud services,” said Bjorn Poonen, an MIT math professor and a four-time winner of the Putnam Competition amongst other awards. “My colleague Andrew Sutherland did a computation that would take roughly 300 years in three hours because he was basically using lots of computers at the same time. It can really change what you choose to investigate if you know you have that level of computing possibility.”
James Maynard, a research professor at Oxford who has won the Whitehead Prize and the much-coveted European Mathematical Society Prize in recent years, says that computer-assisted proofs have enormous potential to improve what mathematicians are able to do. “We’re very fortunate that we have the possibility of going through a huge number of calculations, many more than we could go through by hand,” he said.
Machine assisted proofs are also coming to be essential for academic journals to carry out their own refereeing processes before publishing articles. But, there are challenges. How do different academic groups and institutions arrive at a conclusion as to which machine assisted proofing systems are trustworthy.
Luís Cruz-Filipe provided further evidence for both the benefits and challenges facing machine-assisted learning. “There’s been a shift in what we consider the style of computer proofing, from ad hoc proofs where we need to trust the program to theorem proven [methods],” said the mathematics professor at Rutgers, Pham Huu Tiep and University of Southern Denmark
Harald Andres Helfgott, the current Humboldt Professor at the University of Göttingen (in addition to being the recipient of the Whitehead Prize, the Leverhulme Prize and the Adams Prize), agreed with the benefits of the technology, but voiced concerns regarding its challenges. He said that going forward, it’s important to define what rigorous computing is, look at the probability of computing errors and ways to reduce their occurrence, and whether computers can also be used to check proofing errors for machine assisted proofing systems.