|
|
|
|
|
|
by CogitoCogito
1666 days ago
|
|
|
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. |
|
|
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