|
Here's a take from a mathematician-in-training, and it's biased toward research-level math, or at least math from the last hundred years: Math is difficult, and a lot of what we have is the result of the sharpest minds doing their best to eke out whatever better understanding of something they can manage. Getting any sort of explanation for something is hard enough, but to get a clear theory with good notation takes an order of magnitude more effort and insight. This can take decades more of collective work. Imagine complaining about cartographers from a thousand years ago having sketchy maps in "unexplored" regions. Maps are supposed to be precise, you say, there's actual earth there that the map represents! But it takes an extraordinary amount of effort to actually send people to these places to map it out -- it's hardly laziness. Mathematics can be the same way, where areas that are seemingly unrigorous are the sketches of what some explorers have seen (and they check that their accounts line up), then others hopefully come along and map it all in detail. When reading papers, there's a fine balance of how much detail I want to see. For unfamiliar arguments and notation, it's great to have it explained right there, but I've found having too much detail frustrating sometimes, since after slogging through a page of it you realize "oh, this is the standard argument for such-and-such, I wish they had just said so." You tend to figure that something is being explained because there is some difference that's being pointed out. I've been doing some formalization in Lean/mathlib, and it is truly an enormous amount of work to make things fully rigorous, even making it so that all notation has a formal grammar. It relies on Lean to fill in unstated details, and figuring out ways to get it to do that properly and efficiently, since otherwise the notation gets completely unworkable. |