If you’re here for the philosophy you might not have heard: a few days ago, Vinay Deolalikar of HP Labs has posted a draft paper containing a serious attempt to prove that P ? NP, one of the Clay Mathematics Institute’s Millennium Problems. The math/theory scene is all aflutter over it. This wiki page collects the current state of the discussion in various places, notably on Dick Lipton’s blog Gödel’s Lost Letter. It’s a problem in computational complexity theory—the logic connection is that the proof uses a result due to Immerman and Vardi from finite model theory, viz., that over finite ordered structures, the relations expressible in first-order logic with a least fixed point operator FO(LFP) are exactly the polynomial-time computable ones. Alas, the prevalent opinion now seems to be that the proof is probably not correct.