[FOM] Foundational Challenge

[Thomas Klimpel]

Lew Gordeew wrote:
> Peer-reviewed proof of NP = PSPACE is already available
>
> http://dx.doi.org/10.18778/0138-0680.2020.16
> https://czasopisma.uni.lodz.pl/bulletin/article/view/8169
>
> (Warning: it's hard proof theory)

What happened to the LEAN formalization that Edward Hermann Haeusler
wanted to finish first
(https://cs.nyu.edu/pipermail/fom/2019-July/021620.html), before
publishing (yet another incomplete version of) this article? What
happened since https://arxiv.org/abs/1907.03858, on which this new
proof is based according to the abstract, and where he did not appear
as co-author?

Why did neither of you ever update https://arxiv.org/abs/1609.09562,
even so your subsequent publications clearly show that you accept that
this version contains a serious mistake?

A peer-reviewed article is certainly a nice achievement, but it
shouldn't be overstated in the context of ambitious proofs. A link to
a funny reference with many examples was given in
(https://www.scottaaronson.com/blog/?p=3409#comment-1743482): "This
P!=NP paper from 2017
(http://cris.teiep.gr/jspui/bitstream/123456789/1482/1/The_3rdClay_version1_Conference.pdf)
contains a nice reference section of P vs NP proofs which actually
managed to get published in some seemingly serious journals, like IEEE
Latin America Transactions."


Thomas