[FOM] Gordeev and NP = PSPACE again

[Timothy Y. Chow]

Edward Hermann Haeusler wrote:

> As prof. Gordeev knows, we took slightly different directions in order 
> to proof our result. In order to avoid incomplete versions, I and my 
> students, are formalizing our version in LEAN. Only after each relevant 
> part is formalized and checked there will be an article published it in 
> arxiv......

This is very interesting.

I'm curious as to why you chose Lean as opposed to some other proof 
assistant?

As you know, one thing that a skeptic can say even when shown a formal 
proof is, "Yes, you've produced a formal proof of *something*, but what 
you've proved isn't the statement that we know as `NP = PSPACE.'"  I'm 
curious how you plan to meet this objection (of course, assuming that your 
project succeeds and that someone voices this objection).  Does Lean 
already have a substantial amount of computational complexity theory 
encoded in it, so that there won't be any major doubts in the community 
about whether what you have proved is indeed the assertion that NP = 
PSPACE?

Tim