> 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.

Zing