[FOM] Gordeev and NP = PSPACE again

[Edward Hermann Haeusler]

Dear Tim,

     Thank you for the question and sorry for the delay in answering it. I
was on holiday (very short indeed)
    Concerning the decision of using LEAN as the ITP to formalize and proof
the conjecture (NP=PSPACE), my students know it better than other ITPs. We
give some classes on it and they have been using it.  LEAN's learning
impedance in this case is lower. The current goal is to formalize the proof
of the main lemma on existence of redundancy in some particular
superpolynomially sized class of trees. We have to encode many of the
concepts, it is true, but we have more driving power in the formalization
steps instead. You are right about the fact that the intended meaning and
the obtained semantics may be (slightly) different, but it seems that we
have no way to escape from posing an informal argument to adjust this
difference.
After showing that the removal of redundancy yields a polynomially sized
dag that can be checked for being a proof of a tautology in minimal logic
we can draw the conclusion that NP=PSPACE.  The details will be provided
and submitted  only after a complete verification of the formalization by
LEAN. I would like to have no incompleteness in the argument.

Edward  Hermann Haeusler


On Fri, Aug 2, 2019 at 12:33 AM Timothy Y. Chow <tchow at math.princeton.edu>
wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
>

-- 
Edward Hermann Haeusler
Associate Professor
Department of Informatics
PUC-Rio
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190812/8ad7eba0/attachment.html>