It’s clear to me that, in spite of the best of intentions, this has been mainly a dialogue of the deaf, much like the situation described in this post, which in spite of its name is definitely part of this thread. It can be characterized as a dialogue between one group who are convinced that mathematics is ripe for a conceptual revolution or paradigm shift, which would take the form of adoption of new foundations, and a second group who see no need for such a revolution. The dialogue is complicated by the fact that the overwhelming majority of the members of the first group come from programming or proof theory, and by the fact that the overwhelming majority of mathematicians are completely indifferent to the proposed new foundations.

I would draw your attention to the irony of the fact that I have been the target of a variety of reactions, ranging from abuse to well-meaning attempts at explanation of matters about which I have already written at length; and this because, unlike the overwhelming majority of my colleagues, I am talking and writing about the new proposals rather than dismissing them out of hand. I naturally anticipated that by speaking out I would be making myself a target, simply because it’s easier to talk back (to kill the messenger, so to speak) to someone who is paying attention than to someone who is ignoring you.

So let me explain that, while I am naturally curious about new intellectual developments and while I anticipate that this new research program will have very interesting consequences, which may or may not have anything to do with “Foundations,” the arguments put forward in support of the new movement are essentially irrelevant to my practice as a mathematician — except in one important way, which I will explain below. If you want to know what factors I do consider relevant to my research, I’m afraid you’ll have to read my book; they are not easy to summarize and they don’t fit into a neat logical sequence.

Here’s a passage in my book in which I quote Mike Shulman.

“I never would have guessed,” wrote Mike Shulman in 2011, “that

thecomputerization of mathematics would be best carried out… by an enrichment of mathematics” [my emphasis] along the lines of Voevodsky’s univalent foundations project, to which Shulman is an active contributor.I italicized the definite article in the Shulman quotation to emphasize how mechanization of mathematics — with or without human participation in the long term — is viewed in some circles as inevitable. To my mind, the fixation on mechanical proof checking is less interesting as a reminder that standards of proof evolve over time, which is how it’s usually treated by philosophers and sociologists, than as a chapter in the increasing qualification of machines as sources of validation, to the detriment of human rivals. In Yevgeny Zamyatin’s novel

We, whose protagonist is a mathematician named D-503, the scourge of human subjectivity — what virtual reality pioneer Jaron Lanier calls “the unfathomable penumbra of meaning that distinguishes a word in natural language from a command in a computer program” — is ultimately eliminated by an X-ray operation that turns people into machines.

Here is a dangerously oversimplified model of scientific revolution: In the absence of external forces (like the *mission civilisatrice* to which I allude in the last post) a scientific revolution takes place as a response to a crisis. Voevodsky’s article made it clear that he perceived the need for new foundations in response to a contemporary crisis in the verification of mathematical proofs. I respect both his perception and his response, but very few of my colleagues share that perception. To express “surprise” or “disappointment” that this is the case is to display a fundamental misunderstanding of the sociology of mathematical practice. And if you are not actually a mathematician, I’m not sure that “disappointment” with the attitudes of mathematicians is an appropriate reaction, even if you are Plato.

The notion of revolution may be broadened to include radical innovations like Grothendieck’s new (small f) foundations of algebraic geometry, or even important innovations that largely remain within an established framework, like derived algebraic geometry or Scholze’s perfectoid geometry. In striking contrast to HOTT/UF, these have been adopted eagerly and rapidly by highly motivated groups of mathematicians all over the world. Surely there is a sociological lesson in this contrast, for those willing to see it?

To make my own motivations clear, in my book I treated projects to mechanize mathematics, including (one aspect of) HOTT/UF, as one of two “proposals for reconfiguration” that challenge “the professional autonomy to which we have grown attached.” The other one is the pressure to subordinate pure research to an “entrepreneurial mindset.” The book briefly mentions a possible convergence between these proposals: if the providers of the material conditions — the “external goods” — on which mathematics depends become convinced (1) that this is only necessary because of eventual commercial or industrial spinoffs and (2) that computers can provide these spinoffs more reliably than pure researchers, then the future of pure research in mathematics is by no means guaranteed.

From this perspective, one is entitled to wonder whether the conscious or unconscious intention of mathematicians and computer scientists who argue along the lines of point (2) above isn’t to redirect some of the limited supply of “external goods” from pure mathematics to automated proof. I don’t know anyone who is actually arguing for such a shift, of course. But it’s easy to imagine that it would be welcomed by decision-makers, and rationalized as progress in Silicon Valley.

A.G.I find your conclusion very interesting. As a side remark, I know some computer scientists working on “applied” formal methods/proofs (e.g., for software safety) feel that the HoTT/UF “buzz” is an attempt from pure(r) mathematicians to get a slice of the CS funding pie.

LikeLike

Mike ShulmanI don’t agree. I would say that the homotopy-theoretic revolution, to whatever extent there is or was one, has essentially already happened, with the work of Grothendieck through Lurie and everyone before, in between, and after. HoTT/UF, to whatever extent it were adopted as new foundations, would be only a natural outgrowth of that; it would have interesting implications for foundations and philosophy, but there’s no reason to expect it to cause significant changes to everyday mathematics, which the word “revolution” implies. I feel as though you are “looking for a fight”, maybe because it would be interesting to write about, and so you see a conflict where there isn’t one. (I’m not saying that that’s what you

aredoing, just that that’s how itfeelsto me.)In particular, the fact that the overwhelming majority of mathematicians are indifferent to HoTT/UF as a “new foundation” is exactly as it should be, because if a foundation is to be worthy of the name, it should suffice as a foundation for

existing mathematics, and the world of HoTT/UF includes a world of familiar sets that is a home for existing mathematics. If HoTT/UF has an advantage as a foundation, it is to make certain things more possible or convenient; but it’s perfectly natural that most mathematicians, who never want or need to do those certain things, will be indifferent to whether their sets “live inside” HoTT/UF or are those of ZFC or ETCS (or even aren’t formalized at all).LikeLiked by 1 person

mathematicswithoutapologiesPost authorIn this post it sounds like you’re in the second group. The first group does exist as a body of quotations. Some of them can be found in earlier comments on Parts 1 and 2 (I’m sorry, I don’t know how to link to them in this format). Some are in my book. I have also seen enough remarks about “transforming the way mathematics is done” in the course of my research on mechanizing mathematics to know that I’m not making it up. And Voevodsky (who has not participated in this blog) has several times stated his hope that the new foundations will change mathematics. Maybe the connection between mechanization of mathematics and HOTT is not so strong. We’ll see. In the meantime, I have no doubt that mechanized mathematics is more consistent than human mathematics with the “market rationality” whose development as a model for universities has been the subject of hundreds of books and articles by colleagues in the humanities and social sciences but which scientists seem largely to have ignored.

LikeLike

Mike ShulmanThe date displayed underneath the author of a comment is a “permalink” to that comment. So you can right-click on it and “Copy link location”, then paste it into a new comment with a link like <a href=”PASTE HERE”>link text</a>.

Since I haven’t read your book and you’ve declined to explain on the blog anything that’s discussed in the book, I don’t know exactly what you mean by “mechanized mathematics”. But I do think it’s important to distinguish, as has been pointed out elsewhere, between proof

checkingand prooffinding.LikeLike

Mike ShulmanI also disagree that I can be put in your second group. To me, saying that the second group “see no need for such a revolution” implicitly implies an acceptance that what the first group is proposing

isa revolution, together with a belief that there is no need for it. What I’m saying is that I don’t think the proposal is for a revolution at all.LikeLike

mathematicswithoutapologiesPost authorFrom the Flyspeck Project Fact Sheet:

“A formal proof is understood in the sense of the QED manifesto”

From the QED Manifesto:

“[P]erhaps the foremost motivation for the QED project is cultural. Mathematics is arguably the foremost creation of the human mind . . . one of the most basic things that unites all people, and helps illuminate some of the most fundamental truths of nature, even of being itself. In the last one hundred years, many traditional cultural values of our civilization have taken a severe beating, and the advance of science has received no small blame. . . . The QED system will provide a beautiful and compelling monument to the fundamental reality of truth. It will thus provide some antidote to the degenerative effects of cultural relativism and nihilism.”

Again from the Flyspeck Project Fact Sheet:

“We are looking for mathematicians (from the advanced undergraduate level up) who are computer literate, and who are interested in transforming the way that mathematics is done.”

From an article by Maggesi and Simpson:

“[A]re we most interested in creating proofs which are readable by the human reader? or are we most interested in creating, as quickly and easily as possible, true proofs that are verified by the computer and which we don’t subsequently care about? . . . [W]e feel that the greatest benefits will come from the second approach.”

(All of this can be found in my Androids article or in my book, by the way.)

Now I have the utmost respect for Tom Hales, and (from my very remote vantage point) I think the Flyspeck Project is terrific. But that sounds like pretty revolutionary talk to me, and anyone who writes a Manifesto has revolution on the mind.

LikeLike

Mike ShulmanExactly what dichotomy are you talking about, in your description of the dialogue of two groups? Are you talking about HoTT/UF, or are you talking about computer-formalized proof? I thought you were talking about HoTT/UF, since the previous posts in this series have been about that, and since you specifically mentioned the people in the first group as talking about adoption of new foundations.

LikeLike

Gershom BIt seems worthwhile to address this: “I have no doubt that mechanized mathematics is more consistent than human mathematics with… ‘market rationality'” since it seems at the heart of your concerns.

We can perhaps look at the field of computer science for a case study. Increasingly, and people are proud of this, at the major “Theory B” (models / semantics / logic / programming languages) conferences, more papers come with some form of verifiable machine-checked artifact. However, these are considered _supplemental_ to the papers, and also _supplemental_ to the presentations, both of which are designed for people to understand and in which communication, humor, and clarity of exposition is highly valued. These formal developments are largely not designed to replace human understanding, but to provide checks against significant mistakes being made, or even insignificant ones that could still impede human understanding.

A very nice example is the “Run Your Research” paper from POPL 2012, in which a team took 9 papers from POPL 2009, and encoded them in a system for lightweight verification — not proving them correct, but rather running randomized tests against them and attempting to invalidate them. They found errors in all 9 papers. Of these, one described a result fully proved in Agda — the error the team found was introduced in the transliteration into the paper. Another described a result proved in Coq with the exception of one section. In that section they found two (repairable) errors.

In this sort of work I don’t even begin to see any sort of tension between the use of machines and traditional human creative endeavor. Rather, we just see machines as tools to help people be precise when they want to be.

Perhaps if we think of these various automated tools not as “androids” or the like, but just overgrown calculators, that might help. After all, nobody concerns themselves much if in the course of a proof they need to multiply two large numbers and reach for their HP rather than doing it by hand. Doing this for rather more complex problems seems to me more a difference of degree rather than kind. And — in fact, though number theory is not my thing at all, I am under the impression that a fair amount of people do use systems such as sage and mathematica to grind out various calculations to help them in their work. So one can see the use of formal verification even there — if just to assure us that these systems actually do what they are claiming to.

LikeLike

mathematicswithoutapologiesPost authorThere is a massive literature on the introduction of management principles into universities and research evaluation; I quote some of that in my book, and Chapter VI of Wendy Brown’s book, which will be the focus of my next post, summarizes quite a lot of it. On the other hand, there is a no less massive literature about the future of AI and what it means for production and culture more generally. I’ve already quoted Jaron Lanier’s

Who Owns the Futureseveral times; as he tells it, much of Silicon Valley is convinced that their innovations have made the species obsolete. My scenario is consistent with long-term international trends in higher education and research and is far less apocalyptic than what some of our farsighted West Coast billionaires envision. And of course, it is consistent with these prescient words written more than 150 years ago:The bourgeoisie has stripped of its halo every

occupation hitherto honoured and looked up to with

reverent awe. It has converted the physician, the

lawyer, the priest, the poet, the man of science,

into its paid wage labourers.

or

All fixed, fast-frozen relations, with their

train of ancient and venerable prejudices and

opinions, are swept away, all new-formed ones

become antiquated before they can ossify. All that

is solid melts into air, all that is holy is profaned,

and man is at last compelled to face with

sober senses his real conditions of life, and his

relations with his kind.

I’m sure the colleagues who invented elliptic-curve cryptography didn’t expect to put independent bookstores and record stores out of business and to give increasing control over publishing and music to a few high-tech companies, but that’s what happened.

LikeLike

mathematicswithoutapologiesPost authorI’m sorry, I haven’t learned HTML (or any other programming language since I was in high school), so I’m not able to follow your suggestion. I’m sure that, in the minds of some readers of this blog, this disqualifies me to speak about any topic whatsoever. But I can direct you, as I believe I have already done once for someone, to the article mentioned on the right-hand side of this page, which you can read at

http://webusers.imj-prg.fr/~michael.harris/androids.pdf

It’s also discussed on pp. 65-68 of the book. I don’t understand what you mean by declining to explain anything that’s discussed in the book. Everything I write here is about the book. I hope you will forgive me for being less than forthcoming when asked to rewrite off the top of my head what I spent three years researching.

I understand the difference between proof-checking and proof-finding; I write about it in the (pre-HOTT) article referenced above. I also understand that Voevodsky doesn’t speak for everyone; but I suppose he’s not completely isolated. Moreover, Ian Hacking portrays him as a paradigmatic Leibnizian mathematician in his book “Why is There Philosophy of Mathematics at All?”

Finally, although you may find this hard to believe, I am MUCH MORE sympathetic to this project than just about any of the number theorists I know.

LikeLike

Mike ShulmanYou don’t actually need to know any HTML to use my suggestion; just copy-and-paste it and replace the text PASTE HERE with the URL. You can also just paste the URL itself into the comment, as you did with the URL to your androids paper above.

I totally understand that you don’t want to repeat yourself; I’ve been feeling recently like I’ve been doing a lot of repeating myself! But let me try to explain how it feels to me: imagine that you are at your university coffee shop and you walk by a discussion some colleagues are having about a subject that you’ve been working on. You sit down and join the conversation, but after a while someone says “oh, that’s in chapter 8.” After a little work you figure out what book they are talking about, which is one you haven’t read. You ask whether they could summarize what’s in chapter 8 so that the conversation can continue, but they reply “well, for just X dollars you can buy the book”. I don’t know how you would feel, but I would feel a little annoyed.

To put it another way, I think you may be trying to use a blog in a way that differs from the common expectations and conventions of the genre. That’s your choice, of course, but you have to be prepared for some pushback.

LikeLiked by 1 person

mathematicswithoutapologiesPost authorFirst of all, I owe you some links to expressions of surprise and shock with regard to my attitude, or attitudes of mathematicians in general, to foundational questions. You’ll find both of them in this post (thank you for the tip, and for indirectly providing a lesson in HTML):

https://mathematicswithoutapologies.wordpress.com/2015/04/27/pantheism-and-homotopy-theory-part-1/comment-page-1/#comment-92

and you may be surprised to find “surprise” in this one:

https://mathematicswithoutapologies.wordpress.com/2015/04/27/pantheism-and-homotopy-theory-part-1/comment-page-1/#comment-107

There are other examples.

About the blog: I never set out to create a blog for any reason other than to expand on my book and to clarify some of my motivations, for readers of the book. There are now two pictures of the cover and lots of allusions to the book on the home page. I don’t know how I could have made this clearer. I wish I could agree that I am using this “in a way that differs from the common expectations and conventions of the genre.” Nearly every page of the book is devoted to subverting the common expectations and conventions of the genre of book to which it belongs and exposing them as conventions. I had no interest in writing a conventional book and I don’t see why the blog should be conventional either. However, we are all being strongly advised by the spirit of the times to learn to market our most precious commodities, namely ourselves, to think of ourselves as Investments, and therefore to promote our Brands. In line with this entrepreneurial mindset, authors are strongly advised to establish a visible presence on Social Media. There has thus arisen a genre of Book Blogs, of which this one is a reasonably conventional representative, except that I keep leaving my entrepreneurial mindset in the closet when I leave home and therefore I am not using it efficiently to promote my Brand.

Now as for revolutions and the relation between HOTT and formal proofs, I agree that there has been an inexcusable slippage, due no doubt to my lack of sleep, between talk of a revolution in foundations (HOTT) and a revolution in mathematical practice (formalization of proofs with the help of computers). In my last comment I quoted two of the most eminent mathematicians involved with mechanized proof (either proof-assistants or automated theorem proving), and I have quoted Voevodsky several times elsewhere. All three have all been seen hanging around the two big HOTT gatherings of the past few years, and there really aren’t all that many mathematicians involved. So I think I can be forgiven for detecting a pattern and a connection, especially when I read things like this:

(From the very first pages of the HOTT book, for readers who spend too much time on social media to read books.) Maybe there is no logically necessary connection between proposing a new foundations “in a way that differs from the common expectations and conventions of the genre” (i.e., not in response to a perceived crisis) and writing about “the idea of a foundation of mathematics that can be implemented in a computer proof assistant.” But both in practice and in print it looks like the two are intimately linked, even if this link has been denied several times on this blog.

LikeLike

mathematicswithoutapologiesPost authorThere’s another consideration: this is not a coffee shop. No one would be listening if I were to propose a capsule description of the contents of my book at a coffee shop table (except for the local equivalent of the NSA, and as a rule they don’t intervene in intellectual controversies). But I consider everything written here to be on the record. If I took such a long time writing my book, and was so careful in my choice of wording, that’s because I see intellectual shortcuts as a source of confusion, and there are far too many of them in writing about mathematics. Maybe intellectual shortcuts are among the “common expectations and conventions of the genre,” or maybe I just think too slowly to be a Media Socialite.

LikeLike

Mike ShulmanThanks, but actually, I think that what you owe me is some links to expressions of surprise or shock “that mathematicians are not ready to adapt to the new axiomatics”. That was what you said and what I couldn’t remember hearing any of. In the comment of mine you linked to I said I was surprised by “the indifference and ignorance of mathematicians about foundations and by the absence of logic from mathematics curricula”, and in Andreas’ comment (which I overall found as disturbingly aggressive as you did, and not representative of anything I’ve heard from actual practitioners of HoTT) he said he was shocked to find that it was not the case “that mathematicians are interested in a precise science, not the hand-waving kind”. Those are both very different things.

I’m not familiar with “book blogs”; my experience just generally leads me to expect blogs and their comments to be a place for discussion rather than marketing.

The question of the relationship between HoTT and computer formalization deserves a much longer answer, so give me a little while to compose one.

LikeLike

mathematicswithoutapologiesPost authorI’ve also seen and especially heard expressions of surprise of the kind I apparently owe you, but I’m not sure they are easy to document and I won’t have enough energy to try in the next few days.

I’m glad you and I feel the same way about marketing. You’ll be relieved to know that this blog has been extremely ineffectual as a marketing tool. The number of visitors has tripled or quadrupled since I started posting about pantheism (and pantheism, by the way, not HOTT, was originally supposed to be the point of the post), but the all-important Amazon ranking has gone through the floor, in the US at least. Maybe the blog is discouraging sales. That would provide an interesting data point for my publisher. Twitter is supposedly more effective, but I’m much too long-winded to make good use of that.

LikeLike

Pingback: Does mathematics work like this? | Mathematics without Apologies, by Michael Harris