Earlier quoted context omitted.
> There's so much "pure" and "universal" about math, but the humans who write about it are too lazy to write about it in a rigorous manner. Are you sure it's laziness? Maybe it's a result of there not actually being any universal notation (not even within subfields) or the exactness you refer to really isn't necessary. This doesn't mean that unclear exposition is a good thing. Mathematical writing (as with all writin…
> But clarity doesn't require some sort of minutely perfectly consistently notation which would be required by a computer I made this point in another comment, but I think it bears repeating and elaboration: Consistency isn't required (at least outside any single paper), but explicitness would be a tremendous boon. Software incorporates outside context all the time, but it pretty much always does it explicitly (thoug…
That is just an example of bad exposition in my opinion. It's also not technically "unclear" in any notational sense so it's a bit of an aside from this argument. But I agree with you 100% that it is bad bad bad. This is a perfect example of why arguments like "does this proof make coq happy" totally misses the point.