Erroneous Proof of NP=PSPACE

I was excited to see a claim that NP=PSPACE (pdf) on the Theory of Computing Blog Aggregator.

Unfortunately, Lemma 3 is in error.  A simple counterexample: the QBF “Ay Ex p(x,y)” where p(x,y)=”(x or not(y)) and (not(x) or y)” is predicted by Lemma 3 to be equivalent to “Ex x and not(x)” which is false.  (A means for all, E means exists).  But suppose y is false - then x=false makes p(x,y) true.  Alternatively, let y be true - then x=true makes p(x,y) true.  This means that for all y, there’s an x such that p(x,y), which is the original QBF.

For PSPACE to be in NP, you would need to be able to verify short proofs (of polynomial size and in polynomial time) verifying the correctness of a program’s output (provided the program uses space bounded by some polynomial of the input size).  That would be amazing.