Terence Tao wrote a blog post years ago dividing math education into 3 stages: pre-rigourus, rigourus, and post-rigorous. That distinction seems relevent here.
Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. We could make every invocation of a canonical isomorphism explicit, but that would make all of math far too unwieldy to do.
This is the core problem with formal proof verification. Current provers need you to prove things at such a low level that they are simply unwieldy to use. That does not mean we need to reinvent all of math. It means we need to improve formal verification tooling. Maybe we also need to train mathamaticians in formal verification systems. In much the same way that they had to be trained to use computer algebra systems. We didn't reconstruct all of math. We just learned how to work within the limitations of tools when we use those tools.
[0] Unless you go out of your way to construct them to be the same thing. There is not actually any official definition of, for example, what the integer 1 is. Since so many definitions of it are equivalent, that is a fundamentally pointless conversation to have. A few textbook authors need to make a decision for pedalogical purposes. No one else cares.
Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. We could make every invocation of a canonical isomorphism explicit, but that would make all of math far too unwieldy to do.
This is the core problem with formal proof verification. Current provers need you to prove things at such a low level that they are simply unwieldy to use. That does not mean we need to reinvent all of math. It means we need to improve formal verification tooling. Maybe we also need to train mathamaticians in formal verification systems. In much the same way that they had to be trained to use computer algebra systems. We didn't reconstruct all of math. We just learned how to work within the limitations of tools when we use those tools.
[0] Unless you go out of your way to construct them to be the same thing. There is not actually any official definition of, for example, what the integer 1 is. Since so many definitions of it are equivalent, that is a fundamentally pointless conversation to have. A few textbook authors need to make a decision for pedalogical purposes. No one else cares.