I first read about this on hacker news, which I encourage more people to subscribe for quality content in the tech/science space. Many people have raised doubts (including Scott Aaronson whose Democritus blog I used to follow) about the validity of the proof, but few seem to be able to point out any flaw to date. I found it generally well-written in the beginning, except some of the preliminary results seem too basic, such as the conversion between CNF and DNF, such as Lemma 1 and Lemma 2. The writing style reminds me of my REU project during summer 2007, when I wrote my first original research papers: the balance between non-triviality and clarity is often a newbie’s struggle.

In any case, I was happy with most of the arguments until the proof of Theorem 2. I am not questioning the correctness of its statement since I haven’t had time to try to find a counterexample or come up with a proof independently. The assertion, “By construction, no variable can be removed from without destroying this property”, however, does seem wrong to me. Here is a simple counterexample:

Take , , , and , where implicit product means and () and sign means or (). Furthermore let and . Then is clearly an -clause but not a prime one, since alone is an -clause.

Now I am not sure if this step is critical to the rest of the proof of Theorem 2, but I am suitably discouraged at this point to put in more salvaging time. This also highlights another complaint of mine, which is the unnecessarily complicated notation , which I feel can be replaced by something more standard and light-handed.