> However, the paper itself and the formalization that it claims for support are not
in a form that is readily usable to anyone who wants to understand or check it. This is
not just because of the needless length or complexity of the argument (which is indeed
overwhelming as presented), or because the formal repository is not in normal form, or
because much of the text is misleading or poorly organized, but mainly because there
is so much irrelevant puff to push through.
