I'd love to play around with such tools, but I think they'd only get you so far before they'd start to become a hinderance.
The linter in mathematics is whether the other mathematician (whoever you're proving to) knows what you mean. If you're locked into a rigidly defined syntax, an obvious line of questioning is: what's not expressible in this syntax?
I fear that by the time the tooling was agreed on, built, and taught in schools, you'd have something like APL, which might be cool to code in, but from which the mathematical conversion would have moved on a while ago. Efforts like that, after all, are how math becomes engineering.
Consider, for instance, Russel's theory of types, which was interesting math at the time and now strikes the student with an engineering background as "pretty much just Java" (or any "normal" statically typed language).
If you're learning math for career reasons rather than just pure curiosity, engineering is the main/possibly only place you'd use it besides statistical analysis.
Yeah that sounds about right. I was more musing about the philosophical boundary between math and engineering (math being a creative pursuit and engineering being about outcomes).
I can't quite pin it down, like with a definition, but I'm tempted to say that if it has a linter it's not math anymore, even if it once was.
The linter in mathematics is whether the other mathematician (whoever you're proving to) knows what you mean. If you're locked into a rigidly defined syntax, an obvious line of questioning is: what's not expressible in this syntax?
I fear that by the time the tooling was agreed on, built, and taught in schools, you'd have something like APL, which might be cool to code in, but from which the mathematical conversion would have moved on a while ago. Efforts like that, after all, are how math becomes engineering.
Consider, for instance, Russel's theory of types, which was interesting math at the time and now strikes the student with an engineering background as "pretty much just Java" (or any "normal" statically typed language).