Mathematician here. There is a sentiment here, that seems to be that the hard part of mathematics is in the notation, and that this could be solved by just impl

Mathematician here. There is a sentiment here, that seems to be that the hard part of mathematics is in the notation, and that this could be solved by just implementing all mathematics in a programming language. I quite disagree. I believe that mathematics is hard, because explaining ideas is hard. Additionally, it is quite possible to state and prove an important theorem, without at all explaining where this theorem comes from, why it is important and how on earth you might ever cook up something like this. (In fact, I think there is a very great lack of good mathematical resources, even in pure mathematics). With regards to notation and mathematical writing in general, the problem is that it is never explicitly taught. Too many students of mathematics never learn to properly structure sentences in mathematics. In studying programming languages, you have no choice but to understand the structure explicitly. I do think mathematics has all the features you mention, it's just not explicit. > Variable Scope. In mathematical writing, the convention is that every variable is a global variable - and in a paper you quicky run out of variable names to use. Variables usually have local scope. In a mathematical statement like "for a continuous function f ...", the letter f is not defined after the sentence ends. Another common way to "initialize" variables is by statements like "Let f be a continuous function", and while it is true that it is never formally cleared, it is reintroduced when needed in another context. In some rare cases, you might start a chapter with "In this chapter, we let $H$ denote a fixed Hilbert space...", which is the mathematical equivalent to a global variable. > Strict Typing. You skim a paper, and you see "x + y". But what is x? a matrix, a vector, a scalar, an operator, a set, a random variable, you have no idea. The "+" operator is so overloaded x and y could be anything. I don't understand how programming languages are different here. Most modern programming languages also have operator overloading or polymorphism which has precisely this problem. Do you prefer C-style add_object_of_type_T(x, y)? > Having to hunt down the definitions for every variable is a time consuming and frankly wasteful process. Conventions are built up around this (upper case letters A,B at the beginning of the alphabet are matrices, but upper case letters at the end X,Y are random variables) but they are mostly rater silly. There needs to be an easy way to infer the type of a variable quickly. The common convention is to introduce variables just before you use them. That's as I would do it in a programming language? You seem to desire an IDE for mathematics, so that I could ctrl-click any variable to the definition. Though I have to say, if that's such a problem, the paper is probably horribly structured. I don't understand your problem with conventions. Conventions are suggestive, to help you remember the definition, it's much in the same way we choose suggestive variable names in programming languages. > Anonymous Objects. There is no way to declare a function without either giving a name to it (f(x) = x^2) or at least declaring its input symbols (x |=> x^2). But you can't go, say (x |=> x^2)(y). Sure you could write (x |-> x^2)(y), you're allowed to introduce any notation you like. But why wouldn't you just write that expression as y^2? You could declare a function as "the function which ...", which doesn't give it a name. If you want a symbolic expression, I'm not sure how you would do that without declaring any input symbols.