A Proof That P Is Not Equal To NP?

Interesting, as blogged before, I am one of the few who believe that P might equal NP. I couldn't follow the whole argument from the blog, but it seems he uses results from randomized sat examples and phase transitions. As far as I know, it's just possible to generate sat examples either easy or hard exactly on transition bounds, so, interesting how that will turn out. (That it is no to say that in general, random sat-structures with a certain ratio aren't `harder' than others, it's just not a law.)

Guess I am wrong anyway in my interpretation of his proof. Feels too much like: P doesn't equal NP since sat-solving is hard, which reverses an arrow.

Still, I don't see how he lifts phase transitions: He needs to show that all possible sat-solvers have phase-transition behavior on (specific) sat instances, and I just don't see how one can generalize that from the behavior of a few current DPLL based solvers. (Got bored, read some of the arguments against his construction, starts to make some sense, again.)

A distinguished author comments on the proof at the CACM. It didn't pass scrutiny, both on the use of finite model theory -which I don't understand- and -if I read it correctly- the author has similar doubts on whether a characterization of an NP problem as being hard on phase transition boundaries of some sort is actually a characterization of an NP problem.

The latter interests me. To most people in the field, it feels natural, therefor it must be true. I don't know, I guess one of the results of his failed attempt might actually be that people start looking into whether such an assumption is actually correct. I.e., does the feeling hold up to mathematical rigor?

(Hmm, I wonder whether I got the second part of his argument right. Should look in to it. Read a bit further, of course his constructions are way more elaborate than my weak simplification of his approach. He starts of by assuming P=NP, and tries to derive a contradiction, no idea at the moment. I find it strange that he actually can derive a contradiction. He poses specific clauses, and derives that determining a solution is impossible, though he assumes a P=NP algorithm?)