The following argument from the blog post is wrong: "First, write a bash script P1 that runs a SAT solver on every possible SAT problem and halts if any of the

The following argument from the blog post is wrong: "First, write a bash script P1 that runs a SAT solver on every possible SAT problem and halts if any of them take exponential time. You don't actually have to run P1, just call HALTS(P1, Solver) to see if the solver solves all problems in polynomial time." The difficulty here is that it could turn out that there's a SAT algorithm that is better than exponential, but the SAT solver used in the experiment does have worst case exponential time. What has to be proved, to prove P != NP, is that there is no possible SAT algorithm that has sub-exponential worst case time.