The act of formalizing mathematics in a way that can be machine verifiable is an active area of research, but not one that is much of a concern to the majority

The act of formalizing mathematics in a way that can be machine verifiable is an active area of research, but not one that is much of a concern to the majority of mathematicians. I will say that in the current state-of-the-art writing machine verifiable proofs is often quite difficult and unintuitive, and not possible yet for many branches of math. The foundations upon which generations of mathematics are based upon do not lend themselves to machine verifiable proofs. Placing these fields on such foundations is very non-trivial, but people are trying. To your points on notation, I think requiring math to use purely ascii characters would end up being more of a burden than you expect. There are a lot of concepts in math and having more characters to use to represent them in a small space is helpful. I would much rather see a phi (one char) than a word representing something because it's easier to parse. Succinct notation lets you abstract big concepts and express relationships between them in a big-picture sort of way without requiring multiple lines. Then it's easier to remember the resulting relation. It's also worth noting that a piece of notation generally doesn't have one global use throughout mathematics. As long as notation is defined it's generally not a problem.