> Higher level math would be an order of magnitude easier with machine checked syntax.
This just isn't true, at least in terms of developing new mathematical ideas. There are already tools (e.g Coq) for providing mathematical syntax checking etc, but nobody uses these in developing new ideas because it would cripple the process of doing mathematics.
Particularly in the early stages of work, mathematics is very intuition and heuristic driven, you tend to sketch out an idea by actively using the ambiguity in the notation. Once you've got something that looks broadly correct you progressively try to shore it up by using more detailed and rigorous argument.
Maybe as an analogy, think of how architects design houses. They don't start by placing each brick according to correct civil engineering practice. They design something that broadly makes sense and then the civil engineers 'shore it up'.
You are right that it wouldn't be true in regards to new mathematical ideas. That's not what I meant, I should have been clearer. What I meant was 10x easier to learn.
Coq isn't about mathematical syntax checking. Coq is about encoding the whole proof in such a way Coq can machine verify it. That's 100 steps further then what I'm talking about. Just a simple syntactic check. Similar to what gofmt does. Is what you are writing considered valid syntax. Not whether what you are writing is correct.
This just isn't true, at least in terms of developing new mathematical ideas. There are already tools (e.g Coq) for providing mathematical syntax checking etc, but nobody uses these in developing new ideas because it would cripple the process of doing mathematics.
Particularly in the early stages of work, mathematics is very intuition and heuristic driven, you tend to sketch out an idea by actively using the ambiguity in the notation. Once you've got something that looks broadly correct you progressively try to shore it up by using more detailed and rigorous argument.
Maybe as an analogy, think of how architects design houses. They don't start by placing each brick according to correct civil engineering practice. They design something that broadly makes sense and then the civil engineers 'shore it up'.