Computers have transformed a broad range of human activities, from sales to basic research. Now, for an enthusiastic contingent of mathematicians and computer scientists, they are poised to deliver on a long-standing promise to do the same for mathematics.
The renewed excitement grows from discoveries that expand the scope of computer-assisted proofs of theorems, but also provide a new and more intuitive way of grounding new results to the bedrock foundations of mathematics, even as those results grow more complex. Tools based on these developments could help establish a growing library of certified results backed by computer verification. Along the way, it could change the culture of mathematics by making it easier for individuals to dependably add to this growing edifice.
The most prominent face of the new movement is Vladimir Voevodsky, at the School of Mathematics of the storied Institute for Advanced Study (IAS) in Princeton, NJ. In 2002, Voevodsky shared the International Math Union’s Fields Medal which, together with the Abel Prize, are often called the mathematics equivalent of the Nobel Prize. In recent years, he has turned his attention to exploring how computers can enhance mathematics research.
In the process, Voevodsky has inspired a high-powered group of mathematicians and computer scientists to explore the implications of the new framework. Over the 20122013 academic year, several dozen of them assembled at IAS to work towards this goal.
"It was really thrilling," said co-organizer Steve Awodey of Carnegie Mellon University in Pittsburgh, PA. "You felt like you were part of the Manhattan Project of computer science. Everybody had the feeling they were part of something important, and I think they were. I think we really made some amazing progress there, the consequences of which are going to take time now to play out."
In part to build on this momentum, some 25 of the researchers wrote a 600-page textbook (available free online at http://homotopytypetheory.org/book/) describing the new view, called Homotopy Type Theory (HoTT) for reasons discussed later. The book was prepared collaboratively over just a few months, as illustrated in the time-lapse video available at http://vimeo.com/68761218, sharing and editing documents using the GitHub version-control platform originally designed for code development.
This collaborative authorship is an intriguingly parallel to the group’s vision of a reliable and consistent encapsulation of a body of mathematical knowledge, analogous to a library of trusted subroutines in a computer program. This vision is an old one: more than a century ago, mathematicians strove to formalize all mathematics, and trace it all back to a few axioms. That goal ran into trouble when it was proved that, for any formal system, it is impossible to prove all theorems about that system. As a result, "working mathematicians decided that foundations are irrelevant for their purposes," says Awodey. Moreover, there was no particular payoff for tracing everyday work back to first principles. Although the new framework does not avoid these problems, Awodey said, it doesn’t much matter. "This system of foundations has a much more practical aspect; it is closer to the way mathematicians reason."
"This system of foundations has a much more practical aspect; it is closer to the way mathematicians reason."
The system could also enhance cooperation between mathematicians. If computer-verified proofs become mainstream, Voevodsky says, "it will eventually lead us to a possibility of big, collaborative projects." If the computer can guarantee that a particular result is correct, others can build on it with confidence, even if it comes from an unknown or novice researcher, or an expert who is importing novel ideas into a different subfield.
Voevodsky stresses that human ingenuity will always be important. "It’s not like someone who doesn’t know anything in mathematics can just use this library and start producing great mathematics on top of it. One still has to have the internal [mental] representation of what’s going on there."
Another advantage of a computer library of mathematics, says IAS participant Andrej Bauer of the University of Ljubljana, Slovenia, would be the ability to search for relevant results. Even if the new framework lives up to its promise, he cautions, "ultimately, it is not just the math; it is the question of how new mathematical ideas get adopted by the wider community of mathematicians."
Indeed, for a century, mathematicians have considered set theory to be an adequate basis for formalizing all of mathematics. Starting with concepts like the null set (corresponding to zero) and the set containing only the null set (corresponding to one), one can, in principle, systematically construct all the objects of mathematics. In practice, however, the process is clunky and time-consuming—and therefore, rare. The proponents of HoTT hope it will provide easier and more intuitive tools that will allow rigorously formalized mathematics to become standard practice.
HoTT is based on a mathematical framework called type theory. Unlike sets, which are like bags that can contain various kinds of object, objects of a particular type have specific rules about how they can be manipulated. They are reminiscent of the data types that help enforce rigor in high-level programming languages, but the mathematical version of types can be more elaborate; for example, an n-dimensional vector whose precise character depends on a natural number n that must be computed.
A version of type theory is used in most versions of automated "proof assistants," which have been growing in power since their introduction in the 1960s but are still not widely used in pure mathematics. This framework expands the notion of types so that, for example, the formulation of a theorem can itself be a type, and a proof of the theorem can be an object of that type; thus, if such an object even exists, the theorem is proved. These exotic types can even ensure that no logical cases are overlooked.
One of the best-known successes was the formal proof of the four-color map theorem in 2005 by Georges Gonthier of Microsoft Research in Cambridge, UK. (The earlier 1976 proof by Kenneth Appel and Wolfgang Haken of the University of Illinois at Urbana-Champaign had combined computer code for some parts with text arguments for others.) Gonthier used the proof assistant Coq, which in 2013 won the Programming Languages Software Award of the ACM Special Interest Group on Programming Languages (SIGPLAN).
This Coq flavor of type theory has good computational properties, in particular a feature called decidability of equality. This means there is an algorithm to determine whether any two objects are equal, which is a key step in its use for proofs. Yet Thierry Coquand of the University of Gothenburg, Sweden, who was one of the developers of Coq, noted "there was always something missing" in the notion of equality in this type theory. "The concept of equal is better" in HoTT, he said. "Hopefully, it will lead to practical things."
A version of type theory is used in most versions of automated "proof assistants," which were introduced in the 1960s but are still not widely used in pure mathematics.
The new view of equality arises from the realization, arrived at independently by Voevodsky and by Awodey and his student Michael Warren, of a connection between completely different branches of mathematics. To give a more familiar example, the ancient understanding of circles, ellipses, hyperbolas, and parabolas as cross-sections is enriched and complemented by their description by algebraic equations. In a particular situation, one description or the other may be more useful, but their combination can lead to new insights and perhaps a glimpse of a larger reality. "This happens in mathematics over and over again," says Bauer. "We’re discovering a new connection, and this new connection is now influencing both sides of the connection."
Similarly, homotopy type theory represents a connection between type theory and homotopy theory, which is a branch of topology. In the homotopy view, the types (which can be theorems) are envisioned as spaces, and the objects of that type (which can be proofs) are points in the space. The equality of two points can then be thought of as the existence of a path in the space connecting the two points. This connection allows a host of tools from homotopy theory to be applied the task of mathematical proof.
At a minimum, HoTT extends the domain of proof assistant to new areas of mathematics. "Coq was designed by computer scientists, so its initial area of application was basically programming language theory and combinatorics," Gonthier noted. Many papers presented at SIGPLAN’s Principles of Programming Languages (POPL) symposium are backed by computer proofs, but this kind of problem "isn’t all of mathematics," he says, and applying it to other areas "is quite important and interesting."
Beyond applying logical reasoning, for example, to topological problems, Gonthier says, "the correspondence can be used in the reverse way, to try to deduce something about the logical system based on insights that have been developed for, basically, topology."
"It’s definitely expanding our notion of what a proof can mean, because it’s explaining proofs in a geometric way," says Bauer. "We know it’s going to bring us something new, but time will tell what."
"Formalization of mathematics is somehow too compelling and effective to go away," said Awodey. "It’s going to happen. It’s just a question of when and using what system," whether HoTT or something else.
Further Reading
The Univalent Foundations Program, Institute for Advanced Study
"Homotopy Type Theory: Univalent Foundations of Mathematics" (Princeton, 2013) available for download or purchase at http://homotopytypetheory.org/book/.
Georges Gonthier
"Formal Proof—The Four-Color Theorem", Notices of the American Mathematical Society 55 (11): 13821393 (2008).
Thomas Hales
"Mathematics in the Age of the Turing Machine", to be published in Turing’s Legacy: Developments from Turing’s Ideas in Logic (Lecture Notes in Logic), ed. R. Downey, (Cambridge University Press, 2014)
Join the Discussion (0)
Become a Member or Sign In to Post a Comment