A new foundation for mathematics

Is there a revolution coming along in mathematics? A shift that will fundamentally change the way in which mathematicians work? In the near future, will computers rather than humans reliably verify whether a mathematical proof is correct?

According to the blogger Julie Rehmeyer the Russian mathematician Vladimir Voevodsky (*1966) has developed an approach that could indeed revolutionise mathematics and its foundations: He has been able to show in principle that homotopy theory, which deals with the deformation of geometric objects, expresses the same ideas as the theory of programming languages and mathematical logic, only in a different language (homotopy theory plays a major role in Voevodsky¡¯s work on the Milnor conjecture which earned him the prestigious Fields medal in 2002).

Voevodsky, a professor at the Institute for Advanced Study in Princeton, wants to bring together two streams of development of today¡¯s mathematics. ETH has invited him to present his ideas in Zurich as a speaker of the 2014 Paul Bernays Lectures in September. Giovanni Felder, the director of the ETH Institute for Theoretical Studies (ITS), will introduce his research to the lecture audience at ETH. He says: ¡°Voevodsky is developing a new theory which places mathematics on a new foundation. The questions he raises concern the foundations of mathematics as well as those of computer science and logic.¡± This theory is called ¡°Homotopy Type Theory (HoTT)¡±, and ¡°Univalent Foundations of Mathematics¡± is the computer-oriented project in which it is being investigated.

A simpler language for computer proofs

Within the framework of HoTT, Vladimir Voevodsky is developing an approach that allows mathematical proofs to be translated into a programming language for computer proof assistants much more easily than they can be today. If this approach succeeds, computers could in the future check proofs that are so complicated that even distinguished mathematicians make mistakes. ¡°With the help of computer proof assistants, we can build highly complex and highly abstract mathematical theories¡±, says Voevodsky.

For mathematicians, such proof assistants would be no bagatelle for on the one hand verification is something like their key technique, and on the other hand these proof assistants require new foundations of mathematics. In order to be accepted, proofs in mathematics must be correct and follow the rules of logic. Their correctness must be derivable without error and from certain true principles (axioms) and already proven statements. It has been the dream of many mathematicians to formulate axioms from which virtually all mathematical theorems can be derived and proven unambiguously.

Set theory is difficult to translate

One such system of axioms was proposed in 1908 by Ernst Zermelo. Today it is known as the Zermelo-Fraenkel set theory with the axiom of choice and it serves as a foundation of all of mathematics, as all mathematical objects can be interpreted as sets.

The disadvantage of set theory is that its principles are very difficult to translate into the programming language of a proof assistant. This is why the computer proof systems existing today, such as ¡°coq¡±, which Voevodsky uses, are based on type theory, which the British mathematician and philosopher Bertrand Russell (1872-1970) proposed as an alternative to set theory.

The innovative thing about Voevodsky¡¯s approach is that he interprets the propositions of the formal system of type theory in the language of homotopy theory. In this interpretation, an additional feature applies, namely univalence, which Voevodsky adds to the foundations of mathematics as a new axiom. In it he relates the equality of logical-mathematical propositions to the equivalence in the sense of homotopy theory.

Mug and donut: a more comprehensive language

This approach may be surprising at first, as homotopy theory is actually about how different geometric objects can be transformed into each other by deformation. This can be illustrated with a coffee mug and a donut: When you look at their shapes, they are completely different. But if you look at their properties, they are both an ¡°object with an opening¡±. The donut is a ring and the mug has a handle. The mug can be transformed into a donut in such a way that the points lying next to each other on the mug also lie next to each other on the donut. Therefore, these two intuitively different objects have the same properties. As mathematicians would say, they are equivalent.

This equivalence problem also arises in the interpretation of equations used in mathematics and in programming languages. An equation such as ¡°a=b¡± is a mathematical proposition in which two different symbols have the same value. Logically, this corresponds to the two different shapes with structurally equal properties.

Same idea, different languages

¡°Thanks to Voevodsky, we now know that such equivalence relationships can be better formulated in homotopy theory because it is a more comprehensive theory¡±, says Giovanni Felder. Homotopy theory explains not only why ¡°a equals b¡± but also how to get from a to b. In set theory, this information would have to be defined additionally, which makes the translation of mathematical propositions into programming language more difficult, says Felder. ¡°The hope is that Voevodsky¡¯s method will allow proofs to be translated into programming language more directly and verified more efficiently.¡°

When asked whether computers will eventually prevail over humans when it comes to verifying mathematical proofs, Voevodsky and Felder answer openly. Voevodsky says: ¡°We are still at the very beginning of a long road of change and it is impossible to say today where it will take us.¡± Felder says: ¡°Computers can make mistakes. Humans can make mistakes. All we know for sure is that mathematics is getting more complex and proofs are not getting simpler.¡°