Interview with Vladimir Voevodsky (Part 1)

I’m not the author of the original interview. This is a translation of the original that can be found on Roman’s LJ: https://baaltii1.livejournal.com/198675.html
Nothing was added to or removed from this conversation between the two mathematicians.

July 1, 2012.

This is an interview with mathematician Vladimir Voevodsky. Usually, interviews with scientists touch upon the formal aspects of their work, roughly what is clear without any questions and answers, while what is really interesting and important remains hidden. Vladimir Voevodsky is a Fields Medal laureate, professor at the Institute for Advanced Study in Princeton, creator of the motivic homotopy theory and univalent foundations of mathematics. The conversation will be not only about mathematics but also about life in general, and largely about what is not customary to speak about openly, at least in scientific circles.

We started this conversation in Princeton, strolling through the local life and a beautiful sunset. It seemed that such a conversation could be interesting to many: both mathematicians and simply to searching people. So, the questions are asked by Roma Mikhailov. Vladimir Voevodsky answers.

Vladimir Voevodsky. Photo from Roman’s LJ

- The next academic year at the Institute for Advanced Study is dedicated to the univalent foundations of mathematics. And you act as the founder of this field. But at the same time, your main scientific results, which brought recognition and fame, belong to a completely different area: algebraic geometry, the theory of motives. On your website, you wrote that you devoted about twenty years to the theory of motives but are no longer interested in it. Have you radically changed your field of research?

- The question is rhetorical...

- Your most famous result is the solution of Milnor's problem on K-functors of fields. You got it back in 96. What happened next? How did your scientific interests evolve in the following years?

- First, it was necessary to prove a generalization of Milnor's conjecture, now known as the Bloch-Kato conjecture. I formulated the main ideas of this proof at the end of 96, around the same time when I wrote the first complete version of the proof of Milnor's conjecture. There were several problems in the approach I came up with to prove Bloch-Kato. First, it depended on some "sub-hypothesis," which was a generalization of one of Markus Rost's results. Secondly, on the development of much more advanced concepts in motivic homotopy theory than those that were sufficient to prove Milnor's conjecture. It was clear that Markus would most likely be able to do the first, and I would have to do the second. As a result, the first was completed in, I think, 2007 or 2008 by Suslin, Zhuhovitsky and Weibel, based on Markus's sketches. And I finished all the preliminary work and the proof itself only in February 2010.

It was very difficult. Essentially, it was 10 years of technical work on a topic that I had not been interested in for the last 5 of those 10 years. Everything was done only by willpower.

Starting from the fall of 1997, I already understood that my main contribution to the theory of motives and motivic cohomology had been made. From that time, I very consciously and actively searched. I was looking for a topic that I would do when I fulfilled my obligations related to the Bloch-Kato conjecture. I quickly realized that if I wanted to do something really serious, I had to make the most of my accumulated knowledge and skills in mathematics. On the other hand, seeing the development trends of mathematics as a science, I understood that the time was coming when proving yet another hypothesis would change little. That mathematics is on the verge of a crisis, or rather two crises. The first is related to the separation of "pure" mathematics from applied mathematics. It is clear that sooner or later the question will arise as to why society should pay money to people who are engaged in things that have no practical applications. The second, less obvious, is related to the complication of pure mathematics, which leads to the fact that, again, sooner or later, articles will become too complex for detailed verification and a process of accumulation of unnoticed errors will begin. And since mathematics is a very deep science, in the sense that the results of one article usually depend on the results of many and many previous articles, such an accumulation of errors is very dangerous for mathematics.

So, I decided, we need to try to do something that will help prevent these crises. In the first case, this meant that it was necessary to find such an applied problem that would require modern pure mathematics methods developed in recent years, or at least decades, to solve it.

I have been interested in natural sciences (physics, chemistry, biology), as well as the theory of computer languages since childhood, and starting from 1997, I read a lot on these topics, and even took several undergraduate and graduate-level courses. In fact, I "updated" and deepened the knowledge that I had to a very significant extent. All this time I was looking in what I learned for open problems that would be interesting to me and to which I could apply modern mathematics.

As a result, I incorrectly, as I now understand, chose the problem of reconstructing the history of populations from their modern genetic composition. I messed with this task for a total of about two years and eventually, already in 2009, I realized that what I came up with was useless. In my life, so far, this was probably the biggest scientific failure. A lot of work was invested in a project that completely failed. Some benefit, of course, still was - I learned a lot from probability theory, which I knew poorly, and also learned a lot about demography and demographic history.

At the same time, I was looking for approaches to the problem of error accumulation in works on pure mathematics. It was clear that the only solution was to create a language in which mathematical proofs could be written by people in such a form that it could be checked on a computer. Up until 2005, it seemed to me that this task was much more complicated than the task of historical genetics that I was working on. In many ways, this feeling was the result of the established and very widespread opinion among mathematicians that abstract mathematics cannot be reasonably formalized so accurately that a computer would "understand" it.

In 2005, I managed to formulate several ideas that unexpectedly opened a new approach to one of the main problems in the foundations of modern mathematics. This problem can be informally formulated as the question of how to correctly formalize the intuitive understanding that "identical" mathematical objects have the same properties. Arguments based on this principle are very often used in modern mathematical proofs, but the existing foundations of mathematics (Zermelo-Fraenkel set theory) are completely unsuitable for formalizing such arguments.

I was very well acquainted with this problem and thought about it back in 1989, when Misha Kapranov and I worked on the theory of poly-categories. Then it seemed to us that it was impossible to solve it. What I managed to understand in 2005, combining ideas from homotopy theory (parts of modern topology) and type theory (parts of modern programming language theory), was completely amazing, and opened up real possibilities for constructing the very language in which people can write proofs that a computer can verify. Then there was a big break in my mathematical activity. From June 2006 to November 2007, I did not do mathematics at all. We will discuss what happened during this period in another part of the interview. Now, thinking about what was happening to me at this time, I often recall the story of A. and B. Strugatsky "A Billion Years Before the End of the World". I returned to mathematics at the end of 2007. I worked at first in intervals, then on my ideas related to historical genetics, then on completing the cycle of works with the proof of the Bloch-Kato conjecture. I returned to the ideas related to computer verification of proofs only in the summer of 2009, when it became finally clear to me that nothing was happening with historical genetics. And literally a few months later, two events happened that moved these ideas from general outlines, which, I thought, would have to be worked on for more than one year, to a stage at which I could declare that I had come up with new foundations of mathematics that would allow solving the problem of computer verification of proofs. Now it is called "univalent foundations of mathematics" and both mathematicians and theorists of programming languages are engaged in it. I have almost no doubt that these foundations will soon replace set theory and that the problem of the language of abstract mathematics, which computers will "understand," can be considered basically solved.

- How is this ideology perceived by the modern mathematical community, namely specialists in categories, logic, homotopies? Have many allies been found among professional mathematicians who are ready to seriously work on the univalent foundations?

- Differently. There are quite a lot of associates and more and more are gathering. Of course, it is most difficult for specialists in logic and foundations of mathematics, because in fact what I propose shifts both set theory and classical logic to the background.

- Do I understand correctly that at the moment you are trying to explain to machines what categorical and homotopy-theoretic intuition is, on which many constructions of modern mathematics are based?

- No, not right. That was the first stage, which ended in the fall of 2009. Now much more technical work is underway to improve the language as such. The first examples of languages of the class with which I work were created in the late 1970s and are known as "Martin-Löf type theories". In an amazing way, the languages were created, software systems using these languages were created and even became popular (especially the "Coq" system created by the French), but there was no understanding of what these languages allow talking about. It turned out that only a very small part of the language's capabilities is used, the one that, as it is now clear, allows talking about sets. The language as a whole allows us to talk about homotomous types of any level of complexity. The gap, as you understand, is huge. As a consequence, the languages themselves were not improved, because it was not clear what could be changed and what could not. Now, when we understand what is essential in these languages and what is not, the opportunity opens up to make them significantly more "powerful" and, as a result, more convenient for practical use.

- How do you see it, when will the computer be able to verify your solution to the Milnor's problem?

- If you simply set yourself the task of writing a formal version of the proof using the Coq formal proof system that already exists now, then, probably, this can be done in 3-4 years. I don't plan to do this, as I believe that it is much more important and interesting to develop a new system for formal proofs built taking into account the univalent semantics and the new vision of "meaning" in type theory languages that it opens up. And how long it may take, I don't see at all yet.

Vladimir Voevodsky and Roman Mikhailov. Photo from Roman’s LJ

- A couple of years ago, a conference on general scientific issues was held in St. Petersburg. You spoke there and said the following. "What we now call the crisis of Russian science is not a crisis of only Russian science. There is a crisis in world science. Real progress will consist in a very serious fight between science and religion, which will end with their unification. And don't hit my face.."

I confess, when I read this statement, I laughed joyfully, just happiness covered me, because someone spoke about the deep, not about politics-financing-economics, but about what is really important. But this statement probably remained incomprehensible to many. You are a person brought up in materialistic paradigms, with the corresponding ideology, aesthetics, morality. By caste, you are a Soviet intellectual, while at the same time having made a brilliant scientific career. And society, stereotypes, patterns shout from everywhere that in the life of such a person there is no place for religion and mysticism. But you openly begin to talk about some kind of unification of science and religion, your table at home is piled with Hindu books, Sanskrit textbooks, books in ancient Greek, books about supernatural phenomena, shamanism, and the history of religions are on the shelves. How so?

- Here is the story. As I said, I know the natural sciences quite well for a non-professional. Several areas of physics, several areas of biology, chemistry, a little geology and paleontology. In addition, I was seriously interested in artificial intelligence and language semantics. In 1997-1999, I read many modern books whose authors tried to create a kind of scientific philosophy, i.e. to combine the existing scientific theories into a general picture of our world. I especially remember the book by Edward Wilson, "Consilience" (I don't know how it is in Russian). As a mathematician, I am very sensitive to "holes" in arguments, to those places where the conclusion does not formally follow from the premises, but is, as they say, pulled by the ears. So, after reading all these books, I was convinced that those who say that modern science explains our world are wrong. Yes, some sciences very successfully and accurately explain individual groups of phenomena. But these explanations do not "glue together" into a complete picture of the world in any way. Moreover, some of the so-called scientific explanations are essentially, I will not be afraid of this word, a profanation. The most important example of such a situation is Darwinism. No argument, the Earth's biosphere has evolved and is evolving, and the processes of natural selection and random mutations play a certain role in this development. But they do not in any way explain this development. By the way, this is now gradually beginning to be discussed by serious biologists, but even ten years ago, in America, a biologist, having expressed such a point of view, could seriously ruin his career.

The understanding of how little our sciences actually explain came to me somewhere when I was 35 years old, i.e. around 2001. At that time, I did not in any way connect this with the fact that in the 20th century, science excluded from the field of its attention what is now commonly called the "supernatural". I still treated everything mystical-religious as deception or delusion. I stood very firmly on this position until 2007. The period from 2001 to 2006 was very difficult. For several years I saved myself only by taking up wildlife photography. Some of my photos from that period can be found here: http://pics.livejournal.com/vividha.

- It happens that people of search become so after coming into contact with something that does not fit into their old understanding, into their usual picture of the world. For example, they say that Gurdjieff as a child witnessed a ritual act in which children circled a Yazidi boy, and he could not break out of this circle. Shocked by the supernatural he saw, as well as by human cruelty, Gurdjieff began to search for new knowledge about the world and man. Have you had any points, events, inexplicable phenomena that served as an impetus for rethinking?

- In 2006-2007, many things happened to me, both external and internal, after which my point of view on the issues of the "supernatural" changed significantly. What was happening to me during these years can probably be compared most closely to what happened to Carl Jung in 1913-14. Jung called it a "confrontation with the unconscious." I don't know what to call it, but I can describe it in a nutshell. While remaining more or less normal, except for the fact that I tried to discuss what was happening to me with people with whom I probably should not have discussed it, in a few months I gained a very considerable experience of visions, voices, periods when individual parts of my body did not obey me and many incredible coincidences. The most intense period was in mid-April 2007, when I spent 9 days (7 of them in the Mormon capital of Salt Lake City) without falling asleep once in all those days.

Almost from the very beginning, I discovered that many of these phenomena (voices, visions, various sensory hallucinations), I can control. Therefore, I was not scared and did not feel sick, but perceived everything that was happening as something very interesting, actively tried to interact with those "beings" in the auditory, visual, and then tactile spaces that appeared (by themselves or on call) around me. It probably needs to be said, in order to avoid possible speculation on this topic, that I did not use any drugs during this period, tried to eat and sleep a lot, and drank diluted white wine.

Another comment - when I say beings, then naturally I mean what in modern terminology is called complex hallucinations. The word "beings" emphasizes that these hallucinations "behaved" independently, had a memory independent of my memory, and reacted to attempts at communication. In addition, they were often perceived consistently in various sensory modalities. For example, I played (hallucinated) ball with a (hallucinated) girl several times, and I both saw this ball and felt it tactilely with my palm when I threw it.

Despite the fact that all this was very interesting, it was also very difficult. It happened over several periods, the longest of which lasted from September 2007 to February 2008 without interruption, and there were days when I could not read, and days when the coordination of movements was disturbed to such an extent that it was difficult to walk.

I managed to get out of this state by forcing myself to start doing mathematics again. By mid-spring 2008, I could already function more or less normally and even went to Salt Lake City to see the places where I wandered, not knowing where I was, in the spring of 2007.

It must be said that despite many conversations with immaterial "beings" during this period, I did not understand at all what actually happened. I was "offered" many explanations, including hypnotists, aliens, demons, and secret communities of people with magical abilities. None of the explanations explained everything I observed. In the end, since some terminology was needed in conversations, I began to call all these creatures spirits, although now I think that this terminology is not correct. The terms "worldwide system" (apparently of control over people) and, especially at the beginning, "a game whose hostess is fear" also sounded in this context.

After I returned to a more or less normal state, and in particular, I could read serious books again, I began to very actively study those areas of knowledge that I had previously ignored. First of all, I began to try to find descriptions of similar events that happened to other people. I must say that I did not succeed in this (not counting Jung). Something a little similar, but without visions, happened to Karen Armstrong, who then began to write books about different religions. There were many descriptions of how people experienced visions, voices, unusual emotional states, etc. for hours or days ("mystical experience"). As a rule, this either strengthened them in the religion in which they grew up or made them religious. A classic and very interesting example of when events of this kind continued with a person for a long time is Swedenborg. However, this was not similar to my case - Swedenborg quickly accepted what was happening to him as coming from God, and after that the process proceeded in a completely different way. Perhaps the most interesting story for me was the story of Carl Jung's "confrontation with the unconscious," but there the situation was also different because Jung, unlike me, encountered "supernatural" events from childhood and believed in God.

Part 2: