Vladimir Voevodsky died last week. He won the Fields Medal in 2002 for proving the Milnor conjecture in a branch of algebra known as algebraic K-theory. He continued to work on this subject until he helped prove the more general Bloch–Kato conjecture in 2010.

Proving these results—which are too technical to easily describe to nonmathematicians!—required him to develop a dream of Grothendieck: the theory of motives. Very roughly, this is a way of taking the space of solutions of some polynomial equations and chopping it apart into building blocks. But this process of ‘chopping’ and also these building blocks, called ‘motives’, are very abstract—nothing easy to visualize.

It’s a bit like how a proton is made of quarks. You never actually see a quark in isolation, so you have to think very hard to realize they are there at all. But once you know this, a lot of things become clear.

This is wonderful, profound mathematics. But in the process of proving the Bloch-Kato conjecture, Voevodsky became tired of this stuff. He wanted to do something more useful… and more ambitious. He later said:

It was very difficult. In fact, it was 10 years of technical work on a topic that did not interest me during the last 5 of these 10 years. Everything was done only through willpower.

Since the autumn of 1997, I already understood that my main contribution to the theory of motives and motivic cohomology was made. Since that time I have been very conscious and actively looking for. I was looking for a topic that I would deal with after I fulfilled my obligations related to the Bloch-Kato hypothesis.

I quickly realized that if I wanted to do something really serious, then I should make the most of my accumulated knowledge and skills in mathematics. On the other hand, seeing the trends in the development of mathematics as a science, I realized that the time is coming when the proof of yet another conjecture won’t have much of an effect. I realized that mathematics is on the verge of a crisis, or rather, two crises.

The first is connected with the separation of “pure” and applied mathematics. It is clear that sooner or later there will be a question about why society should pay money to people who are engaged in things that do not have any practical applications.

The second, less obvious, is connected with the complication of pure mathematics, which leads to the fact that, sooner or later, the articles will become too complicated for detailed verification and the process of accumulating undetected 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, this accumulation of errors for mathematics is very dangerous.

So, I decided, you need to try to do something that will help prevent these crises. For the first crisis, this meant that it was necessary to find an applied problem that required for its solution the methods of pure mathematics developed in recent years or even decades.

He looked for such a problem. He studied biology and found an interesting candidate. He worked on it very hard, but then decided he’d gone down a wrong path:

Since childhood I have been interested in natural sciences (physics, chemistry, biology), as well as in the theory of computer languages, and since 1997, I have read a lot on these topics, and even took several student and post-graduate courses. In fact, I “updated” and deepened the knowledge that had to a very large extent. All this time I was looking for that I recognized open problems that would be of interest to me and to which I could apply modern mathematics.

As a result, I chose, I now understand incorrectly, the problem of recovering the history of populations from their modern genetic composition. I took on this task for a total of about two years, and in the end, already by 2009, I realized that what I was inventing was useless. In my life, so far, it was, perhaps, the greatest scientific failure. A lot of work was invested in the project, which completely failed. Of course, there was some benefit, of course—I learned a lot of probability theory, which I knew badly, and also learned a lot about demography and demographic history.

But he bounced back! He came up with a new approach to the foundations of mathematics, and helped organize a team at the Institute of Advanced Studies at Princeton to develop it further. This approach is now called homotopy type theory or univalent foundations. It’s fundamentally different from set theory. It treats the fundamental concept of *equality* in a brand new way! And it’s designed to be done with the help of computers.

It seems he started down this new road when the mathematician Carlos Simpson pointed out a serious mistake in a paper he’d written.

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. I didn’t have the tools to explore the areas where curiosity was leading me and the areas that I considered to be of value and of interest and of beauty.

So I started to look into what I could do to create such tools. And it soon became clear that the only long-term solution was somehow to make it possible for me to use computers to verify my abstract, logical, and mathematical constructions. The software for doing this has been in development since the sixties. At the time, when I started to look for a practical proof assistant around 2000, I could not find any. There were several groups developing such systems, but none of them was in any way appropriate for the kind of mathematics for which I needed a system.

When I first started to explore the possibility, computer proof verification was almost a forbidden subject among mathematicians. A conversation about the need for computer proof assistants would invariably drift to Gödel’s incompleteness theorem (which has nothing to do with the actual problem) or to one or two cases of verification of already existing proofs, which were used only to demonstrate how impractical the whole idea was. Among the very few mathematicians who persisted in trying to advance the field of computer verification in mathematics during this time were Tom Hales and Carlos Simpson. Today, only a few years later, computer verification of proofs and of mathematical reasoning in general looks completely practical to many people who work on univalent foundations and homotopy type theory.

The primary challenge that needed to be addressed was that the foundations of mathematics were unprepared for the requirements of the task. Formulating mathematical reasoning in a language precise enough for a computer to follow meant using a foundational system of mathematics not as a standard of consistency to establish a few fundamental theorems, but as a tool that can be employed in everyday mathematical work. There were two main problems with the existing foundational systems, which made them inadequate. Firstly, existing foundations of mathematics were based on the languages of predicate logic and languages of this class are too limited. Secondly, existing foundations could not be used to directly express statements about such objects as, for example, the ones in my work on 2-theories.

Still, it is extremely difficult to accept that mathematics is in need of a completely new foundation. Even many of the people who are directly connected with the advances in homotopy type theory are struggling with this idea. There is a good reason: the existing foundations of mathematics—ZFC and category theory—have been very successful. Overcoming the appeal of category theory as a candidate for new foundations of mathematics was for me personally the most challenging.

Homotopy type theory is now a vital and exciting area of mathematics. It’s far from done, and to make it live up to Voevodsky’s dreams will require brand new ideas—not just incremental improvements, but actual sparks of genius. For some of the open problems, see Mike Shulman’s comment on the *n*-Category Café, and some replies to that.

I only met him a few times, but as far as I can tell Voevodsky was a completely unpretentious person. You can see that in the picture here.

He was also a very complex person. For example, you might not guess that he took great wildlife photos:

You also might not guess at this side of him:

In 2006-2007 a lot of external and internal events happened to me, after which my point of view on the questions of the “supernatural” changed significantly. What happened to me during these years, perhaps, can be compared most closely to what happened to Karl Jung in 1913-14. Jung called it “confrontation with the unconscious”. I do not know what to call it, but I can describe it in a few words. Remaining more or less normal, apart from the fact that I was trying to discuss what was happening to me with people whom I should not have discussed it with, I had in a few months acquired a very considerable experience of visions, voices, periods when parts of my body did not obey me, and a lot of incredible accidents. 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), never falling asleep for all these days.

Almost from the very beginning, I found that many of these phenomena (voices, visions, various sensory hallucinations), I could control. So I was not scared and did not feel sick, but perceived everything as something very interesting, actively trying to interact with those “beings” in the auditorial, visual and then tactile spaces that appeared around me (by themselves or by invoking them). I must say, probably, to avoid possible speculations on this subject, 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”, naturally I mean what in modern terminology are called complex hallucinations. The word “beings” emphasizes that these hallucinations themselves “behaved”, possessed a memory independent of my memory, and reacted to attempts at communication. In addition, they were often perceived in concert in various sensory modalities. For example, I played several times with a (hallucinated) ball with a (hallucinated) girl—and I saw this ball, and felt it with my palm when I threw it.

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

I managed to get out of this state due to the fact that I forced myself to start math again. By the middle of spring 2008 I could already function more or less normally and even went to Salt Lake City to look at the places where I wandered, not knowing where I was, in the spring of 2007.

In short, he was a genius akin to Cantor or Grothendieck, at times teetering on the brink of sanity, yet gripped by an immense desire for beauty and clarity, engaging in struggles that gripped his whole soul. From the fires of this volcano, truly original ideas emerge.

This last quote, and the first few quotes, are from some interviews in Russian, done by Roman Mikhailov, which Mike Stay pointed out to me. I used Google Translate and polished the results a bit:

• Интервью Владимира Воеводского (часть 1), 1 July 2012. English version via Google Translate: Interview with Vladimir Voevodsky (Part 1).

• Интервью Владимира Воеводского (часть 2), 5 July 2012. English version via Google Translate: Interview with Vladimir Voevodsky (Part 2).

The quote about the origins of ‘univalent foundations’ comes from his nice essay here:

• Vladimir Voevodsky, The origins and motivations of univalent foundations, 2014.

There’s also a good obituary of Voevodsky explaining its relation to Grothendieck’s idea in simple terms:

• Institute for Advanced Studies, Vladimir Voevodsky 1966–2017, 4 October 2017.

The photograph of Voevodsky is from Andrej Bauer’s website:

• Andrej Bauer, Photos of mathematicians.

To learn homotopy type theory, try this great book:

• *Homotopy Type Theory: Univalent Foundations of Mathematics*, The Univalent Foundations Program, Institute for Advanced Study.

Thank you for sharing this. I can’t help but notice some stunning parallels between his mathematical ideas and his wildlife photos: they portray creatures with true character within a framework of intense beauty. Do others see this as well?

Hmm, I hadn’t thought of that. I’ll have to ponder it.

There are some interesting comments on an essentially identical post of mine over here.

Indeed, thanks!

A tragedy, condolences to all concerned, and that includes all those who worry about the foundations of thinking.

I am an advocate of ultra-finitism (no infinity enabled in any axiom, whatsoever; for example no axiom of indefinite induction). Computers, as we have them now, practice ultra-finitism (and they work). However, of course, if one puts garbage into a machine, one has to exert great care not to get garbage out.

Namely if some axioms enabling some impossible operation (like the Axiom of Choice) is installed inside the data entering the computer, it may well be like inserting self-contradictory data.

Some may wonder what the motivation of ultra-finitism would be. Simple: mathematicians would start focusing more on more practical, thus powerful, mathematics, such as hypersonic flow. And all sorts of nonlinear mathematics, which are all over the natural world.

Patrice Ayme

Thank you so much for writing this.

You’re welcome!

Path-dependent equality sounds interesting.

How/where is that used?

I’m not sure what you’re referring to, but in homotopy theory a path between points is considered to be ‘just as good as’ an equation between points… so, roughly speaking, homotopy type theory takes paths as a kind of replacement for equations.

I remember when mathematicians lamented over Russell-Whitehead’s failure to subdue logic with mathematics. Nowadays I wonder if- besides putting mathematicians out of work, if automated theorem proving would also lead to the robot uprising and extinction of humanity as we know it.

But really, I was wondering if this,

It treats the fundamental concept of equality in a brand new way!, was less dangerous in terms of physics where a classical “equality” operator would work for say, identical particles, while this more potent version would lead to actual physical (visible) paths. For instance, Faraday’s idea of magnetic lines of force are considered a virtual if practical artifice, but the idea that those lines were actually “instantiated” (borrowing a software engineering term to distinguish pointers fromactualreferences) in terms of visible lines in iron filings. On this matter I once had a long discussion with an x-ray physicist who refused to acknowledge the existence of those lines in iron filings. This seemed to me a bit too much like arguing phenomenology with Thermostellar Bomb #20.It also hasn’t escaped my attention that the diplomatic/legal uses of the logical “or” (exclusive xor vs. inclusive ior) are often to blame for causing many misunderstandings (I have on only one occasion also noticed a similar ambiguity in the abuse of the logical “and”). The xor operation is notoriously useful from computer graphics to quantum computing.

And similarly QT and SR are wrought with logical stumpers caused say, whenever one particle is said to take two paths through two slits at the same time or any notion that it is more lucrative to age wine at the speed of light than in caves.

Astonomy is also wrought with many logical head scratchers. If an astronomer looks through the eyepiece of a really big telescope, way back in time, they should in principle be able to see the proton that’s currently residing in the back of their own head: because (most?) protons have allegedly been around since the Big Bang. So how’d it get there? Any explanation of an FTL expansion period won’t prevent a flood of more sci.physics FAQ questions about say, …how long a meter stick is in a galaxy that’s 13 billion light-years away compared to how long it is right here and now and whether or not Doppler shift calculations of velocities from long-slit spectrographs are corrected for such dispersions.

So- whenever I hear anything about an improved logic or definitions of “equivalent”, “equal”, “equality”, “identical”, … my ears perk up, because such things seem terribly fundamental.

I was really sad to hear this news. I had the pleasure of meeting him a couple of times, and I learned a lot from my conversations with him.

“From the fires of this volcano, truly original ideas emerge.” I have difficulty with the implication that psychological difficulties can be advantageous for creative mathematical work. Just seeing both properties present in a single person does not imply causation, in any direction.

There may be no causality, but there was a strong coherence in his personality, his goals and his determination to pursue them. The obituaries hiding the dark sides of his quest neither reflect nor pay enough tribute to the extremely perilous path he took and the strength of his mind. I fully agree with the conclusion of this post.

Maybe I said things the wrong way. This was a tribute, not a psychological study, so I shouldn’t be trying to draw general conclusions, just talk about

one way a life can be lived. But I feel I understand how some people are driven to brand new ideas through immense mental turmoil combined with a strong love of order and beauty. I was dissatisfied with how some obituaries focused solely on Voevodsky’s mathematical achievements and not his actual life: they presented a superficial, shiny, fake version of the real person.Of course obituaries may not be the place for honesty. But the

New York Timesfilled in some more details:By the way, Mr James Oliver Vicary, your new monicker seems awfully formal. Did you get a promotion or something?

A demotion more like, if I’m Mr rather than Dr!

Going through the process to post this comment, I notice that Chrome autofills the Name field with this stupid title, which it probably scraped from the last time I ordered something on Amazon.

I agree that Vladimir had an unconventional life, by the standards of many mathematicians. But I see no evidence that his mathematical work was enhanced by this, rather than produced in spite of it. Even if it were

enhancedby it, for many others this would not be the case, and indeed there are many people on this planet with unconventional lives, who are at the same time not mathematical geniuses. Therefore it seems wrong to me—and even potentially damaging, to people who may be enduring similar struggles—to romanticise the idea of the troubled mathematical genius.I remember him telling me great stories about spending evenings as a teenager breaking into some sort of Soviet military facility near his house.

“This was a tribute, not a psychological study, so I shouldn’t be trying to draw general conclusions, just talk about one way a life can be lived. But I feel I understand how some people are driven to brand new ideas through immense mental turmoil combined with a strong love of order and beauty. I was dissatisfied with how some obituaries focused solely on Voevodsky’s mathematical achievements and not his actual life: they presented a superficial, shiny, fake version of the real person.” Thank you, this is exactly my feeling as well (and I liked the version before you edited even better!).

“I agree that Vladimir had an unconventional life, by the standards of many mathematicians. But I see no evidence that his mathematical work was enhanced by this, rather than produced in spite of it. Even if it were enhanced by it, for many others this would not be the case, and indeed there are many people on this planet with unconventional lives, who are at the same time not mathematical geniuses. Therefore it seems wrong to me—and even potentially damaging, to people who may be enduring similar struggles—to romanticise the idea of the troubled mathematical genius.” Come on, any attempt to deduce universal psychological laws from VV’s life sounds ridiculous enough.

If there was a link between his struggles and accomplishments, I’d search for it in a genuine and uncompromising attitude without safeguards, both in mathematics and in life, though I doubt VV would approve any speculations on this subject.

Yet he was open about his experiences and his demons, including alcohol, and fighting them with admirable energy, They shaped his personality, whether we like it or not. Eluding them (as in the obituary of the nyt) amounts to considering them as shameful. I do not think they were, and we certainly have no right to judge.

A fine remembrance and tribute. Thanks.

[…] are a few of links that I read and on which I base this post: an obituary by John Baez, with some links, including to an account by himself of the origins of “univalent […]