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.