Over on Mastodon, John Baez started a discussion about your Opinion 185, and Aaron Meurer suggested a certain irony with Opinion 184. Whether or not the two opinions are compatible, your Op. 184 seems misguided to me, with all due respect :-)
My primary reaction is just that Opinion 184 is barking up the wrong tree. You make a distinction between "Greek" style mathematics and "Babylonian" style mathematics, and place proof assistants like Coq and Lean in opposition to computer-algebra systems like Sage and Maple. But really these systems have much more in common than your opinion suggests. Proof assistants like Coq and Lean, which are both based on type theory and the proofs-as-programs correspondence, are programming languages in their own right, allowing the user to give explicit constructions of mathematical objects, and to write proofs as algorithms and execute them on concrete inputs. Indeed, it can be argued that the reason why type theory is a much more natural framework for formalizing ordinary mathematics than, say, axiomatic set theory is precisely because of its constructive nature.
Moreover, as I wrote on the thread, in practice many people use proof assistants as tools in the spirit of computer-algebra systems, because they want to hack around with mathematical concepts and get immediate feedback from the computer, rather than because they are obsessed with logical rigor. Martin Escardo is an example of such a person, and he wrote in response that "proof assistants are my smart blackboard". Although it varies from system to system and from user to user, proof assistants in themselves do not enforce a "religious-fanatical obsession with (often alleged) full rigor" as you claim. Many proof assistants (including Coq and Lean) allow users to write proofs with holes, which can be filled (or not) at the user's leisure. Also, some proof assistants allow the user to moderately adjust the foundation itself, including logical principles which are either of unknown consistency or even known to lead to contradiction if abused. For example, the Agda proof assistant has a flag --type-in-type, which roughly corresponds to adding the axiom that there is a type of all types. This is known to be inconsistent, but is a useful simplifying assumption if one wants to avoid (perhaps only temporarily) the labor of keeping track of a hierarchy of different universes of types. Similarly, although Agda comes equipped with a termination checker which tries to decide whether the functions you wrote in your proof-as-program are terminating on all inputs, you can override the checker and assert that any function you write is terminating, even though abuse of such assertions allows you to prove false things in general.
Another issue with Op. 184 is that you characterize proof assistants as being about mere formalization of human-generated mathematics. But in reality, the aim of proof assistants is to enable humans to prove things that couldn't be proved without the aid of computers, or could only be proved with great difficulty and by exceptional humans. There are already examples of this coming from engineering, where proof assistants have been used to verify complex systems that would have been impossible or extremely expensive to verify by hand. And it seems that this is also a direction that mathematics is headed in. As Ian Agol said in the Mastodon thread, "Proof assistants are being used to verify long complicated proofs that can be understood by few people, or are computer aided". This was the use for proof assistants that Vladimir Voevodsky envisioned, motivated by his own personal experience of proofs of complicated results (written by him or by others in his field) that were trusted based on authority but were later discovered to contain sometimes unfixable errors: see his article, "The Origins and Motivations of Univalent Foundations". And it's also similar to the experience Peter Scholze described in his six-month report on the "Liquid Tensor Experiment", see in particular his comments about how the Lean proof was used to better understand and revise the informal blueprint in human readable form:
it's not the blueprint from which the Lean code was formed, but (largely) the other way around! The Lean Proof Assistant was really that: An assistant in navigating through the thick jungle that this proof is. Really, one key problem I had when I was trying to find this proof was that I was essentially unable to keep all the objects in my "RAM", and I think the same problem occurs when trying to read the proof. Lean always gives you a clear formulation of the current goal, and Johan confirmed to me that when he formalized the proof of Theorem 9.4, he could -- with the help of Lean -- really only see one or two steps ahead, formalize those, and then proceed to the next step. So I think here we have witnessed an experiment where the proof assistant has actually assisted in understanding the proof.
In this sense, I am confident that the ultimate side-effect of the widespread use of proof assistants in mathematics will be the development of truly "deep" mathematics, in the sense of your Opinion 51, and I am sure that it will be beautiful!
Noam Zeilberger, 4 January 2023