11 ms·

Vladimir Voevodsky has died

397 points by slbenfica 9y ago

danharaj 9y ago
This is a massive loss for mathematics and the world :( 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.
- auggierose 9y ago
  It is. I wonder what this will mean for Homotopy Type Theory.
  - zitterbewegung 9y ago
    I think that people will still develop the theory. It still needs a bunch of work but it seems popular enough to stay around.
    - javra 9y ago
      Working in the field I rather have the feeling that it is slowly but surely falling asleep. One of Voevodsky's views was that all the foundation for a dependently typed formalization of maths is already there, and that it mainly needs to be organized in a better way (cf his unimath project).
- defen 9y ago
  That's two Fields Medalists taken entirely too early in the past 3 months (the other being Maryam Mirzakhani). Very sad.
  - deleted 9y ago
    [deleted]
SomeStupidPoint 9y ago
A great loss for mathematics! 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 9y ago
  Could you expand on his work, related to CS and/or his influence in your work? I've never heard of him so I'm curious, being a Field medalist and all.
  - deleted 9y ago
    [deleted]
  - danharaj 9y ago
    Voevodsky won the Fields medal for A^1 homotopy theory: https://en.wikipedia.org/wiki/A%C2%B9_homotopy_theory https://en.wikipedia.org/wiki/A%C2%B9_homotopy_theory It's quite technical to describe what that is, but the general idea is that he imported homotopy theory, a fundamental concept in mathematics which allows you to describe topology with an algebra of paths in that geometry, to algebraic geometry. This allowed him to solve some major open problems in the field. Topology is essentially the study of continuity and the properties that are invariant of objects under continuous deformation. The prototypical example of a topological space is the continuum although the concept of continuity has been generalized a great deal. Homotopy is the study of continuous paths which are defined as continuous functions from the unit interval into topological spaces, as well as higher dimensional "paths". It turns out that these paths have a rich algebraic structure which give you a strong idea of what the "shape" of the space is like. Classically algebraic geometry is the study of solutions to systems of polynomial equations over systems of numbers related to the integers, rationals, reals, and complex numbers. More modernly, it is the study of models of theories that resemble the previously mentioned theory in fundamental ways. For example, the theory of elliptic curves which underlies some of our modern cryptography is part of algebraic geometry.
grondilu 9y ago
That's young. What happened?
- cft 9y ago
  Suicide? Edit: I wonder why it is getting downvoted? I am actually about to quit HN due to its increasingly oppressive PC culture.
  - deleted 9y ago
    [deleted]
  - madez 9y ago
    It was also my first thought.
  - andrewflnr 9y ago
    You're getting downvoted because putting forward suicide as an explanation without any evidence is, well, "bad taste" doesn't really cut it. If you're going to speculate about it, at the very least give some justification.
    - cft 9y ago
      It's from a text from a friend who knew him, if that matters. We all got PhDs from the same school. I have been here for 6.8 years and in the last two I find myself going back to Slashdot more and more.
      - tomhoward 9y ago
        Your first comment didn't say anything about having a personal connection or any first-hand knowledge of the situation, so it was reasonable for people to consider the comment as empty, insensitive speculation. There are valid grounds for wishing that HN was better than it is, but this case doesn't epitomise anything that is fundamentally wrong with HN; you could have done better in your initial comment, and then done better than to use it as an opportunity to take a swipe at the entire community. For HN to be better, it relies on all of us to do our bit to make it better.
j-pb 9y ago
F*. This is an unfatomable loss both him as a amazing person and him as an outstanding mathematician. We just lost the Hilbert of the new Hilbert program.
tuxguy 9y ago
Does anyone know what happened ? Was he sick ? Was it cancer ?
- shivak 9y ago
  He struggled deeply with alcoholism, but the cause of his death has not been announced.
  - AnkhMorporkian 9y ago
    I cannot confirm this in any way, but one of my Russian friends told me he had Cirrhosis and was being treated for it.
  - downandout 9y ago
    It’s a frightening testament to the power of addiction that even some of the smartest, most logical people in the world cannot control some of their own extremely illogical decisions.
    - sillysaurus3 9y ago
      On the other hand, lacking proof this comment chain amounts to nothing more than a smear. "Vladimir Voevodsky alcohol" gives zero results. Can we let one person's death be a little respectful? Just once.
      - agumonkey 9y ago
        Just for the sake of it, I may say that first I understand your concern, but whatever takes away someone, might be a source of shame, disrespect or lack of care for the parent poster. Maybe the opposite even. Regards
      - dsacco 9y ago
        I think you're being pretty hyperbolic in your reaction here. A lot of people like to indulge in their morbid curiosity, and they're free to do so. If that means aimless speculation about the cause of someone's death as a means of rationalizing it then so be it. It's not really your place to be the arbiter of someone's death and others' reactions to it. A friend of mine died when he was only 24 due to a sudden brain aneurysm in his sleep, and in that same year I had two other friends commit suicide (in fairness one was questionable, but it was by a train). I grappled with that for well over a year, to the point that it caused me a great deal of anxiety and insomnia for someone apparently healthy to die that young. It fundamentally crushed a lot of my own personal sense of control and security. One of the most difficult things for me to process was the utter lack of information - how did he die? Did he have chronic headaches and didn't check? Is there a way I could consider him accountable for it? Something to understand the situation would give me greater closure than the reality that people simply die, sometimes quite suddenly, for no predictable reason at all. This is an extreme example for me to give, but the message is this: I understand that you're upset by this individual dying and the way others reacted to it (take a look at a comment I made here when John Nash died in a car accident in 2015: https://news.ycombinator.com/item?id=9597349 https://news.ycombinator.com/item?id=9597349). But what you're doing is policing other peoples' emotions, and they have a right to react to the death by speculating about its causes. That is a natural and very common response that you cannot artificially remove.
mathgenius 9y ago
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.)
- pandaman 9y ago
  The word is voevoda (воевода) and, indeed, originally meant "a general". https://en.wikipedia.org/wiki/Voivode https://en.wikipedia.org/wiki/Voivode
  - avenoir 9y ago
    It seems like the word "Voevoda", at least in Ancient Rus, was the highest military rank given to someone who exceled in very specific areas of warfare. For instance, the Voevoda of Defense (modern minister of defense?) would figure out how to fortify and defend a city from assault. Similarly, a Reconnaissance Voevoda would be sent to figure out the position and the size of an enemy. So it's not necessarily the general, although it looks like the highest class of Voevoda "Bolshoi Voevoda" or "Big Voevoda" could probably be compared to modern day Generals. I'm not entirely sure if one could progress up the ranks or if they just sort of branched out. Very interesting read here (in Russian) [1] [1] https://ru.wikipedia.org/wiki/воевода https://ru.wikipedia.org/wiki/воевода
    - int_19h 9y ago
      The description by your link is from the Tsardom period, by the time when the title already acquired a different meaning (more along generic administrative lines). In Ancient Rus, it was strictly a military rank, and simply meant "general" (or something roughly equivalent - a commander of a large military force, at the level where large-scale strategic considerations are as important as battlefield tactics).
- robotomir 9y ago
  >old russian words That word "voevoda" existed before Russians were even a thing.
dkural 9y ago
:( Such a huge loss to the world. What a terrible year, to lose such bright and young mathematicians.
robinhouston 9y ago
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. http://baaltii1.livejournal.com/198675.html 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.”
- gtt 9y ago
  I'm getting access denied on this entry. Could you copy-pase it somewhere else?
  - jlgaddis 9y ago
    Try this (may have to run it through Translate): http://archive.is/b4gHd http://archive.is/b4gHd
    - stepik777 9y ago
      Second part: http://archive.is/NtBiy http://archive.is/NtBiy
      - deleted 9y ago
        [deleted]
- 9y ago
carlob 9y ago
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.
- mathgenius 9y ago
  https://github.com/vladimirias https://github.com/vladimirias
monort 9y ago
Amusing anecdote from the life of Voevodsky (https://lj.rossia.org/users/tiphareth/2097217.html https://lj.rossia.org/users/tiphareth/2097217.html): 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.
- wolfgke 9y ago
  > It has to be said, that living and sleeping in the office is a terrible taboo and social stigma in America I am not a US-American, so can you elaborate?
  - aswanson 9y ago
    Not having a home in general is looked down upon here. Everyone is expected to have their place of work/study to be separate from the place where they bathe, sleep, etc.
    - patrickaljord 9y ago
      Any idea why it's frown upon though?
      - aswanson 9y ago
        My guess is that the US is a very individualistic, achievement, money-is-good, capitalistic place. Not owning a place to rest your head, being homeless, etc is associated with moral failure: laziness, lack of drive, addiction to drugs...
  - 9y ago
fermigier 9y ago
A great video interview of VV (2014) discussing his career, in english (subtitled in French) is available here: https://vimeo.com/99586217 https://vimeo.com/99586217 French transcription here: http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazette_142_87-94.pdf http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazet...
fermigier 9y ago
From http://www.mathunion.org/ICM/ICM2002.1/Main/icm2002.1.0099.0104.ocr.pdf http://www.mathunion.org/ICM/ICM2002.1/Main/icm2002.1.0099.0... (2002): "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...
marchdown 9y ago
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.
deleted 9y ago
[deleted]
cdetrio 9y ago
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] 1. https://nautil.us/issue/24/error/in-mathematics-mistakes-arent-what-they-used-to-be https://nautil.us/issue/24/error/in-mathematics-mistakes-are... 2. https://plato.stanford.edu/entries/russell-paradox/ https://plato.stanford.edu/entries/russell-paradox/ 3. https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-12 https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-... 4. https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/ https://www.quantamagazine.org/univalent-foundations-redefin... 5. https://www.ias.edu/sites/default/files/pdfs/publications/letter-2014-summer.pdf https://www.ias.edu/sites/default/files/pdfs/publications/le...
doall 9y ago
What a huge loss :( 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.
doall 9y ago
Comments from the members of Homotopy Type Theory - Google Groups. https://groups.google.com/forum/#!topic/homotopytypetheory/K_4bAZEDRvE https://groups.google.com/forum/#!topic/homotopytypetheory/K...

397 points by slbenfica 9y ago

This is a massive loss for mathematics and the world :( 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.

auggierose 9y ago
It is. I wonder what this will mean for Homotopy Type Theory.
- zitterbewegung 9y ago
  I think that people will still develop the theory. It still needs a bunch of work but it seems popular enough to stay around.
  - javra 9y ago
    Working in the field I rather have the feeling that it is slowly but surely falling asleep. One of Voevodsky's views was that all the foundation for a dependently typed formalization of maths is already there, and that it mainly needs to be organized in a better way (cf his unimath project).
defen 9y ago
That's two Fields Medalists taken entirely too early in the past 3 months (the other being Maryam Mirzakhani). Very sad.
- deleted 9y ago
  [deleted]

SomeStupidPoint 9y ago

A great loss for mathematics! 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 9y ago
Could you expand on his work, related to CS and/or his influence in your work? I've never heard of him so I'm curious, being a Field medalist and all.
- deleted 9y ago
  [deleted]
- danharaj 9y ago
  Voevodsky won the Fields medal for A^1 homotopy theory: https://en.wikipedia.org/wiki/A%C2%B9_homotopy_theory https://en.wikipedia.org/wiki/A%C2%B9_homotopy_theory It's quite technical to describe what that is, but the general idea is that he imported homotopy theory, a fundamental concept in mathematics which allows you to describe topology with an algebra of paths in that geometry, to algebraic geometry. This allowed him to solve some major open problems in the field. Topology is essentially the study of continuity and the properties that are invariant of objects under continuous deformation. The prototypical example of a topological space is the continuum although the concept of continuity has been generalized a great deal. Homotopy is the study of continuous paths which are defined as continuous functions from the unit interval into topological spaces, as well as higher dimensional "paths". It turns out that these paths have a rich algebraic structure which give you a strong idea of what the "shape" of the space is like. Classically algebraic geometry is the study of solutions to systems of polynomial equations over systems of numbers related to the integers, rationals, reals, and complex numbers. More modernly, it is the study of models of theories that resemble the previously mentioned theory in fundamental ways. For example, the theory of elliptic curves which underlies some of our modern cryptography is part of algebraic geometry.

grondilu 9y ago

That's young. What happened?

cft 9y ago
Suicide? Edit: I wonder why it is getting downvoted? I am actually about to quit HN due to its increasingly oppressive PC culture.
- deleted 9y ago
  [deleted]
- madez 9y ago
  It was also my first thought.
- andrewflnr 9y ago
  You're getting downvoted because putting forward suicide as an explanation without any evidence is, well, "bad taste" doesn't really cut it. If you're going to speculate about it, at the very least give some justification.
  - cft 9y ago
    It's from a text from a friend who knew him, if that matters. We all got PhDs from the same school. I have been here for 6.8 years and in the last two I find myself going back to Slashdot more and more.
    - tomhoward 9y ago
      Your first comment didn't say anything about having a personal connection or any first-hand knowledge of the situation, so it was reasonable for people to consider the comment as empty, insensitive speculation. There are valid grounds for wishing that HN was better than it is, but this case doesn't epitomise anything that is fundamentally wrong with HN; you could have done better in your initial comment, and then done better than to use it as an opportunity to take a swipe at the entire community. For HN to be better, it relies on all of us to do our bit to make it better.

j-pb 9y ago

F*. This is an unfatomable loss both him as a amazing person and him as an outstanding mathematician. We just lost the Hilbert of the new Hilbert program.

tuxguy 9y ago

Does anyone know what happened ? Was he sick ? Was it cancer ?

shivak 9y ago
He struggled deeply with alcoholism, but the cause of his death has not been announced.
- AnkhMorporkian 9y ago
  I cannot confirm this in any way, but one of my Russian friends told me he had Cirrhosis and was being treated for it.
- downandout 9y ago
  It’s a frightening testament to the power of addiction that even some of the smartest, most logical people in the world cannot control some of their own extremely illogical decisions.
  - sillysaurus3 9y ago
    On the other hand, lacking proof this comment chain amounts to nothing more than a smear. "Vladimir Voevodsky alcohol" gives zero results. Can we let one person's death be a little respectful? Just once.
    - agumonkey 9y ago
      Just for the sake of it, I may say that first I understand your concern, but whatever takes away someone, might be a source of shame, disrespect or lack of care for the parent poster. Maybe the opposite even. Regards
    - dsacco 9y ago
      I think you're being pretty hyperbolic in your reaction here. A lot of people like to indulge in their morbid curiosity, and they're free to do so. If that means aimless speculation about the cause of someone's death as a means of rationalizing it then so be it. It's not really your place to be the arbiter of someone's death and others' reactions to it. A friend of mine died when he was only 24 due to a sudden brain aneurysm in his sleep, and in that same year I had two other friends commit suicide (in fairness one was questionable, but it was by a train). I grappled with that for well over a year, to the point that it caused me a great deal of anxiety and insomnia for someone apparently healthy to die that young. It fundamentally crushed a lot of my own personal sense of control and security. One of the most difficult things for me to process was the utter lack of information - how did he die? Did he have chronic headaches and didn't check? Is there a way I could consider him accountable for it? Something to understand the situation would give me greater closure than the reality that people simply die, sometimes quite suddenly, for no predictable reason at all. This is an extreme example for me to give, but the message is this: I understand that you're upset by this individual dying and the way others reacted to it (take a look at a comment I made here when John Nash died in a car accident in 2015: https://news.ycombinator.com/item?id=9597349 https://news.ycombinator.com/item?id=9597349). But what you're doing is policing other peoples' emotions, and they have a right to react to the death by speculating about its causes. That is a natural and very common response that you cannot artificially remove.

mathgenius 9y ago

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.)

pandaman 9y ago
The word is voevoda (воевода) and, indeed, originally meant "a general". https://en.wikipedia.org/wiki/Voivode https://en.wikipedia.org/wiki/Voivode
- avenoir 9y ago
  It seems like the word "Voevoda", at least in Ancient Rus, was the highest military rank given to someone who exceled in very specific areas of warfare. For instance, the Voevoda of Defense (modern minister of defense?) would figure out how to fortify and defend a city from assault. Similarly, a Reconnaissance Voevoda would be sent to figure out the position and the size of an enemy. So it's not necessarily the general, although it looks like the highest class of Voevoda "Bolshoi Voevoda" or "Big Voevoda" could probably be compared to modern day Generals. I'm not entirely sure if one could progress up the ranks or if they just sort of branched out. Very interesting read here (in Russian) [1] [1] https://ru.wikipedia.org/wiki/воевода https://ru.wikipedia.org/wiki/воевода
  - int_19h 9y ago
    The description by your link is from the Tsardom period, by the time when the title already acquired a different meaning (more along generic administrative lines). In Ancient Rus, it was strictly a military rank, and simply meant "general" (or something roughly equivalent - a commander of a large military force, at the level where large-scale strategic considerations are as important as battlefield tactics).
robotomir 9y ago
>old russian words That word "voevoda" existed before Russians were even a thing.

dkural 9y ago

:( Such a huge loss to the world. What a terrible year, to lose such bright and young mathematicians.

robinhouston 9y ago

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. http://baaltii1.livejournal.com/198675.html 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.”

gtt 9y ago
I'm getting access denied on this entry. Could you copy-pase it somewhere else?
- jlgaddis 9y ago
  Try this (may have to run it through Translate): http://archive.is/b4gHd http://archive.is/b4gHd
  - stepik777 9y ago
    Second part: http://archive.is/NtBiy http://archive.is/NtBiy
    - deleted 9y ago
      [deleted]
9y ago

carlob 9y ago

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.

mathgenius 9y ago
https://github.com/vladimirias https://github.com/vladimirias

monort 9y ago

Amusing anecdote from the life of Voevodsky (https://lj.rossia.org/users/tiphareth/2097217.html https://lj.rossia.org/users/tiphareth/2097217.html): 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.

wolfgke 9y ago
> It has to be said, that living and sleeping in the office is a terrible taboo and social stigma in America I am not a US-American, so can you elaborate?
- aswanson 9y ago
  Not having a home in general is looked down upon here. Everyone is expected to have their place of work/study to be separate from the place where they bathe, sleep, etc.
  - patrickaljord 9y ago
    Any idea why it's frown upon though?
    - aswanson 9y ago
      My guess is that the US is a very individualistic, achievement, money-is-good, capitalistic place. Not owning a place to rest your head, being homeless, etc is associated with moral failure: laziness, lack of drive, addiction to drugs...
- 9y ago

fermigier 9y ago

A great video interview of VV (2014) discussing his career, in english (subtitled in French) is available here: https://vimeo.com/99586217 https://vimeo.com/99586217 French transcription here: http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazette_142_87-94.pdf http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazet...

fermigier 9y ago

From http://www.mathunion.org/ICM/ICM2002.1/Main/icm2002.1.0099.0104.ocr.pdf http://www.mathunion.org/ICM/ICM2002.1/Main/icm2002.1.0099.0... (2002): "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...

marchdown 9y ago

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.

deleted 9y ago

[deleted]

cdetrio 9y ago

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] 1. https://nautil.us/issue/24/error/in-mathematics-mistakes-arent-what-they-used-to-be https://nautil.us/issue/24/error/in-mathematics-mistakes-are... 2. https://plato.stanford.edu/entries/russell-paradox/ https://plato.stanford.edu/entries/russell-paradox/ 3. https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-12 https://en.wikipedia.org/wiki/Russell%27s_paradox#cite_note-... 4. https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/ https://www.quantamagazine.org/univalent-foundations-redefin... 5. https://www.ias.edu/sites/default/files/pdfs/publications/letter-2014-summer.pdf https://www.ias.edu/sites/default/files/pdfs/publications/le...

doall 9y ago

What a huge loss :( 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.

doall 9y ago

Comments from the members of Homotopy Type Theory - Google Groups. https://groups.google.com/forum/#!topic/homotopytypetheory/K_4bAZEDRvE https://groups.google.com/forum/#!topic/homotopytypetheory/K...