Proof assistants are computer programs designed to verify the accuracy and the logic of formal mathematical proofs. Though we never see them, these proofs provide the basis for much of the math underlying the operations of our daily lives. Increasingly, as these proofs become too long or complex to be checked by people, their verification is being turned over to machines. Despite concerns about bugs entering the system, proof assistants are creating new possibilities for mathematicians to collaborate and advance even faster.
(Flickr / Ian Ruotsala)
If you took high school geometry, you may remember doing proofs, detailing the step-by-step logic that would lead you to the desired mathematical conclusion. These outlines involved multiple steps, which your teacher would check for technical and logical accuracy. Imagine that today you’re a mathematician and your job is to produce high-level proofs that can run to 40,000 lines. Who’s going to check your work now? As no human would be up to the task, computers are being used more and more frequently in this role, raising questions about how confident we can be in their results. Though some don’t like the idea of turning the verification step over to machines, computer-assisted proofs are making more things possible in math—to the point that the Institut Henri Poincaré (IHP) in Paris is devoting its next quarterly series to the subject, starting next Tuesday, April 22.
The intermingling of math and computer science is not surprising. At a press event held at CNRS headquarters on April 3, a handful of mathematicians and computer scientists discussed this relationship. Cédric Villani, France’s famous face of mathematics and director of the IHP, sees computer science as a branch of math that has become autonomous—if not a heresy, he joked. “Computer science is a sort of a lab for mathematics, a place to experiment. Think of any technology or technique; these things emerge from computer science.”
The concept of formal proofs of mathematical concepts was developed in the 1930s by logicians like Alan Turing to better understand the nature of the reasoning used to arrive at mathematical truths and ensure the absence of errors. Forty years later, the Curry-Howard correspondence emerged, showing that a logical proof is built on the same skeleton as a computer program.
Today, computers are, of course, used all the time in math, but more for experimentation than for proofs. For some mathematicians, it’s impossible to have confidence in a verification step that, in a sense, has been taken out of human hands. For instance, the Kepler conjecture, first stated in the 17th century by the astronomer of the same name, was at last, more or less, proved by Thomas Hales in 1998. However, the fact that his proof depends in part on complex computer calculations originally led to criticism, as no authority could check it. But, in fact, as Georges Gonthier, a researcher with Microsoft Research known for his computer-assisted proof of the four color theorem, points out, the proof that a mathematician publishes isn’t truly complete anyway; it details only the basic method followed. Furthermore, while traditionalists can’t believe a computer-assisted proof that required two months of work by a computing center and whose results can’t realistically be replicated, others with a more modern mindset say that part of any proof might rely on 2,000 pages of diagrams that couldn’t possibly be error-free anyway.
Above and beyond this shared potential to harbor errors is the promise held by the use of computers to carry out proofs. Already, computer-assisted proofs have industrial applications in nuclear power plants, for instance, and are involved in more everyday concerns like banking. Hugo Herbelin, a researcher with INRIA who manages the development of the proof assistant software Coq, explained that they are used to check the protocols governing money transfers, making sure that such a transaction doesn’t happen twice, for example. “This is not about security, really, but it’s essential for the functioning of society.”
In the world of mathematics, Paul-André Melliès of the CNRS and the University of Paris-Diderot feels that computer-assisted proofs are making international collaborations possible, which means making progress faster. “You no longer need the single world expert watching over everything and declaring the work is all ok.” Today, each group on a project develops its part of a theorem, and the individual pieces of software are verified independently before being combined. This makes it easier to check that they all work together and allows the system to maintain its intellectual flexibility. Not to mention, Melliès points out, on a very practical level, if a subject in mathematics gets old, there simply may not be an authority on the topic anymore. In this case, computers can step in, allowing all the elements to still be checked.
To learn more about the intersection of math, computer science and logic found in computer-assisted proofs, visit the Institut Henri Poincaré as it launches a 3-month series dedicated to “Semantics of proofs and certified mathematics”.