During grad school I had to spend a year at IAS, because my advisor was there on sabbatical.
The Institute is not very grad-student-friendly (by design): there are a lot of cultural and bureaucratic hurdles a student might find there, such as refusing any affiliation, both for visa and academic purposes, not offering proper office place, and a certain aloofness of the faculty.
My experience was a bit better than the norm at the then-new School for System Biology, but I have a lot of great memories of discussion with Voevodsky over lunch. He had found in me and another grad student from the same group two people interested in the use of computers in science, and he didn't care that we completely out of our depth discussing the foundations of mathematics. We were both just very interested in how computers were transforming science, and he kept telling us that the same revolution was going to happens for mathematics as well, despite the resistance of some of his colleagues.
These discussions sparked an interest I still have for proof verification, automatic theorem proving, and type systems.
Here's to hoping his legacy lives on and that the revolution he helped start brings on a new era in mathematics.
This interview (link below) gives some interesting insight into his work and motivations. It’s in Russian, but Google Translate does a pretty good job with it.
Among many other things, he describes some unusual experiences in 2006–7 that clearly had a powerful impact on his thinking:
[Translation by Google]
“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 can control. So I was not scared and did not feel sick, but perceived everything as something very interesting, actively trying to interact with those "creatures" in the auditorial, visual and then tactile spaces that appeared (themselves or by call) around me. I must say, probably, to avoid possible speculations 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.”
Thank you for posting this! I'm lucky to be able to read the interview in the original (for those who can't, google translate does a reasonable job). Part I: http://archive.is/b4gHd. Part II: http://archive.is/NtBiy.
Voevodsky was too lazy to search for an apartment, so he lived in his office (at Harvard each graduate student gets a personal office) and slept on the roof. Unfortunately, the windows of dean office (Willy Schmid) had direct view at that roof. Volodya didn't adhere to the usual day routine (and didn't adhere to anything at all), sometimes he slept during the dean office hours. Some day Schmid looked through the window and saw a roof and Voevodsky was sleeping at the roof. It has to be said, that living and sleeping in the office is a terrible taboo and social stigma in America, so Schmid was outraged. Voevodsky was almost expelled, but everything turned out well, though he was forced to rent an apartment and he has lived there from then on.
I was a grad student at Harvard... let me correct a few things. First, Wilfred Schmid would probably never be called Willy. It's a funny idea though. Like calling the Queen of England Lizzy. He wasn't the dean... he might have been the dept chair at the time. As for living/sleeping at the office -- it's not a "terrible taboo and social stigma in America". (I'm American). But it's not allowed due to problems with hygiene (no showers in most bathrooms), smell, clutter, disruption at odd hours, etc.. So it's not allowed in any workplace. When it happens, the response of most departments is sympathy and an effort to find the cause and find the person a place to live. And grad students at Harvard are financially supported well enough to afford a decent room in the area. I mean... I wasn't rich, but lived comfortably in apartments shared with a few other grad students.
"Among his main achievements are the following: he defined and developed motivic cohomology and the A1-homotopy theory of algebraic varieties; he proved the Milnor conjectures on the K-theory of fields."
Oh no! I was following his work closely and had high hopes for him delivering on his vision: type theory and constructive notion of equality not getting in the way of doing mathematics with computer, but helping us along. It will hopefully will be picked up by his collaborators.
Reading the story[1] about Voevodsky, I was reminded of how Bertrand Russell described Gottlob Frege as "almost superhuman":
> As I think about acts of integrity and grace, I realise that there is nothing in my knowledge to compare with Frege’s dedication to truth. His entire life’s work was on the verge of completion, much of his work had been ignored to the benefit of men infinitely less capable, his second volume was about to be published, and upon finding that his fundamental assumption was in error, he responded with intellectual pleasure clearly submerging any feelings of personal disappointment. It was almost superhuman and a telling indication of that of which men are capable if their dedication is to creative work and knowledge instead of cruder efforts to dominate and be known. [2]
And how rare it is to see such "exceptionally honest" academic dialogue as Frege's:
> Frege starts his analysis by this exceptionally honest comment : "Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr Bertrand Russell, just when the printing of this volume was nearing its completion" [3]
Voevodsky too, upon finding himself in the same position as Frege, reacted with a super-human level of integrity and intellectual honesty:
> In 1998, the American mathematician Carlos Simpson published a paper indicating there might be a mistake in Voevodsky and Kapranov’s 1990 result. For years Voevodsky sifted through the details without making much progress. He remained convinced the result was right. Then, in the autumn of 2013, as the leaves changed color and summer gave way to autumn, he made a breakthrough. Of sorts. He confirmed the error. The important result was no longer quite so important.
> “It is plainly wrong. The main theorem is incorrect,” he says. “It’s not that there is some gap in the proof. It’s that the main theorem is plainly wrong.” The mistake, he explains, was in failing to question the obvious. “We had proved that an assertion was indeed true in all of the difficult cases, but it turned out to be false in the simple case. We never bothered to check.” In confirming the error, he added an addendum to the original citation in his official publications list—“Warning: The main theorem of this paper was shown by Carlos Simpson to be false.” [1]
It is all the more remarkable that he spent years of working through painstaking details to prove to himself that he was wrong. And rather than quietly issuing a retraction, he shouted it from the rooftops, leading a heroic charge to get mathematicians to stop hand-waving with English-language proofs, and start writing code. [4]
> And I now do my mathematics with a proof assistant. I have a lot of wishes in
terms of getting this proof assistant to work better, but at least I don’t have to go
home and worry about having made a mistake in my work. I know that if I did
something, I did it, and I don’t have to come back to it nor do I have to worry
about my arguments being too complicated or about how to convince others that
my arguments are correct. I can just trust the computer. There are many people in
computer science who are contributing to our program, but most mathematicians
still don’t believe that it is a good idea. And I think that is very wrong.[5]
Univalent Foundations is apparently controversial. It appeared to come to a head a couple years ago when a lively debate played out in the comments of a blog (including a comment by Voevodsky himself): https://mathematicswithoutapologies.wordpress.com/2015/05/13...
I have been dreaming that one day we will have a fully developed type system for programming languages based on HoTT and I can develop a new language based on that.
Can we not? Do you think that they would have wanted the thread about their death to be filled with speculation about whether he killed himself or drank himself to death? No one knows anything, and even if they did it would be impolite to offer up that information.
> More recently he became interested in type-theoretic formalizations of mathematics and automated proof verification. He was working on new foundations of mathematics based on homotopy-theoretic semantics of Martin-Löf type theories. His new "Univalence Axiom" has had a dramatic impact in both mathematics and computer science.
And some of his online lectures outlining his reasoning and motivations became greatly influential on my own interests.
The name Voevodksy comes from two old russian words: vodit, which means "to lead", and voena which means war. So, voevod, would mean something like "war leader", or general. (Source: russian friend that I just consulted.)
In Polish, there is the word "wojewoda" (Polish uses "w" where in English or Latin languages you would use a "v"). Historically it meant the same as in Russian, but nowadays it is the title of the governor of a province.
To make things even more interesting, Poland is actually divided in regions / provinces called "województwa" (plural), or literally "lands that belong to the wojewoda". A "województwo" (singular) is more or less the equivalent of a German "Land" or US American "states".
[+] [-] carlob|8 years ago|reply
The Institute is not very grad-student-friendly (by design): there are a lot of cultural and bureaucratic hurdles a student might find there, such as refusing any affiliation, both for visa and academic purposes, not offering proper office place, and a certain aloofness of the faculty.
My experience was a bit better than the norm at the then-new School for System Biology, but I have a lot of great memories of discussion with Voevodsky over lunch. He had found in me and another grad student from the same group two people interested in the use of computers in science, and he didn't care that we completely out of our depth discussing the foundations of mathematics. We were both just very interested in how computers were transforming science, and he kept telling us that the same revolution was going to happens for mathematics as well, despite the resistance of some of his colleagues.
These discussions sparked an interest I still have for proof verification, automatic theorem proving, and type systems.
Here's to hoping his legacy lives on and that the revolution he helped start brings on a new era in mathematics.
[+] [-] mathgenius|8 years ago|reply
[+] [-] robinhouston|8 years ago|reply
http://baaltii1.livejournal.com/198675.html
Among many other things, he describes some unusual experiences in 2006–7 that clearly had a powerful impact on his thinking:
[Translation by Google] “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 can control. So I was not scared and did not feel sick, but perceived everything as something very interesting, actively trying to interact with those "creatures" in the auditorial, visual and then tactile spaces that appeared (themselves or by call) around me. I must say, probably, to avoid possible speculations 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.”
[+] [-] coffeemug|8 years ago|reply
Well worth reading.
[+] [-] gtt|8 years ago|reply
[+] [-] monort|8 years ago|reply
Voevodsky was too lazy to search for an apartment, so he lived in his office (at Harvard each graduate student gets a personal office) and slept on the roof. Unfortunately, the windows of dean office (Willy Schmid) had direct view at that roof. Volodya didn't adhere to the usual day routine (and didn't adhere to anything at all), sometimes he slept during the dean office hours. Some day Schmid looked through the window and saw a roof and Voevodsky was sleeping at the roof. It has to be said, that living and sleeping in the office is a terrible taboo and social stigma in America, so Schmid was outraged. Voevodsky was almost expelled, but everything turned out well, though he was forced to rent an apartment and he has lived there from then on.
[+] [-] ynotyman|8 years ago|reply
[+] [-] wolfgke|8 years ago|reply
I am not a US-American, so can you elaborate?
[+] [-] j-pb|8 years ago|reply
We just lost the Hilbert of the new Hilbert program.
[+] [-] danharaj|8 years ago|reply
Although I've never met him, I've been strongly influenced by his writings and contributions to math, especially his down to earth blog posts.
[+] [-] defen|8 years ago|reply
[+] [-] auggierose|8 years ago|reply
[+] [-] fermigier|8 years ago|reply
"Among his main achievements are the following: he defined and developed motivic cohomology and the A1-homotopy theory of algebraic varieties; he proved the Milnor conjectures on the K-theory of fields."
Quite an achievement, indeed...
[+] [-] fermigier|8 years ago|reply
French transcription here: http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazet...
[+] [-] marchdown|8 years ago|reply
[+] [-] doall|8 years ago|reply
https://groups.google.com/forum/#!topic/homotopytypetheory/K...
[+] [-] dkural|8 years ago|reply
[+] [-] cdetrio|8 years ago|reply
> As I think about acts of integrity and grace, I realise that there is nothing in my knowledge to compare with Frege’s dedication to truth. His entire life’s work was on the verge of completion, much of his work had been ignored to the benefit of men infinitely less capable, his second volume was about to be published, and upon finding that his fundamental assumption was in error, he responded with intellectual pleasure clearly submerging any feelings of personal disappointment. It was almost superhuman and a telling indication of that of which men are capable if their dedication is to creative work and knowledge instead of cruder efforts to dominate and be known. [2]
And how rare it is to see such "exceptionally honest" academic dialogue as Frege's:
> Frege starts his analysis by this exceptionally honest comment : "Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr Bertrand Russell, just when the printing of this volume was nearing its completion" [3]
Voevodsky too, upon finding himself in the same position as Frege, reacted with a super-human level of integrity and intellectual honesty:
> In 1998, the American mathematician Carlos Simpson published a paper indicating there might be a mistake in Voevodsky and Kapranov’s 1990 result. For years Voevodsky sifted through the details without making much progress. He remained convinced the result was right. Then, in the autumn of 2013, as the leaves changed color and summer gave way to autumn, he made a breakthrough. Of sorts. He confirmed the error. The important result was no longer quite so important.
> “It is plainly wrong. The main theorem is incorrect,” he says. “It’s not that there is some gap in the proof. It’s that the main theorem is plainly wrong.” The mistake, he explains, was in failing to question the obvious. “We had proved that an assertion was indeed true in all of the difficult cases, but it turned out to be false in the simple case. We never bothered to check.” In confirming the error, he added an addendum to the original citation in his official publications list—“Warning: The main theorem of this paper was shown by Carlos Simpson to be false.” [1]
It is all the more remarkable that he spent years of working through painstaking details to prove to himself that he was wrong. And rather than quietly issuing a retraction, he shouted it from the rooftops, leading a heroic charge to get mathematicians to stop hand-waving with English-language proofs, and start writing code. [4]
> And I now do my mathematics with a proof assistant. I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don’t have to go home and worry about having made a mistake in my work. I know that if I did something, I did it, and I don’t have to come back to it nor do I have to worry about my arguments being too complicated or about how to convince others that my arguments are correct. I can just trust the computer. There are many people in computer science who are contributing to our program, but most mathematicians still don’t believe that it is a good idea. And I think that is very wrong.[5]
1. https://nautil.us/issue/24/error/in-mathematics-mistakes-are...
2. https://plato.stanford.edu/entries/russell-paradox/
3. https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-...
4. https://www.quantamagazine.org/univalent-foundations-redefin...
5. https://www.ias.edu/sites/default/files/pdfs/publications/le...
[+] [-] cdetrio|8 years ago|reply
[+] [-] doall|8 years ago|reply
I have been dreaming that one day we will have a fully developed type system for programming languages based on HoTT and I can develop a new language based on that.
[+] [-] tuxguy|8 years ago|reply
Was he sick ? Was it cancer ?
[+] [-] shivak|8 years ago|reply
[+] [-] sillysaurus3|8 years ago|reply
He was a great mathematician. RIP.
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] SomeStupidPoint|8 years ago|reply
I became familiar with his work through HoTT --
> More recently he became interested in type-theoretic formalizations of mathematics and automated proof verification. He was working on new foundations of mathematics based on homotopy-theoretic semantics of Martin-Löf type theories. His new "Univalence Axiom" has had a dramatic impact in both mathematics and computer science.
And some of his online lectures outlining his reasoning and motivations became greatly influential on my own interests.
[+] [-] saganus|8 years ago|reply
I've never heard of him so I'm curious, being a Field medalist and all.
[+] [-] mathgenius|8 years ago|reply
[+] [-] iagooar|8 years ago|reply
To make things even more interesting, Poland is actually divided in regions / provinces called "województwa" (plural), or literally "lands that belong to the wojewoda". A "województwo" (singular) is more or less the equivalent of a German "Land" or US American "states".
[+] [-] pandaman|8 years ago|reply
[+] [-] robotomir|8 years ago|reply
That word "voevoda" existed before Russians were even a thing.
[+] [-] grondilu|8 years ago|reply
[+] [-] cft|8 years ago|reply
[deleted]