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

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.