Recent advances in automated theorem proving support my first postulate.

My second post in this blog was a postulate that most algorithms are outside the scope of computer science because even if they are created and proved correct, they still cannot be understood. In that post I raised an open question: “‍Do human-defined problems ever have only larger-than-mind-sized solutions?‍” Advances in automated theorem proving, brought to my attention by a recent article¹¹  M. Heule and O. Kullman, “‍The Science of Brute Force‍” In CACM 60(8) pp. 70–79. August 2017. DOI:10.1145/107239 in Communications of the ACM do not address this postulate or its associated open questions directly, but they do provide related correct-but-incomprehensible results in another field.

Since I expect most of my readers have not taken a theory of computation course and thus will find that article a bit opaque, I will attempt a summary.

• Many succinct mathematical claims can be written in a much more verbose form called a “‍Boolean Satisfiability problem‍” which, though longer, consists of only very simple pieces.

• Each satisfiability problem is either “‍satisfiable‍” or “‍unsatisfiable‍”, corresponding roughly to the original claim being either true or false.

• We are getting very good at writing programs that can solve these satisfiability problems, providing a proof of (un)satisfiability along the way.

• Proofs of satisfiability are small and almost self-evidently true. Proofs of unsatisfiability are much longer, but can be checked by extremely simple (and thus easy to trust) algorithms.

• When we convert unsatisfiability proofs back into the original mathematical domain, they look like huge numbers of detailed proof-by-cases²²  e.g. a proof that you cannot color a map of the united states using three colors might include the case split “‍Either Wyoming and Wisconson are given the same color, or they are given different colors. Consider first the case where they have the same color…‍” splits.

• Some simple(ish)-to-state and interesting (to some people) problems have very large proofs; for example, the Boolean Pythagorean Triples Problem’s best known proof is 200TB long. On days when I do little more than read, I read about 1MB³³  I’m being fast-and-loose with numbers here. I read about 1MB of ASCII (letters and spaces); that’s less than 150KB of information, because ASCII is not very compact. But I don’t happen to know how compact the BPTP proof is, and this is just a “‍which is big‍” argument anyway. a day; thus, it would likely take me more than 500,000 years to read this proof.

• There is strong (but not yet iron-clad) reason to believe that many interesting problems (including the correctness of some algorithms) may only have these incomprehensibly-large proofs.

The above-summarized work addresses the understandability of proofs, not algorithms, but it does suggest that there are interesting problems with only incomprehensible solutions. While those problems are currently theorems and the solutions currently proofs, I don’t see any intrinsic reason why the same shouldn’t apply in other domains. The Frustrating Universe, where we can’t understand why a program works even if we know that it does, appears more probable now than it did when I postulated its existence six years ago.