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

## Will Computers Redefine the Roots of Math?

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.

Asaf KaragilaThe slide in the photo caused me to raise an eyebrow.

Is first-order arithmetic the only viable thing that we can use? I can prove the consistency of PA just easily, using ZFC. I can prove the consistency of ZFC just fine, using ZFC+inaccessible cardinal. I can prove the consistency of … Okay, you get my point.

Just like the axiom “There are two elements” is neither provable, nor disprovable, from the empty theory (in whatever language), we need to acknowledge that provability and truth are two different things. And then do one of the following:

If someone wants to assume a Platonist approach, then they should remember that axioms tells us what we can ensure is true. If you believe PA is consistent, then you should work in the theory PA+Con(PA) and not just PA. If you believe that theory is consistent as well you should extend that. It makes zero sense to me how a Platonist will not work in a “maximally consistent” theory that they can find (not necessarily maximal in the mathematical sense; just throw in all the statements you believe are true). And if this means that your axioms are not recursively enumerable anymore… tough cookie. But if you are a Platonist, and you believe certain things to be true in the universe, I don’t know why someone like that would not insist to add them as standard assumptions to their work.

(And if a Platonist still wants to work with something “weaker than true”, then they should accept the fact that provability need not be equal to truth, just a subset thereof.)

If someone does not want to assume the Platonist approach, then there is no problems to go from one universe of mathematics to another. One where ZFC is inconsistent, another one where it is consistent, other universes which have these properties and those properties. And then “transcendental knowledge” is a meaningless statement, because it implicitly assumes some sort of absolute truth. Then it’s not an issue to work in a mathematical universe which is a model of PA, or work in a mathematical universe which is a model of ZFC.

(One of the nicer things about the foundations of set theory, is that despite the fact we often work with large cardinals and transitive models of set theory and so on; all the formal arguments can be reduced back to some weak system of arithmetic. So if you don’t believe in a mathematical universe of sets, you can still talk about “these axioms prove those axioms” or “the consistency of these axioms implies the consistency of those axioms” in a very weak fragment of arithmetic.)

If someone wants to be a formalist, then the entire slide makes no sense. PA cannot derive a certain statement, moving on.

There is one thing that I neglected here, perhaps due to my affinity towards classical logic. If someone is a Platonist, but does not believe that every statement is either true or false, then the slide doesn’t make sense either. Since again, provability implies truth, but none of the three options allow some sort of “neither true nor false” option.

In either case, the slide should be raising more eyebrows. Not just mine.

LikeLiked by 1 person

Mike ShulmanMy eyebrows are up with yours.

(Although I don’t see why set theory would be special among foundations in that its consistency statements can be reduced back to weak fragments of arithmetic.)

LikeLike

Mike ShulmanYes, by focusing entirely on Voevodsky and his dedication to computerizing math, it gives an inaccurate impression of the field. It doesn’t even mention the HoTT Book! This distortion is also evident in Roberts’ article. Score one for “charisma” and against democracy and truth.

The first few paragraphs also give a

seriouslymisleading picture of Awodey’s role. In fact, he and his students had proved important theorems in the subject before they had any contact with Voevodsky, and he played a much larger role in the special year at IAS.LikeLike

mathematicswithoutapologiesPost authorMike, you have put your finger on a very interesting feature of democracy in mathematics, namely that it stops at the gates of institutions like the IAS. It’s inconceivable that the IAS would have devoted an entire year to HOTT on its perceived merits alone, without the full support of an Institute Professor. I think this would be true even if HOTT/UF were a long-established field. I don’t particularly approve of this state of affairs, but if I had to choose between charisma and branding I’m pretty sure I would pick the former in most circumstances.

Whether there is “truth” outside the history recorded by journalists is another interesting question. I happen to know that two ambitious and talented young historians of mathematics are following this blog, and I wonder what they make of your point on “truth.”

LikeLike

Mike ShulmanDon’t get me wrong; I’m grateful for all that Voevodsky’s charisma has done for the field, including the IAS year. I don’t really know whether there are more democratic methods of organizing mathematics that would be as or more effective than the current dependence on charismatic leaders; it seems related to the search for alternative models for recognizing and validating research that could replace the current referee and journal publication system.

What bugs me is when people assume that because of Voevodsky’s charisma, that his interests define the field, or that the rest of us are all following his “research programme”. I used to find such assumptions totally baffling; but after reading chapter 2 of your book, I get the impression that there are fields of mathematics in which it really is the case that the “big name” mathematicians set out “research programmes” that everyone else is expected to follow. It’s not at all what my experience in mathematics has been like (including work in algebraic topology, category theory, and now homotopy type theory), but maybe the problem is that people from fields that do work that way assume that all fields work that way. Or did I mis-read chapter 2?

LikeLike

mathematicswithoutapologiesPost authorMike, I have thought about these questions quite a lot, and I’ll come back with a long answer in a few days, after I have struggled with the kind of higher category theory I’ll need to follow Dennis Gaitsgory’s talk on Thursday. The questions are at the heart of chapter 2, although the main theme of that chapter is anti-epistemological — that philosophy of mathematics should follow rather than precede its sociology. Your reading is not wrong (and I’m delighted you decided to read at least chapter 2) but I have the strong impression that the dominant institutions remain hierarchical, regardless of the field. My sympathies are naturally with the kind of revolution that would make mathematics more democratic; but then I wonder what would happen to the value system.

As I said, there will be more in a few days. Anyway, I’m planning a series about charisma. One thing I regret about Chapter 2 is that it apparently leaves the impression that mathematics is highly competitive; I should have added (maybe I already wrote this) that it’s also the most cooperative of the academic disciplines.

LikeLike

Pingback: This is what charisma looks like, part 3: Is mathematics democratic? | Mathematics without Apologies, by Michael Harris

Pingback: Mathematics without Apologies, by Michael Harris

Pingback: Is the Continuum Hypothesis a definite problem? | Asaf Karagila