Every mathematician should probably read Vladimir Voevodsky’s article in the Summer 2014 IAS Letter. Only time will tell whether it will be remembered as a historic document of the highest importance; in the meantime, it can be read as an unusually lucid and frank account of what the subtitle calls a Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes. Voevodsky tells a few stories about subtle mistakes in important papers, including his own, that left him uneasy. I’ll skip ahead to the happy ending.
I now do my mathematics with a proof assistant. I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don’t have to go home and worry about having made a mistake in my work. I know that if I did something, I did it, and I don’t have to come back to it nor do I have to worry about my arguments being too complicated or about how to convince others that my arguments are correct. I can just trust the computer. There are many people in computer science who are contributing to our program, but most mathematicians still don’t believe that it is a good idea. And I think that is very wrong.
The emphasis is mine. “Most mathematicians” is certainly an understatement; leaving aside logicians (especially proof theorists), I only count a handful of mathematicians who believe it is a good idea. My book asks:
Who finds machines more appealing than humans, and for what ends?
Voevodsky’s article gives one perfectly coherent answer to the question from a standpoint that is unquestionably that of a mathematician. My impression is that a large fraction of the unprecedent 788 views (or more) Part 1 received yesterday were by visiting computer scientists, whose priorities are not necessarily the same. A lot of the talk about HOTT/UF on the n-category café, and in some of yesterday’s tweets on my earlier post, qualifies as enthusiasm in what the OED calls the “principal current sense” of the word:
Rapturous intensity of feeling in favour of a person, principle, cause, etc.; passionate eagerness in any pursuit, proceeding from an intense conviction of the worthiness of the object.
I think this correctly qualifies the attitude of some HOTT/UF defenders who, noting that most of the people involved are computer scientists rather than mathematicians, express surprise (or even “shock”) that mathematicians are not ready to adapt to the new axiomatics, rather than asking themselves whether they might not be misconstruing the goals and motivations of mathematicians. (Mathematicians, apart from logicians, were distinctly in the minority at last year’s trimester program at the Institut Henri Poincaré in Paris.) Parts of chapters 3 and 7 are addressed to such people.
Some of the talk even qualifies as enthusiasm in the original 17th century sense, which goes back to antiquity, of
Possession by a god, supernatural inspiration, prophetic or poetic frenzy.
In spite of the word “Mission” in Voevodsky’s subtitle, and in spite of his conviction that most mathematicians are “very wrong” not to follow his lead in learning to use proof-assistants, I hesitate to call him an enthusiast, because his text is so precise and convincing and consistent with the “internal goods” of the practice of mathematics — although, as I’ll explain in what will have to be Part 3, I’m not convinced that computer-assisted proofs are the future of mathematics.
On the other hand, I’m tempted to call Voevodsky a pantheist, not only because of his astonishingly sensitive nature photography (you should look at the original files) but because the experience he described in 2012, in a two-part interview (part 1, part 2) with a Russian website, is more akin to a pantheistic revelation than to an incident of divine possession or poetic frenzy.
В 2006-2007 годах со мной произошло множество как внешних, так и внутренних событий, после которых моя точка зрения на вопросы “сверхестественного” существенно изменилась.
which translates roughly as “In 2006-2007 I had a number of internal and external experiences, after which my view of ‘supernatural’ questions was substantially altered.” You can read his detailed account of these experiences in Russian; as far as I know they haven’t been translated, although they would not have been out of place in 19th century New England, or in the Beat Generation (from the Footnote to Howl by Allen Ginsberg):
Holy time in eternity holy eternity in time holy the clocks in space holy the fourth dimension holy the fifth International holy the Angel in Moloch!Holy the sea holy the desert holy the railroad holy the locomotive holy the visions holy the hallucinations holy the miracles holy the eyeball holy the abyss!
Voevodsky himself compared his experience to what C. G. Jung (who is often identified as a pantheist) called his “confrontation with the unconscious.” It was at the end of this extended altered state that Voevodsky returned to mathematics, after a long interruption, and developed the basics of his univalent foundations by 2009. (Readers can supply their own parallels from myth or literature.) His IAS article is circumspect and modest in that he only claims to be seeking assurance of the rightness of his arguments. In his Russian interview, however, he expresses full confidence in the rightness of his mission.
Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут “понимать” компьютеры можно считать в основном решенной.
(roughly: “I have practically no doubt that these foundations will soon replace set theory and that the problem of a mathematical language that computers can “understand” can be considered essentially solved.”)
There is no hint of a divine presence in Voevodsky’s account of his experience. Pantheism of this sort has a respectable pedigree in the history of science and mathematics.
There is another thread that tied Felix Klein to Wilhelm von Humboldt: his belief in a preestablished harmony. With Klein and his fellow mathematicians, the Leibnizian preestablished harmony became more specific. It became a preestablished harmony between physics and mathematics and the foundation of their pantheistic faith.
(S. Schweber, In the Shadow of the Bomb)
I originally chose this title in the expectation that I would find something of this pantheistic impulse at the root of interest in HOTT/UF. But the reactions to the first part of this post indicate that the interest is primarily motivated by logos rather than eros, and if there is a pantheistic tendency it doesn’t seem to extend much beyond Voevodsky.
Mathematics without Apologies, by Michael Harris 
It’s still surprising me to see that so called good mathematicians are not necessarily “true” scientists in the sense of being led by spiritual motives, like Newton, Einstein, Grothendieck (and many other) were.
I actually think that the belief in some form of pantheism, say, the belief in the existence of some beautiful, consistent “structure” governing existence, is a good criterion to discriminate true scientists from false ones.
Why that? Because the goal of science is to explain and to make sense of existence (at least some part of it). People who takes maths or physics as a game are in this respect no true scientists: they don’t try to make sense of things, they just play around purposelessly, without any deep reasons behind their research but problem solving, fun, or fame. So, who shall we blame for that?
High-school for not teaching sciences as they are, that is, full of rigor, exigence and spirituality -, thus forbidding children to discover sciences as they are and getting really interested into them?
Liberalism, for telling us that “its all meaningless” and that everything that an explanation is no different than a description? For telling us that a theory (what gives meaning) is the same thing as a model (what gives concrete example of),and that everything should necessarily be related to experiment or be falsifiable?
Mathematician (and scientists) themselves, who work purposelessly, following blindly the inertia and the trends of the academics, without knowing why they should do maths rather than being musician or a pro pizza eater?
In any case, it’s surprising to see that a pantheist motive is related to “proof checking” rather than “understanding” itself.
LikeLike
“…without any deep reasons behind their research but problem solving, fun, or fame.”
Isn’t problem solving and fun sort of the whole point?
LikeLike
Only if you are or aspire to be/stay a low level scientist, without any vision, I suppose.
The goal of science (physics, maths, computer sciences, …) is to make sense of things, that is, to explain and enhance our understanding. Solving a problem never been equivalent to its understanding. The latter is metaphysical thing, related to concepts, theories, and point of views on “something” (say, a problem, or the world itself). Would you claim that the four color theorem is understood because it is solved in a brute force way, or would you be satisfied by a theory that would eventually develop a whole new language trivializing it?
You see, this is what I find really disappointing with so called scientists: they don’t know why they do or should do science, they have no purpose nor vision. Can good research be made this way, without any will to understand? You tell me.
LikeLike
Name-calling (“low level”, “without any vision”, etc.) are not especially welcome here. There is room for an ethical discussion but it should be informed by a basic respect for participants. I’m allowing this comment to stand as an example but I don’t want to see many more like that.
LikeLike
I think that “problem solving and fun” is part of, but not the entire, point of doing mathematics. There is an old meaning of the word “transport”: overwhelm with strong emotion, especially joy. There are probably many mathematicians who occasionally experience transport at certain ah-ha! moments. This goes beyond fun and some might call this almost spiritual, others an additive drug. Then there are those who strive to marry mathematics and physics — a very practical endeavor, often frustrating, but sometimes also transporting. [I don’t do mathematical physics, but am very curious about it. I found the recent interview with Ed Witten in Notices fascinating.]
LikeLike
This is my initial knee jerk reaction to Voevodsky’s article.
“Formulating mathematical reasoning in a language precise enough for a computer to follow …”
I’m not interested in computer verification of proofs if it involves warping my language into hideous “precise” computer-like code. (Yes, I’ve written computer code.) Mathematics, as it has been practiced, is a satisfying human and social endeavor partly because we can communicate with each other about it within a wrapper of natural and semi-natural language. It’s the computer that needs to adapt to the demands of people, not the other way around.
“The primary challenge that needed to be addressed was that the foundations of mathematics were unprepared for the requirements of the task.”
Again, it’s the computer that’s unprepared for, and inadequate to, the requirements of humans.
Voevodsky was shaken by an error of his that went undetected for a period of time. Hasn’t that happened to almost everyone at least once? We clean up the mess, move on, and grow from it.
LikeLiked by 1 person
Richard, it’s worth remembering that existing formal foundations of math suffer from the same sort of warping of natural language. If you’ve forgotten this, it may be worth trying to prove formally that function sets exist in ZFC. In some sense, ZFC was the state of the art for computer-checkable mathematical proofs; after all, were we so inclined, we could have a computer check formal proofs from the ZFC axioms, but doing so would be a nightmare.
So from the computer-verification standpoint, HoTT represents an attempt to do what you say must be done: adapt computers to the demands of mathematicians. Voevodsky is trying to formalize math he’s already done. Existing formal systems (“existing computers”) were insufficient.
For most (or at least many) people involved in homotopy type theory, a primary motivator is to find a formal language which can “encode” mathematics in a way which is closer to the way mathematicians actually think. Or, perhaps, more as Michael would put it, to bring together the *logos* of formal mathematics and the *eros* of “real” mathematics.
LikeLike
Could you link to some of those expressions of surprise and shock? Off the top of my head I don’t remember any that I’ve heard. I personally am not at all surprised that mathematicians are not immediately ready to jump on a new foundational system. Frankly, I’m (pleasantly) surprised that so many computer scientists have been so enthusiastic about it; HoTT/UF seems to me at least as radically different from what they are used to as it is from what mathematicians are used to. Perhaps it’s because they are more pragmatic than mathematicians, used to the idea of (say) switching between programming languages as dictated by the needs of the moment.
It bugs me when people (listening mostly to Voevodsky, I guess) get the idea that HoTT/UF is mainly about formalizing mathematics in a computer and that this is some sort of new thing. People have been formalizing mathematics in computers for decades. They don’t generally use ZFC either; at least the biggest and most succesful projects use the same sort of type theory that HoTT/UF is built on. In the grand scheme of things, HoTT/UF is (in my opinion) really only a modest improvement in these systems, bringing them a little bit closer, in one aspect, to the way that mathematicians generally think informally. Personally, I think these systems still have a long way to go before one can reasonably expect the average mathematician to use them, and a lot of the problems are “engineering” ones rather than mathematical ones. (I am fairly confident that they’ll get there eventually, but perhaps not in this century.)
I think there is also a significant danger in the use of proof assistants, which is related to Voevodsky’s quote:
Using a proof assistant leads some people to the dangerous (IMHO) attitude that once a proof has been checked by a computer, there is no more to say about it. But we don’t prove things only to be sure that they are correct; we prove them in order to understand them better, and to explain that understanding to other people. Otherwise no one would ever bother to find a new proof of an old theorem. A computer proof assistant should be a supplement to mathematics, reassuring us of the correctness of the details so that we can focus on explaining the ideas. Considering checking by the computer as “all there is to do” also tends to lead one to write unreadable and unmaintainable proof scripts; can you imagine a programmer saying “as long as my code compiles and does what it’s supposed to, I don’t have to worry about it being too complicated or how to explain to others how it works”?
These are some of the reasons I don’t generally try to “sell” HoTT by talking about computer formalization of existing mathematics. I think it’s much more exciting to talk about the new mathematics that it enables us to do. The whole point of the HoTT Book was to show that this sort of HoTT can be done without computers, in the same sort of style (should I say “just as erotically?”) as mathematics has always been done.
LikeLiked by 1 person
This is a fear I share: what if tomorrow, we have some really nice proof checker to review our proofs? I’m afraid that it will become more and more common to see people relying mostly on computers and become too “lazy” (if I can say) to redo them. Moreover, it could sell an image of an entirely automatized mathematical research, more or less dead (in no need of new ideas), where researchers are just little hands doing programs. Also, this wouldn’t at all reverse the very bad situation regarding fundings of fundamental subjects, or its selection process: politics are mostly ignorant about what is science and its way to function (they tend to think that it should be productivist as liberal economy is, and applied to society), while the existence of a proof checker will sooner or later make them want to found people to build a proof finder, thus adding another bias against creativity.
These fears are not illegitimate. In physics, for example, there is a dangerous trends regarding computer simulation. In many places, there are now huge computers running in order to give numbers out of a black box. These guys are seen as “theoretical physicists”, while all they do is actually a computer **experiment** that does not explain anything. Obviously, if you give money to buy super computers and found the work of these people, you don’t give it to people trying to think with a pen and a sheet of paper.
LikeLike
As to why computer scientists have been so enthusiastic, I can think of a few things: On the academic side, there is a long history computer science drawing on topology to try to understand computation more deeply. HoTT seems well in this vein. On the logics side: MLTT and MLTT-derived research have of course been enormously influential in the development of theoretical CS in the past decades. Furthermore, a system that promises both decidability and extensionality has also been a long-held goal. Along with that, speaking for myself and a few others at least, I think it is the case that HoTT is a great deal of fun, and it provides an avenue to take the type-theoretic thinking we are used to and leverage it to understand a much broader range of mathematics. A part of the “constructive impulse” in programming is that for many of us, understanding things is best done by building them. By extending the universe of what we can build, HoTT helps us to extend the universe of what we (or at least I) can understand.
With regards to your comment that “the biggest and most succesful projects use the same sort of type theory that HoTT/UF is built on” — this is not as much the case as you would imagine. To my knowledge, Mizar is really the biggest project, and Isabelle/HOL is also very widespread. For automation of “workaday” verification (typically for chips), ACL2 has found widespread success. All three are based on different foundations, and none on the same sort that Coq or Agda are. I lost quite a bit of time reading through Freek Wiedijk’s compendium “The Seventeen Provers of the World”: http://www.cs.ru.nl/~freek/comparison/comparison.pdf — he also maintains a ridiculously large, and yet still incomplete, list of computer mathematics systems: http://www.cs.ru.nl/~freek/digimath/index.html
There are more logics on heaven and earth Horatio…
(Not in regards to this, but in regards to discussions elsewhere: it is important to distinguish between systems that automate proof _checking_ and those that automate proof _construction_ — Agda does the first, but not the second, for example. Coq can be used in a variety of styles. Meanwhile, a system like ACL2 is much more geared towards automatically generating ‘long, boring’ proofs to verify lots and lots of trivial conditions taken together [such as one might want to discharge when verifying the correctness of an ALU on a chip]. It seems to me that one of the most important areas of research in proof assistants is the ongoing work on systems of tactics towards the end of making the automation part work as a better compliment to the human mind. It is also notable how many of the tools Freek has collected were created primarily with the end of aiding in teaching, exploration, and the development of intuition.).
LikeLike
Thanks for bringing up the other provers. I would argue that HOL is more like MLTT than it is like ZFC, so it also helps to make my point. Mizar I think uses a more ZFC-like system, but it also seems to me to be a fairly isolated community, and while they’ve accumulated a substantial amount of mathematics, I don’t know of it being used to actually verify any new mathematics whose correctness was in doubt, as compared with say the 4-color theorem, the Feit-Thompson theorem, or the Kepler conjecture.
LikeLike
Gershom B reminded me of another concern that I have: the language du jour problem. There have been many fads over the years in computer programming languages, CS folks seem to love inventing new ones, and backwards compatibility with anything is generally not a central concern. In mathematics, there has always been, for example, drift in notation and invention of new words, but it generally happens slowly enough that there isn’t much of a problem reading 50 year old papers. Similarly, TeX, mathematic’s typesetting language, evolves slowly, generally has backward compatibility, and is the universally accepted standard. In contrast, I suspect that we will see a proliferation of different “foundations,” proof checkers, and proof generators driven by CS folks*, and it will never settle down, mirroring the situation with programming languages. I see the chaos of a Tower of Babel. Tell me it ain’t so.
*especially if research money starts to flow
LikeLike