[webmaven]

> 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 (though the explicitness may be transitive, ie. dependencies of dependencies). Math papers often assume context that is not explicitly noted in the citations, nor those papers' citations, etc.

Instead, some of the context might only be found in other papers that cite the same papers you are tracking down. You sometimes need to follow citations both backward and forward from every link in the chain. And unlike following citations backward (ie. the ones each author considered most relevant), the forward links aren't curated and many (perhaps most) will be blind alleys (there also may be cycles in the citation graph, but these are relatively rare). But somehow you have to collect knowledge (or at least passing familiarity) with an encyclopedic corpus in order to at least recognize and place the context left implicit in any one paper in order to understand it.

It's maddening.

[CogitoCogito]

I totally agree. I think that many mathematical papers aren't explained as well as they can be. My advisor was pretty adamant that papers should not be written in some proof-chasing style like you describe and that the author should clearly include the arguments they need (citing those authors they might have learned it from) unless those arguments are truly standard. No "using a method similar to [author] in Lemma 5 of [some paper]" and instead just including it in your paper and making sure if fits in well.

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.

[webmaven]

> That is just an example of bad exposition in my opinion [and] a perfect example of why arguments like "does this proof make coq happy" totally misses the point..

In theory, some kind of checker could validate the semantics of a paper to just tell you whether the arguments made are complete. Not whether there is a correct formal proof, just pointing out any obscured leaps of faith[0]. A rough analogue to test suite coverage for code (which is also not any sort of guarantee of correctness, just basic reassurance that all (or most of) the code is tested and isn't broken in any obvious way, especially while making changes).

I'm trying to think of an equivalent for prose, and am coming up with examples like detecting conflicting descriptions of locations or named characters, or whether the author lost track of which character said which lines in the dialog.

> It's also not technically "unclear" in any notational sense

Perhaps not necessarily, but unfamiliar/borrowed/idiosyncratic notation is a perfect (and common) place for insufficient exposition to be hiding.

[0] https://imgur.com/gallery/ApzhVFj