“If you want to ask how profound his work is, that’s how profound it is,” Dr. Hales said. “It changes the very meaning of what the equals sign means in mathematics.”
He added: “His ideas gave a new way for all mathematicians to do what they do, a new foundation. The foundations of math are like a constitutional document that spells out the governing rules all mathematicians agree to play by. He has given us a new constitution.”
Vladimir Voevodsky was born in Moscow on June 4, 1966. His father, Alexander, directed a laboratory in experimental physics at the Russian Academy of Sciences; his mother, Tatyana Voevodskaya, was a chemistry professor at Moscow University.
Vladimir was kicked out of high school three times, once for disagreeing with his teacher’s assertion that Dostoyevsky, who died in 1881, was pro-Communist. He was also kicked out of Moscow University after failing academically, having stopped attending classes that he considered a waste of time.
He continued to study mathematics independently, however, and with the mathematician Mikhail Kapranov he published several papers so impressive that he was invited to enroll at Harvard as a graduate student, despite never having applied for admission there and holding no formal undergraduate degree.
Once enrolled he again failed to attend lectures — but his body of research was so astonishing, colleagues said, that no one cared. He graduated in 1992 and remained at Harvard to do a fellowship. In 2002 he moved to the Institute for Advanced Study in Princeton, where he spent the rest of his career.
Dr. Voevodsky was awarded the Fields Medal for his discovery of an elusive mathematical object whose existence had been predicted decades earlier. The object provides a sort of mathematical wormhole that allows powerful theoretical tools in one field of mathematics to be pulled through and used in another. He then used those tools to crack a three-decade-old puzzle, giving birth to an entirely new area of mathematics called motivic homotopy theory.
Soon afterward, however, he abandoned that branch of mathematics for what was perhaps a more quixotic quest, to find the answer to a fundamental question: How do mathematicians know that something they prove is actually true?
This question became urgent for him as mathematicians were discovering — sometimes decades after publication — that proof after proof, including one of his own, had critical flaws.
Mathematical arguments had gotten so complicated, he realized, that other mathematicians rarely checked them in detail. And his stellar reputation only made the problem worse: Everyone assumed that his proofs must be right.
Dr. Voevodsky realized that human brains could not keep up with the ever-increasing complexity of mathematics. Computers were the only solution. So he embarked on an enormous project to create proof-checking software so powerful and convenient that mathematicians could someday use it as part of their ordinary work and create a library of rock-solid mathematical knowledge that anyone in the world could access.
Computer scientists had worked on the problem for decades, but it was territory only a few mathematicians had ever ventured into. “Among mathematicians, computer proof verification was almost a forbidden subject,” Dr. Voevodsky wrote.
The problem was that these systems were extraordinarily cumbersome. Checking a single theorem could require a decade of work, because the computer essentially had to be taught all of the mathematics a proof was built on, in agonizing, inhuman detail. Ordinary mathematicians intent on expanding the borders of the field could not possibly devote that kind of effort to checking their proofs.
Somehow, computers and humans needed to be taught to think alike.
Dr. Voevodsky developed a stunningly bold plan for how to do so: He reformulated mathematics from its very foundation, giving it a new “constitution,” as Dr. Hales put it. Mathematics so reformulated would be far friendlier to computers and allow mathematicians to talk to computers in a language that was much closer to how mathematicians ordinarily think.
Today, Dr. Voevodsky declared in 2014, “computer verification of proofs, and of mathematical reasoning in general, looks completely practical.”
Further, Dr. Voevodsky integrated the computer into the process of doing his own research, describing it as a bit like a video game. “You tell the computer, ‘Try this,’ and it tries it, and it gives you back the result of its actions,” he said in an interview with Scientific American in 2013. “Sometimes it’s unexpected what comes out of it. It’s fun.”
Dr. Voevodsky was at the center of an informal but enormous effort to fulfill his vision, having inspired dozens of researchers to join it. “He’s been our leader, even though he lets everybody do whatever they want,” said Robert Harper of Carnegie Mellon University in Pittsburgh. “He’s this inspirational and spiritual leader by example.”
Dr. Voevodsky was especially attentive to young mathematicians. “By being accommodating, encouraging, listening to people, he generated enormous interest,” Dr. Harper said in a telephone interview.
He also nurtured deep interests in many other fields, including biology, politics and nature photography.
Besides Dr. Shalaby, he is survived by their two daughters, Diana Yasmine Voevodsky and Natalia Dalia Shalaby.
Chris Kapulkin, another colleague, at the University of Western Ontario, said of Dr. Voevodsky in an interview, “His contributions are so fundamental that it’s impossible to imagine how things were thought of before him.”
Continue reading the main story