I did some following up on the work of Vladimir Voevodsky and for anyone who might ask, “what’s actually going on in mathematics,” Voevodsky’s work adds, perhaps, even more to the mystery. Not that I mind. The mystery emerges from the limitless depths (or heights) of thought that are revealed in mathematical ideas or objects. It is this that continues to captivate me. And the grounding of these ideas, provided by Voevodsky’s work on foundations, reflects the intrinsic unity of these highly complex and purely abstract entities, suggesting a firm rootedness to these thoughts – an unexpected and enigmatic rootedness that calls for attention.
Voevodsky gave a general audience talk in March of 2014 at the Institute for Advanced Studies at Princeton, where he is currently Professor in the School of Mathematics. In that talk he described the history of much of his work and how he became convinced that to do the kind of mathematics he most wanted to do, he would need a reliable source to confirm the validity of the mathematical structures he builds.
As I was working on these ideas I was getting more and more uncertain about how to proceed. The mathematics of 2-theories is an example of precisely that kind of higher-dimensional mathematics that Kapranov and I had dreamed about in 1989. And I really enjoyed discovering new structures there that were not direct extensions of structures in lower “dimensions”.
But to do the work at the level of rigor and precision I felt was necessary would take an enormous amount of effort and would produce a text that would be very difficult to read. And who would ensure that I did not forget something and did not make a mistake, if even the mistakes in much more simple arguments take years to uncover?
I think it was at this moment that I largely stopped doing what is called “curiosity driven research” and started to think seriously about the future.
It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.
Voevodsky expresses the same concern in a Quanta Magazine article by Kevin Hartnett.
“The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error.
So, at the heart of this discussion seems to be a quest for useful math-assistant computer programs. But both the problems mathematicians like Voevodsky face, and the computer assistant solutions he explored, highlight something intriguing about mathematics itself.
Hartnett does a nice job making the issues relevant to Voevodsky’s innovations accessible to any interested reader. He reviews Bertrand Russell’s type theory, a formalism created to circumvent the paradoxes of Cantor’s original set theory – as in the familiar paradox created by things like the set of all sets that don’t contain themselves. (If the set does contain itself then it doesn’t contain itself) This kind of problem is avoided in Russel’s type theory by making a formal distinction between collections of elements and collections of other collections. In turns out that within type theory, equivalences among sets are understood in much the same way as equivalences among spaces are understood in topology.
Spaces in topology are said to be homotopy equivalent if one can be deformed into the other without tearing either. Hartnett illustrates this using letters of the alphabet:
The letter P is of the same homotopy type as the letter O (the tail of the P can be collapsed to a point on the boundary of the letter’s upper circle), and both P and O are of the same homotopy type as the other letters of the alphabet that contain one hole — A, D, Q and R.
The same kind of equivalence can be established between a line and a point, or a disc and a point, or a coffee mug and a donut.
Given their structural resemblance, type theory handles the world of topology well. Things that are homotopy equivalent can also be said to be of the same homotopy type. But the value of the relationship between type theory and homotopic equivalences was greatly enhanced when Voevodsky learned Martin-Löf type theory (MLTT), a formal language developed by a logician for the task of checking proofs on a computer. Voevodsky saw that this computer language formalized type theory and, by virtue of type theory’s similarity to homotopy theory, it also formalized homotopy theory.
Again, from Hartnett:
Voevodsky agrees that the connection is magical, though he sees the significance a little differently. To him, the real potential of type theory informed by homotopy theory is as a new foundation for mathematics that’s uniquely well-suited both to computerized verification and to studying higher-order relationships.
There is a website devoted to homotopy type theory where it is defined as follows:
Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, constructive type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos.
Voevodsky’s work is on a new foundation for mathematics and is also described there:
Univalent Foundations of Mathematics is Vladimir Voevodsky’s new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. The type theoretic univalence axiom relates propositional equality on the universe with homotopy equivalence of small types. The program is currently being implemented with the help of the automated proof assistant Coq. The Univalent Foundations program is closely tied to homotopy type theory and is being pursued in parallel by many of the same researchers.
In one of his talks, Voevodsky suggested that mathematics as we know it studies structures on homotopy types. And he describes a mathematics so rich in abstract complexity, “it just doesn’t fit in our heads very well. It somehow requires abilities that we don’t posses.” Computer assistance would be expected to facilitate access to these high levels of complexity and abstraction.
But mathematics is, as I see it, the abstract expression of human understanding – the possibilities for thought, for conceptual relationships. So what is it that’s keeping us from being able to manage this level of abstraction? Voevodsky seems to agree that it is comprehension that gives rise to mathematics. He’s quoted in a New Scientist article by Jacob Aron:
If humans do not understand a proof, then it doesn’t count as maths, says Voevodsky. “The future of mathematics is more a spiritual discipline than an applied art. One of the important functions of mathematics is the development of the human mind.”
While Aaron seems to suggest that computer companions to mathematicians could potentially know more than the mathematicians they assist, this view is without substance. It is only when the mathematician’s eye discerns something that we call it mathematics.
Mike Shulman has a few posts related to homotopy type theory on The n-Category Cafe site beginning with one entitled Homotopy Type Theory, I followed by II, III, and IV. There’s also one from June 2015 – What’s so HoTT about Formilization?
And here’s a link to Voevodsky’s Univalent Foundations.
Recent Comments