The problem is that there are actually several components needed: the semantic markup language, an input method no less efficient than LaTeX, and the math-lint itself. LaTeX is not semantic. MathML is just too verbose to type in the raw. The syntax used by theorem-proving software tends to be both esoteric and a bit too verbose (in addition to requiring the statements themselves to be extremely verbose).
I'm not sure that any plaintext markup can be sufficiently compact, semantic, and still resemble the handwritten syntax. That means we'll probably have to come up with a more interactive input method that is a bit more WYSIWYG in nature and has some auto-complete and automatic parenthesizing.
We know how to do type-directed operator overloading in unambiguous cases, eg. static methods in OO, modules and typeclasses in FP. This is often (ab)used to distinguish between alternative definitions. For example, Haskell's Monoid module defines several type synonyms for booleans and numbers, each of which has a different Monoid definition: https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-M...
If we trigger an error for ambiguous cases, the path of least resistance is to make things unambiguous.
Tools like mathematica and MS equation editor have solved this at the same time as the input method question: have an input method which converts to a markup in the background. This markup has enough information to produce typeset output.
I'm not sure that any plaintext markup can be sufficiently compact, semantic, and still resemble the handwritten syntax. That means we'll probably have to come up with a more interactive input method that is a bit more WYSIWYG in nature and has some auto-complete and automatic parenthesizing.