Voevodsky at the IAS on September 25, 2010, courtesy of the IAS
Just short of two weeks after Siobhan Roberts published her article in nautil.us about Voevodsky and Univalent Foundations, it was Kevin Hartnett’s turn at Quanta, with an article entitled
I didn’t do justice to Roberts’s article when I mentioned it in the middle of a post on René Thom. I neglected to mention, for example, that she demonstrates a wicked sense of humor in her very first paragraph, and that the whole text is a model of clarity and reads very well. But Hartnett’s article is of high quality as well, and unlike Roberts, Hartnett really focuses on the mathematics. Not only does he use the word “homotopy” repeatedly (and “groupoid,” and “simplicial set” — none of these words are in the nautil.us article) he even uses Quanta‘s animated graphics to show the reader what a homotopy is. There’s only one thing wrong with Hartnett’s article: he quotes me! This actually counts as two wrongs (which, as readers know, don’t make a right). First, I do remember being called by a Quanta fact-checker, who may have mentioned that I was going to be quoted in the article, and I probably did say more or less what I am quoted as saying, to wit:
“The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” [MH] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.”
But seriously, can anyone think of a more bland expression than “looking for something else?”
The second wrong is that I am obviously being presented as the token mathematician skeptical about this “redefining the roots of math.” I don’t mind being quoted, and I’m grateful for the publicity (which has so far had zero impact on sales of my book, as far as I can tell), but they could easily have found someone more qualified.
Urs Schreiber has referred to talk of computers in this context as a “distraction.” But for both Quanta and nautil.us, computers are the main attraction, and Voevodsky isn’t discouraging them from looking at HOTT/UF in that way. Hartnett’s article has Steve Awodey, Mike Shulman, and Dan Grayson on board with Voevodsky in favor of the new “roots of math.” I guess most readers who see the title will assume all three are no less in favor of Voevodsky’s vision of “formalizing mathematics on the computer.”
Those in the know, on the other hand, are already aware that the real intellectual action is taking place on this very blog, at this very minute in fact, in the comments to this post. Today the blog has already seen 1500 visitors, doubling the previous record. Almost half of them have been referred from (my Columbia colleague) Peter Woit’s “Not Even Wrong” blog. Peter made a perceptive observation when I mentioned this to him:
I do wonder though how much of the blog traffic these days is robots. In this case, perhaps some “proof assistants” have acquired the capability to do internet searches and are following the debate about themselves.