### The nightmare

#### by Orr Shalit

In September 30 the mathematician Vladimir Voevodsky passed away. Voevodsky, a Fields medalist, is a mathematician of whom I barely heard earlier, but after bumping into an obituary I was drawn to read about him and about his career. His story is remarkable in many ways. Voevodsky comes out as brilliant, intellectually honest giant, who bravely and honestly confronted the crisis that he observed “higher dimensional mathematics” was in.

Here 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 foundations”, and also this obituary on the IAS site.

Here I want to write about several aspects of Voevodsky’s story which struck me. Note, it is written from the point of view of a mathematician who has not studied his work at all. I surely am not qualified to give an account of his development of motivic cohomology and his solution of Milnor’s conjecture, achievements for which he won the Fields Medal, nor the development of *Univalent Foundations* or *Homotopy Type Theory *(though I am certainly determined to read the first chapters in the book on homotopy type theory *whenever I find the time*)*.* What really drew my attention in what I read about Voevodsky is the human story of a mathematician and his struggle. It is a story that can be understood by “human-level-IQ mathematicians” – in fact by any person – and it raises some disturbing and disheartening issues. Beyond the human story, there is the story of mathematics – our fractal and fragile profession, which at times seems to be standing on firm ground, and at times seems to be hanging on thin air.

Here are some key parts the story, brutally retold. (The quoted texts below here taken from this account by Voevodsky. The personal information is from the Wikipedia page or the obituaries linked above.)

**The existential nightmare. **Voevodsky apparently did not finish his undergraduate studies at Moscow State University (wiki says that he “flunked”!). However, as a first year undergrad he started reading a manuscript of Grothendiek’s and since then tried to develop his own mathematical ideas. He met Michael Kapranov and together they published a paper “-Groupoids as a Model for Homotopy Category”, where they “claimed to provide a rigorous mathematical formulation and a proof of Grothendieck’s idea…”. Based on this exceptional achievement (presumably), Kapranov arranged for Voevodsky to be accepted to Harvard graduate school (Voevodsky did not apply, and didn’t even know that this was being arranged!) where he worked under the supervision of David Kazhdan. He continued to do outstanding work, and went on to solve famous conjectures, get appointed to the Institute of Advanced Studies, and win the Fields Medal.

What a romantic story! But Voevodsky tells us what happened later:

In October 1998, Carlos Simpson submitted to the arXiv preprint server a paper called “Homotopy Types of Strict 3-groupoids.” It claimed to provide an argument that implied that the main result of the “∞-groupoids” paper, which Kapranov and I had published in 1989, cannot be true. However, Kapranov and I had considered a similar critique ourselves and had convinced each other that it did not apply. I was sure that we were right until the fall of 2013 (!!).

Voevodsky is telling us that his first paper, which boosted his stellar career, turned out to be flawed – the main result was not true! Moreover, he was not able (maybe it was an emotional block, maybe too much work) to settle the issue of who is right for 15 years!! The horror of this situation is unbearable. Or maybe it is not so horrifying – maybe at times he did not care any more, not enough to resolve it?

And another question comes to mind: what if he found his mistake, when he was writing the paper? What if he could not fix it (it was not fixable), and gave up on mathematics? So, should we, should he, be happy that he made this mistake? He also says that Kapranov and he considered this critique, but convinced themselves that it did not apply. Well, what if they still had doubts? Would ignoring these doubts have been the right thing to do? Was scratching the paper the right thing to do? But then maybe there would never have been an arrangement to have Voevodsky study at Harvard, maybe he would have not continued his mathematical pursuits.

Does it make any difference if a paper on -groupoids is correct or not? If a result is proven in a paper, and nobody ever finds the mistake, is it as good as true? If a person got a job, or tenure, on the basis of wrong paper – should he be dismissed? If you write a paper, and find a big mistake, should you withhold the information until the situation gets clearer? After all, its not your fault that you were even more diligent than Voevodsky, and found *your own* mistake, is it?

**The referee’s concerns. **But these are not the only mistakes coming up in this story. Voevodsky tells:

The field of motivic cohomology was considered at that time to be highly speculative and lacking firm foundation. The groundbreaking 1986 paper “Algebraic Cycles and Higher K-theory” by Spencer Bloch was soon after publication found by Andrei Suslin to contain a mistake in the proof of Lemma 1.1. The proof could not be fixed, and almost all of the claims of the paper were left unsubstantiated.

A new proof, which replaced one paragraph from the original paper by thirty pages of complex arguments, was not made public until 1993, and it took many more years for it to be accepted as correct. Interestingly, this new proof was based on an older result of Mark Spivakovsky, who, at about the same time, announced a proof of the resolution of singularities conjecture. Spivakovsky’s proof of resolution of singularities was believed to be correct for several years before being found to contain a mistake. The conjecture remains open.

The approach to motivic cohomology that I developed with Andrei Suslin and Eric Friedlander circumvented Bloch’s lemma by relying instead on my paper “Cohomological Theory of Presheaves with Transfers,” which was written when I was a Member at the Institute in 1992–93. In 1999–2000, again at the IAS, I was giving a series of lectures, and Pierre Deligne (Professor in the School of Mathematics) was taking notes and checking every step of my arguments. Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.

What’s going on? So many flawed papers. Makes one wonder *who were the charlatans who refereed these papers and accepted them for publication*. Of course, I am kidding. It really makes one wonder: *am I, as referee, accepting flawed paper after flawed paper? *Doesn’t it happen to all of us that we review a paper, it is a hard and technical paper, and then there is this lemma, which we can *convince* ourselves is true, but is it really true? It would be really hard to get to the bottom of this, and the other parts of the paper seem fine, and it is Voevodsky, mind you, who is author… I don’t really have time to check each and every lemma in this paper! It’s not my job! Can we let just this lemma pass? In fact, maybe we should, we do not want to block the next Voevodsy?

**The working mathematician’s toil. **If there are these truly important papers out there, by the leaders of our field, that are flawed, some of them even dead wrong, then what is the meaning of all this? Maybe there are more wrong papers, and nobody ever noticed? Does it even matter? Should I quit my job and become a carpenter, build real thing? Voevodsky says:

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 hard 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?

To me, the most inspiring part of Voevodsky’s story, is the way that he chose to handle the crisis that he observed mathematics is in. First of all, he honestly admitted that there is a problem, and he decided to confront it.

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.

But his pursuit for truth was much deeper than a superficial slogan “use computers”:

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.

And so he undertook the herculean task of developing new foundations for mathematics !! (of course, not alone). Could this enormous pressure, coming from within, from his own intellectual honestly, be what drove him to a breakdown? Probably, but not much information is given in the obituaries, since this stuff is very personal. Is it possible that it is not this pressure that led to his death at the very young age of 51?

**The graduate student’s ordeal. **

So let us return to the paper “Cohomological Theory of Presheaves with Transfers”, a very important paper which was certainly studied in many seminars worldwide. And imagine the budding graduate student, who doesn’t understand this lemma.

“Can you explain this?” he asks, and everybody volunteers to explain: “think of it this way…” says the veteran grad student, “it’s like bla bla blab la” and waves his hands. “Well, I see why its *morally* right”, says the budding one, “but I don’t understand the proof…”. Some others try to help, while the graduate starts to regret having asked. The postdoc moves uneasily in her chair. “What a waste of time!” she thinks, to be explaining lemmas to graduates students, and encourages: “I also had problems understanding that one, it’s one of those things that you have to work out on your own”. The supervisor recalls vaguely that he too had to work to understand that lemma (in fact, it was when he refereed the paper!) and that one could fix it somehow…. “um, technically I am not sure that this is precise, but we don’t really need the full power of the lemma, um, one can fix it” he says “now how did that go?”. Everybody waits “You know what, I’ll have to check my notes, why don’t we assume the lemma now and proceed”. And the budding graduate student is left with the feeling that everyone here is a clown except himself, or alternatively that everyone here is genius except himself, and maybe it isn’t that difficult and perhaps all this is not for him…

**The tired mathematician’s worry. **

So at the end, Voevodsky and many other mathematicians have set off to develop new foundations for mathematics, which, among other things, might make it easier to use computers to check proofs. Is this a good development? Is it necessary? Will it really help?

(If they can check our proofs, maybe the computers can do research on their own? Maybe they can also read one another’s papers. Imagine a world where all research mathematician are actually computers: how different would that world be? )

Do I have to invest myself in learning these new foundations? Should I wait? Maybe my field requires a different foundations and a different computer system to check it – is it a good idea to pursue these ideas?

Maybe all that “univalent nonsense” is important only if you want to work on Grothendiek-style shenanigan. If you do honest mathematics that actually relates to reality, you’re probably on safe ground and have nothing to worry about. Should I be worried?

*** * * * ***

To be honest, I am not very worried. I am split between being two opposite opinions. On the one hand, I am somewhat angry and disappointed at Mathematical Culture for **not** putting enough emphasis on correctness and understanding. It is clear that different people have very different notions of “understanding” and “knowing”. On the other hand, I think that mistakes are part of life, and also part of science, and therefore can and should be permitted be part of mathematics. These things happen, and by a process of mutation and selection, we hopefully evolve. (In passing, a request: please post corrigenda to your papers/books/etc.; perhaps math will move on without the corrigendum, but at least you can help that budding graduate student survive grad school in one piece).

And although I am very curious about univalent foundations, I cannot learn it in any deep way without stopping everything I am doing, and this won’t happen (one of the reasons why it won’t happen is that I am very skeptical). The details of Voevodsy’s mathematics, I feel, are not the important part of the story. The heart of the story is the determination to follow truth according to one’s standards and convictions, which is relevant far beyond mathematics, and which everyone can follow within their limitations. And maybe in this story there is also is a warning, or a calling, that those who come too close to the light, might burn.

Thank you for the post. Could you elaborate on your skepticism? About what are you very skeptical?

Thanks for you comment. I will write my feelings about this (please don’t consider this a “critique of HoTT” since to be a critique one needs to be well educated in the subject).

1. I am skeptical in a pratical sense: is it essential for me to know about this or can I just carry on? Does it matter to the working mathematician if the system engineers do some maintenance to the operating system?

And again, on a practical level: I would love to learn Russian. It sounds beautiful, and my Russian friends really did convince me that it is a richer language than Hebrew. I think that it would interesting and fun to learn it, and I believe that if I knew Russian I would be a better mathematician and also a better writer in English and Hebrew too. But I don’t have time to learn another language. And if I did I would learn Arabic.

2. I am skeptical on a personal level. I know that there are many good peopled involved, but focusing on Voevodsky, it seems this grew out of mathematics that is not exactly done the way I do. So, very roughly, “these are the same people” who tried to convince me that category theory is great and indispensable, that everything I know has a deeper and better explanation that uses some high-level algebro-categorical machinery. I’ve heard things like: “the theory of D-modules makes differential equations easy”, or “proving that the Lie algebra of a simply connected Lie group determines the group is easy using category theory: you just need to show that the functor Lie(.) is faithful!”. And then I go to a talk about derived categories, and the speaker promises an application to group theory, but that turns out to be just that he can prove something about derived categories of groups, but the new input to group theory is not clear. Then in some discussions a “space without points” comes up, but it never really does for me something I couldn’t understand otherwise. So you are doing mathematics in Shakespearean language, bravo!

I wasn’t convinced (like Voevodsky was, before univalent foundations) that category has to be the foundations of mathematics. So I am two steps behind this paradigm shift. Other people suggest other paradigm shifts in other directions (say, Doron Zeilberger). I have to make two paradigm shifts in a row, and I need to have a good reason to do that!

3. Finally, a basic element in set theory is a “set”, a basic element in type theory is a “type”. A basic element in homotopy type theory is a “homotopy type” (!!). You see the difference? The foundations require words and intuition that come from algebraic topology. Before we even started! Now isn’t that unfortunate? Maybe it is inevitable that to appreciate the name of the theory: “homotopy type theory” you have to have had mathematical training up to homotopy, but it is certainly unfortunate.

In your point 3 I wonder if you aren’t parsing incorrectly. I am not some HoTT expert, but I can think of two possible ways to read the thing you are concerned about. I am a homotopy theorist, and so I think about homotopy types, but maybe that isn’t what is meant here. For me a homotopy type is an equivalence class as opposed to being an object in some new version of type theory which the adjective homotopy might be used to denote. This doesn’t really argue against your point though, I just thought it might be useful.

To be honest, if you don’t find category theory useful, like for explaining induction and restriction of representations and how this relates to cohomology of schemes, then I am not sure that HoTT would be useful/fun for you. I certainly haven’t gone into it.

Thank you for the reply. I humbly offer a response from the perspective of someone who knows nothing about HoTT.

1. Nothing about HoTT seems indispensable to me either, but I don’t feel this opinion inspires skepticism in the sense of doubting the correctness or usefulness of the ideas. Aside from not rising to the top of your priorities, do you feel any skepticism in the latter sense? In your heart of hearts do you feel the foundational occupations have perhaps been a “waste” of Voevosky’s time and talent, at least in some sense?

2. I do not think the interest in category theory is mainly foundational, so while HoTT grew out of struggles with the book-keeping involved in Grothendick-flavored math, I don’t feel the reluctance to dedicate time to it should naturally extend to categories. The quotes you mention are not particularly modest, but perhaps they are intended for like-minded people. Although your example of Lie groups just paraphrases the problem, I view the very availability of a formalism detached from Lie groups per se as useful for organizing thoughts.

I am not sure the belief in categories as “the” foundation of math is requisite for “believing” HoTT, but finitism and constructivism appear naturally already in topos theory. I agree a good reason is required for shifting paradigms and admit a fair lack of concern for foundational issues.

3. I truly do think homotopy can be a first/second semester notion. Presented from the topological viewpoint, the notion of continuous deformation is intuitive and often easy to envision. I also don’t think foundations have to be elementary. The study of Lie groups involves plenty of verbiage but this is seen as a richness instead of a defect. Perhaps the sneakiness of the notion of equality truly should be viewed as a feature, whence set theory and type theory become “introductions”, interesting in their own right? In summary I don’t think it is necessarily unfortunate that foundations might involve historically sophisticated ideas.

Thanks for your comments, ergomango and Sean.

Sean and ergomango – Regarding my point 3: Maybe I am indeed misunderstanding – all I’ve read about this is the book’s introduction. I was just making the remark that *terminology* seems unappealing from the outset, since it uses technical mathematical words for describing basic constructions. I agree that foundations don’t have to be elementary, and maybe they cannot be.

ergomango – I don’t have doubts about the correctness of that theory, I mean: it seems that a lot of care has been taken with constructing this theory and that many smart people were involved. And in my heart I don’t feel that anything Voevodsky did was a waste of his time and talent. They are his! To the contrary, I find his decision to rationally stop doing “curiosity driven research” and think about something else is commendable and it inspires me to think deeply about what I do and how I do it, and whether and how that should change. I haven’t found the answers yet, and surely the answers I will give to myself will be different.

I do not want to give the impression that I think category theory is useless or bad. Certainly it helps to understand the people who talk this language, and I’ve found it useful to use this language as well.

Thanks for your reply. I really appreciated the way your post highlighted his convictions, I hadn’t really looked at it from that perspective before.

Perhaps you might enjoy the following old blog thread. It is admittedly incredibly long, or at least the comment thread is. However, it may highlight some of the benefits of HoTT as seen from the practitioners. Perhaps it is quicker than digging into the big book.

In case it is hidden too deep in the thread, I will mention one concrete thing we have learned from HoTT. There is an important result called Blakers-Massey Excision. The formulation of this result and its proof into HoTT had a somewhat surprising consequence, in my opinion. Prior to this, all known proofs actually used some geometry while the result itself can be stated purely homotopically. Charles Rezk then reverse engineered a purely homotopical proof from what the HoTT group had done (as their result/proof is stated type theoretically). I don’t mention this to encourage you to delve into HoTT but to offer a takeaway from the whole story which I think is concrete: we had a theorem in homotopy theory that didn’t really have a proof internal to homotopy theory, but through the HoTT proof we (Charles Rezk) found one. Note that this HoTT proof is computer checked! Which to me is just crazy.

Here is the promised blog thread:

https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/

Thanks for the link!

I really enjoyed this blog post.This internal debate that I think we all face between checking everything on one hand or just focusing on general ideas is something that I have been thinking really A LOT about lately you really helped me organize my thoughts by presenting the problem in such a clear and thoughtful way. And indeed it was the perfect (albeit sad) occasion to talk about it. Thank you very much.

Thank you.

Hi Orr,

First, You may know that Voevodsky gave a series of lectures on his ‘univalent foundations’ at the Haifa University, which I attended and seem to have grasped the gist of it (I have to refresh my memory to be more sound).

As I see it, one may somewhat compare the setting here to the case of the Bourbaki project: Bourbaki had an ambitious grand project to create, if you wish, ‘the modern day Elements of Euclid’.

In whatever way one judges their work and influence in light of that ambition,

they did give us some very good mathematical textbooks, while in other volumes they might have chosen a rather bizarre and unfruitful path.

Similarly, I am not convinced, as much as I know about computers, that if

one’s aim is to use computers to check proofs one has any necessary

need of Voevodsky’s approach. All one needs is some formalization (and

mayby now, with half-intelligent software like Apple’s Siri, even that may

be partly avoided). And the 20’th century (the inception, in fact,

occurred in the 19’th) offered many such formalizations.

Yet, Voevodsky’s system is very very nice mathematics. I was impressed,

for instance (as far as I recall), by the ‘unification’ of truth-values

and objects (In the usual approach to logic, a basic distinction is between

‘predicates’ – true or false when objects are substituted in ’empty

places’, such as ‘negative(x)’ or ‘x is bigger than y’, (or, not in

mathematics, good(person)), contrasted with ‘terms’ – functions, if one

wishes – where when one substitutes one get objects, such as ‘the

square of’ (or, not in mathematics: ‘the father of’). When there are no

empty places, these are, respectively, sentences – true or false (their

truth value) or constants.)

True, his construction lies on a foundation of topology, indeed

homotopy, where, for example, a circle is ‘the same’ as a solid round ‘bagel’

or a circle with a solid ball-like ‘bead’ put on it, and similarly for the

mappings. But that should not deter us – we do not seek ‘philosophical

foundation’, no more, as I see it, than prerequisites for a ‘computerizing

project’. One may say, for example, that the formal languages ordinarily

used in logic are natural-numbers ‘appendages’ par excellence. So why not

use ‘topology/homotopy appendages’ as well? Remember: we wish to seek and

get mathematical wisdom – Voevodsky’s system is very beautifully that –

not some philosophical ‘foundational reassurance’.

As for checking mathematical proofs by computer, I would venture to quote

from my arXiv article: ‘CHALLENGES TO SOME PHILOSOPHICAL CLAIMS ABOUT

MATHEMATICS’ (arXiv:1601.07125) page 6:

“Also, it might be helpful to stress the nature of a proof as something

ultimately formalizable thus capable of being viewed as a mathematical

object itself. In this spirit, one should distinguish between the formal

force of the proof and the real world question whether I really have a proof,

so whether I really know that the theorem is true: have I not made a

mistake? can I trust my memory? can I trust this book’s claim that so and

so was proved? can I trust the hardware and software of a computer that I

used in the proof? etc.”

The problem is that while we may (almost) trust that the harware of a

computer will do what the (digital) program – a formal system which may be

thought of as mathematical – dictates (A cosmic ray may thwart that,

but that would be remedies, say, by repetitions), yet if we are beyond

that formal realm, say worry about mistakes, one formal system is as good as

another. If we do not trust our checking the mathematical proof, then

the computer program may as well harbor mistakes (bugs). And basically,

checking one formal system relying on another is no ‘paradigm change’.

Another quote from my above article may be related (page 6, next):

“Note, that Godel’s Incompleteness Theorem is sometimes taken as denying

mathematics a totally formal/mechanical/suitable for computers character

(which it might have had Hilbert’s program succeeded), guaranteeing its

human/creative nature. Another cluster of mathematical ideas –

Computational Complexity Theory – as if counters this. A theorem of

length L whose shortest proof is of length more than, say, L^10 is practically not a

theorem for us, and proving theorems in the sense of finding a proof of

length not more than L^10 (if there is such a proof) is ‘just’ an

NP-complete problem, equivalent to any other NP-complete problem (such as

coloring a graph by 3 colors) if computation that takes polynomial time is

considered ‘easy’, something to do quickly by machine, in a sense ‘trivial’.

In this way mathematics becomes an afternoon riddle – coloring a graph, and

only the ‘hope’ that P \noteq NP prevents it from being trivial altogether in

the just mentioned sense. But one might ‘answer’ this (and let the

pendulum swing back to ‘human mathematics’) by noting that all this refers

to proof as a formal (indeed mathematical) entity, while the proofs that

mathematicians think, discuss and write are something different, ‘human

and unmathematical’. For example, an author of a mathematical article, or an

editor of a journal, endowed by results of Computational Complexity Theory

with an efficient formal way to check proofs written formally, still has to

check whether the formal version is really a rendering of the ‘informal’

ideas (so the formally-written proof may be found wrong though the ideas are

correct).”