| Syntax is about the least of people's worries when they worry about 'mathematical rigor'. Math is made for people to read and write, and they have different 'domain specific languages' for different parts of math. Now what would be useful is a tool, perhaps something like a large language model, to automatically translate from the notation used in one area of math into another. That can't be a fully mechanical procedure (hence the need for something flexible like an LLM), because it's part and parcel of human mathematics to abuse notation here and there in the name of ergonomics. My personal pet peeve is defining a function like f(x) := x + 3, and then treating f(x) as the name of the function, instead of just f. But really, it's just a harmless abuse of notation when done by some humans to other humans. |
For example the convention to use the greek alphabet for certain things. This is totally arbitrary and you could have also used emoticons instead (had they existed). But what this means is that the pupil, before tackling the meat of the mathematical problem has to accept that weird looking letter they have never seen for no real reason whatsoever.
And I say that as someone who can fluently read the greek alphabet.