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.
Getting 'f' vs 'f(x)' right mostly is really important for programmers who deal with higher order functions in general all the time. Most mathematicians don't fall into that category.
You could say calculus deals with higher order functions, like the derivative. And that's a valid way to look at it. But most people get by just fine using special purpose notation for the derivative and not thinking about it as a function just like 'f'.)
I used := to emphasis that I am defining 'f' here, not just writing down any old equation. (Eg like like in the example "Find all functions f such that f(x + 1) = x * f (x).")
Though if you wanted to be pedantic about notation, I could have written that as with the x on the other side of the :=, like f := \x -> x + 3 (for Haskell inspired notation) or f := (x |-> x + 3) where |-> means the little arrow I draw by hand to denote a mapping when I'm writing math on a chalk board or piece of paper.
I'm not sure why := would denote a computation? At most you might want to use it to denote an assignment in a mutable context?
Operators and functionals?
Mathematicians deal with higher order functions all the time, e.g. in functional analysis.
OTOH, the lack of rigor is definitely one of the problems of contemporary math. Many years ago, when I was a student, I studied one paper, coauthored by 2 people - call them X and Y. X was a very established mathematician, Y was a relative newcomer. There was one (set-theoretical) argument I couldn't understand, so I asked Y (he was my advisor's friend) about it. He told me "yeah, X asked me this, too, and I told him to use Zorn's lemma, and after a moment of thinking, he said, Β«yeah, that would workΒ»". I'm not set theorist myself, but it smelled suspicious to me, so I asked another friend, who knew much more about set theory than me. He smiled and said "of course it's wrong, it's a very common mistake".
Had X and Y written out the argument more rigorously, we'd have one less published result with no correct proof...
And I have quite a few other anecdotes like this, unfortunately.
One professor at my former faculty once told how he approaches refereeing papers. "For the first 30 minutes, I try to prove the main result myself. If I don't succeed, I spend the next 30 minutes trying to find a counterexample. This way I write most reviews in half an hour."
A few years ago I coauthored a book about non-linear analysis. Quite a few quite interesting topics. One of the coauthors insisted on writing out proofs in detail and rigorously, and now we joke that our book is the first one where some (quite established and known in this field) theorems are proved correctly for the first time. (And that includes proofs with gaps/mistakes in both research papers and monographs, btw.)
I specifically meant getting this is important for programmers who deal with higher order functions.
It is not so important for mathematicians who deal with higher order functions.
Mostly because the intended audience for their writings is smarter than a computer, and there's typically more context.
In math, := is typically used to denote a definition. Using equality (=) only makes sense if both sides of the equality sign already have a definition.
i mentioned this up-thread but is that why := is assignment in Pascal? Wasn't Pascal the main academic language there for a while?
Edit: On math.SE[2] someone claims that it's notation borrowed form programming. Someone else claims that it was introduced by Bourbaki, which might predate programming, as Bourbaki started publishing in the 1930s. However, I couldn't find any evidence of this from skimming a few Bourbaki PDFs.
[1] https://en.wikipedia.org/wiki/Assignment_(computer_science)
f = y+3 makes sense f(x) = y+3 does not make sense (at least to me), f(y) = y+3 makes sense however.
f(x) is a function of x correct? It's articulated as "f of x".
> I wonder why you used ':=' instead of '=' to define 'f'. There is no computation going on, right?
:= is assignment in Pascal iirc, maybe that's where it's coming from.
For example, that could describe a constant function that doesn't depend on x, and y is a free variable that gets its value from context.
Or y could implicitly be a function of x. That happens a lot in calculus or physics.
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.
If we changed symbols now, it would create an even bigger mess. Because the people that learn the new symbols, could not read any textbook published before 0 A.D. (Anno Discombobuli)
Sure, back then when everybody who learned trigonometry had a classical education with ancient greek picking greek letters when the latin alphabet wouldn't do was a rational decision. It just hasn't aged well.
Virtually all the textbooks use those symbols. Do you have a viable and better alternative to suggest or are you just complaining? And I didn't assume that you know or don't know something, I just wrote it down for the sake of the argument. We are not having a private conversation, we are contributing to a public discussion.
Math also uses made up symbols specific to math a lot (integral, summations, arrows, operators...).
If you want to claim that Greek is the problem, how would you solve the problem of insufficient symbols?
Adding another alphabet alleviates those issues somewhat but even with greek letters added in we still run into this issue somewhat commonly.
Btw, even mathematicians don't mind writing out `sin` or `cos` or `ln` in their formulas. So they are certainly not completely averse to multiple letters.
Agreed. But yet... some of the approaches taken to deal with that can be wildly annoying. Actually, using the Greek letters is probably the best of the lot, since they are a completely different set of characters with known pronunciations.
OTOH, sometimes you'll see people use both upper-case and lower-case latin letters in the same problem, forcing you to read it in stilted language like "The derivative of Big X with respect to y, plus the integral of Little x ..." Aaarrgggh.[1]
And then you get the "stylized" letters, which are (mostly) just Latin letters, but have no obvious unique pronunciation or verbalization without going through contortions. I mean, what do you say for "π" especially if there is also a "n" on the page? And who's even going to recognize these monstrosities unless you're already a mathematician: π, π, π? Aaarrggggghhh.
[1]: to be fair, you could have the same problem with mixed case of Greek letters, but I haven't seen that as a common problem. But maybe that's only because I'm not a mathematician. shrug
Judging maths on its syntax is like judging a poem or work of literature on its font. It really isn't a central thing.
That's probably okay if we view mathematics in the way this book (I have not read it, going based on the description here) advocates, as a sort of toy for playing with arguments. And I'm certainly not saying Math should ever be viewed as an empirical discipline nor constrained by that kind of thinking. But I don't think I'm the only one that takes one look at things in the realm of say higher category theory and thinks it's mostly playing word and symbol manipulation games, and lacks any real mathematical content that could not be discovered at a lower and more understandable (and less likely to produce new research) level of abstraction.
I guess I've sort of betrayed that I am pretty firmly a platonist in that respect so make of that what you will.
Like I said, this is not an unusual opinion for a computer person to have and I'm sure it's fairly annoying to any pure mathematician at this point. But I think it's still fair if we want to understand what turns certain people off of pursuing mathematics further.
https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
TL;DR: They started producing false results.
Note that this was not about capital-F Foundations of Mathematics like (arguably) the foundational crisis of math that had its origins in the 19th century, but rather about lowercase-f foundations of a particular field, in this case algebraic geometry.
Weil's foundations of AG in the eponymous 1946 book were horrible and messy but they solved the issue (even today there are a lot of celebrated results that can only be found as expressed in Weil's language) and later in the 1960s Grothendieck provided the elegant language of schemes in which people generally learn and research AG today, and which helped prove long-standing problems like the Weil conjectures and (to some degree) FLT. Category theory was, in this case, essential to proving theorems about "real mathematical content" like numbers and points.
GED isn't really related to this subject although it contains some of the same themes and characters
I also believe that the emphasis on "rigor" here is misplaced. The argument isn't about whether mathematical rules are rigorous or not. The argument is about whether mathematics exists independent of mathematicians (and they discover it in a way how an astronomer peers into telescope and discovers new stars) vs mathematics being created by mathematicians' minds (similar to how an architect designs a building: there weren't one before, and now there's a concept of a new building with so many walls, floors, windows etc.)
I believe that mathematics is art, not science. I.e. mathematicians create new rules, they don't discover them. The whole argument to support this point would be too long to write it in a single post, but the general idea is that mathematics is a system that can easily describe counterfactual worlds. We use it to also describe our physical world because, of course, it can do that. But then asking the question about the "surprising effectiveness" is moot: we deliberately made it to be as effective as possible, so how is it so surprising that it is?
The "surprising effectiveness" is, I think, one of three things. First, the surprise is that we can create mathematics that describes our physical world.
The second surprise is that, when we find out something new, it often takes the form of existing mathematics that we didn't design to describe the physical world. (Though, from your point of view, I suppose you could say that we created mathematics to describe everything that could be described by mathematics, and so it's not surprising that something was there to describe reality.)
The third surprise (maybe this is just a restatement of the first one) is that mathematics really describes the physical world. It's not that we find some math that describes it, and then we change the situation a little bit and we need to find some new math. The surprise is that the math describes what is going on so well that it applies to situations that we didn't know about when we devised the math that applied. That is, it's predictive, not just descriptive.
Similarly, if mathematics is so powerful as to be able to describe any physical reality, it shouldn't be surprising that it can describe ours, no matter how complex and detailed.
I don't see the reason to think that coincidentally arrived at ideas mean that ideas are discovered. We use the same framework, with the same rules. It's not unlikely that we'll create same ideas, because we use all the same rules, but the framework is so vast... it has so many rule combinations it's mind-boggling how would you think all ideas already exist in this framework.
More practically, we call an action a "discovery" when we (unbeknownst to us) faced the consequences of the phenomenon being discovered, but didn't know why we were facing them. An astronomer who finds a "new" star was ever so slightly influenced by that star's light, gravity etc. A marine biologist who discovers a new deep-water fish was ever so slightly affected by that fish through a complicated chain linking many different species through biosphere.
An artist drawing a new painting isn't discovering it in the same sense. She isn't interested in how an existing painting was connected to the consequences of her life or the lives of the whole human species. By selecting of all possible ways the paint can be laid down on canvas her particular way of doing that she creates something genuinely new, or as new as it can possibly be. It's counterproductive to label this activity "discovery" because then we lose an important distinction between the nature of the work of an astronomer and that of a painter (or a mathematician).
There are sculptors who'd jokingly say that they "discover" the statue in a stone slab. But they do so in a sarcastic kind of way, really (well, artists are weird and will make a lot of nonsense claims just to trigger non-artistic audience). But, deep down, nobody believes that they are searching and finding good images, melodies or novels. I cannot really imagine a mechanism through which I'd discover the answer writing to you. It's a lot easier to explain what i wrote by saying that I meant to write it.
I havent read the book but this dichotomy is not an intrinsic feature of how people pursued mathematics historically.
The "stiffness" and excess focus on rigor and accuracy developed gradually over the 19th century because people were being loose canons - primarily around calculus.