(p. A12) Vladimir Voevodsky, formerly a gifted but restless student who flunked out of college out of boredom before emerging as one of the most brilliant and revolutionary mathematicians of his generation, died on Sept. 30 [2017] at his home in Princeton, N.J. He was 51.
. . .
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.
. . .
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.”
For the full obituary, see:
JULIE REHMEYER. “Vladimir Voevodsky, Dropout Turned Revolutionary Mathematician, Dies at 51.” The New York Times (Sat., OCT. 7, 2017): A12.
(Note: ellipses, and bracketed year, added.)
(Note: the online version of the obituary has the date OCT. 6, 2017, and has the title “Vladimir Voevodsky, Revolutionary Mathematician, Dies at 51.”)