> “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.”

I'm not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of "mechanizing" and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it's worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens.

The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving "100% test coverage" and "instrumentation" of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us.

As a relative layman, I'm often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it's a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas.

But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that's why I'd be most excited about formalizing mathematics: how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?

Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians.

Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.

I am a mathematician and would love to mechanize my proofs. The issue is that systems like Coq construct proofs in a radically different way than how we were trained. I've struggled with Coq even with a somewhat more than a passing knowledge of the system; I used Coq's underlying language Gallina to write interpreters, which were then processed into OCaml while studying in graduate school. At the same time, I can barely turn out a basic proof in Coq.

What would help dramatically for me and others that work in applied math are proofs that cover the material in something like Principles of Mathematical Analysis by Walter Rudin. These are proofs that cover basic real analysis and topics like continuity, differentiation, and integration. It would also help to see basic linear algebra proofs such as that all real symmetric matrices have a real eigendecomposition. Now, these may exist and it's been a couple of years since I've looked. If anyone has a link to them, I'd be extraordinary grateful.

I'm curious, which field of math do you work in?

Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis...