Mistaken premise here in my opinion: Think about typing the character ‘a’ on a keyboard. Fast, right? Just the one keystroke. “It is fast,” Bathiche says, “if you make some certain assumptions. That the position of the letter ‘a’ is where you intended it to be, the font is the way you intended it to be, the size of the ‘a’ is what you intended it to be.” All those decisions are made before you hit the key, and you of…
Can you type LaTeX faster than you can write equations on a chalkboard? I can't.
It was proof heavy so there was a lot of English anyway. Add copy/paste for derivations with a lot of shared structure and it really pulls ahead. If you define your own macros and are good enough at programming them on the fly it's a neat though dumb Lispy symbolic math tool.