Written: July 18, 2022
More than twelve years ago I commented that using logic-based software, like Coq and Lean, to do mathematics, as preached by Kevin Buzzard (see Kevin's ICM 2022 engaging talk, and Gil Kalai's wonderful post) and Georges Gonthier (see Gonthier's fascinating ICM 2022 talk), is not the optimal use of computerkind, and of the talented humans who develop and use them.
While I DO appreciate the pioneering work of Avigad et. al., Tom Hales, Gonthier, and others, to make a political point, and "shut up" all the traditional human-centric and machino-phobic skeptics (e.g. Michael Harris), enough is enough! We don't need more "formal versions" of human-generated mathematics. Formalizing known proofs is not unlilke Pig-Latin. Once you have done it a couple of times, it is no fun anymore. While it is both intellectually and technically challenging, or else such brilliant people would not engage in it, these people are wasting their talents.
Indeed our silicon servants, soon to become our masters, can be used much more fruitfully. COQ and Lean continue the pernicious Greek tradition, that introduced the axiomatic method and made mathematics a deductive, logic-centric science. By inertia, the Euclidean axiomatic approach continues to this day. Current, human-generated, mainstream mathematics is the way it is because it is an artifact of the historical fact that computers were invented recently. Since humans had to do something, they developed a Rococo and in-bred `body of knowledge' of so-called "conceptual mathematics". If an ET would come to us and try to read, say, the Langlands program, it would be very bored, and would not see the point.
Now Buzzard et. al. want to further this agenda, by teaching computers how to emulate, for example, Peter Scholze, and continue this unfortunate 2300-year-old tradition.
Computers are based on algorithms, so now that we have them, we can dump the "Greek", Euclidean, axiomatic, logic-centric, tradition, as implemented by Lean and Coq and their ilk, and go back to the much more fruitful tradition, that of ancient Egypt, Babylon, China, India, Persia, and Arabia. In other words, algorithmic, constructive, explicit, and concrete math. The natural computer-heir to this tradition are computer-algebra systems, like SAGE, Maple, and Mathematica, rather than Coq and Lean. Mathematics should become a physical science again, without the religious-fanatical obsession with (often alleged) full rigor.
Of course, all science requires logic, but computerized logic, while definitely very useful in software engineering, for verifying program-correctness, has no place in the kind of, experimental, empirical, "Babylonian" mathematics that would hopefully emerge, once we get rid of our Greek obsession.
But what truly got me scared is that, a few months ago, I heard a talk about using Lean and Coq in undergraduate math classes. The current math curriculum is already bad enough, indoctrinating our students in Greek-style math, but harnessing Lean and Coq in "Introduction to Proofs" classes, is really going too far.
Added Jan. 4, 2023: Read Noam Zeilberger's insightful comments
Doron Zeilberger's Opinion's Table of Content