## Stream: Coq users

### Topic: Possible polynomial NP-complete solution

#### Victor Porton (Apr 09 2021 at 20:01):

I proved a theorem and then "Linux guessed from it an efficient NP-complete algorithm" :-) and my computer broke, so I write in this chat instead of a normal communication. That was a joke, next there is a serious theorem:

#### Victor Porton (Apr 09 2021 at 20:09):

I've proved that my algorithm is NP-complete under assumption that P=NP. bit.ly/2Q5Xv2V0 Formalize it!

#### Joshua Grosso (Apr 09 2021 at 20:09):

I get a 404 for the bit.ly link :-(

#### Victor Porton (Apr 09 2021 at 20:11):

https://math.portonvictor.org/2021/04/08/my-algorithm-that-is-np-complete-in-the-case-if-pnp/

#### Victor Porton (Apr 09 2021 at 20:13):

It is simpler than you can imagine: proving provability of invertibility of an algorithm is clearly an NP-complete problem. To solve it I just enumerate and run parallel all algorithms.

#### Victor Porton (Apr 09 2021 at 20:14):

Previous message had two typos, corrected.

#### Joshua Grosso (Apr 09 2021 at 20:29):

I skimmed the paper, and I'm confused on the part about enumerating all algorithms—wouldn't this require that the set of all possible algorithms be countably infinite?

#### Victor Porton (Apr 09 2021 at 20:32):

The set of all algorithms is obviously countably infinite.

#### Joshua Grosso (Apr 09 2021 at 20:35):

Oh yeah, ignore me :-P

#### Joshua Grosso (Apr 09 2021 at 20:36):

In that case, I guess my next question is: Can you interleave an infinite number of algorithms? (Wouldn't it take an infinite amount of time to finish e.g. the first step?)

#### Victor Porton (Apr 09 2021 at 20:37):

Loop N algorithms adding one more algorithm after each loop.

#### Joshua Grosso (Apr 09 2021 at 20:39):

Oh yeah, I remember that now (sorry, I don't remember much of the details from when I learned about complexity)

#### Victor Porton (Apr 09 2021 at 20:39):

0 0 1 0 1 2 0 1 2 3...

#### Victor Porton (Apr 09 2021 at 20:43):

So will somebody formalize my proof soon?

#### Joshua Grosso (Apr 09 2021 at 20:45):

Just checked out the references in the paper and they pose a question that I'm also stuck on: For the algorithm to be in polynomial time, I assume each individual A_n also does. Is that requirement explicitly mentioned in the paper?

#### Victor Porton (Apr 09 2021 at 20:46):

No, it's enough that just one "good" A is polynomial

#### Victor Porton (Apr 09 2021 at 20:47):

Just one of An finishes normally, the rest are terminated in the middle.

#### Victor Porton (Apr 09 2021 at 20:51):

BTW, my first solution attempt used (without me noticing that I have no definition) fractional number of algorithm steps. Then I was doing a sum of infinite number of steps being finite. That's not defined, but I think, it can be defined with some new concepts. But my new algorithm is simpler.

#### Victor Porton (Apr 09 2021 at 20:52):

An is even not required to halt.

#### Joshua Grosso (Apr 09 2021 at 20:52):

Okay I lied, I do have another question: How do we know when we've found the "correct" A_n? (More explicitly, does A_n return "yes"/"no", or does it return an actual proof of that fact? I think the latter, but I want to make sure I'm understanding it right.)

#### Victor Porton (Apr 09 2021 at 20:54):

An "should" return a proof (or not a proof, in which case we ignore the result). Most results will be "garbage".

#### Victor Porton (Apr 09 2021 at 20:56):

It returns a proof in some formal system like first-order predicate calculus. Maybe for coq implementation, it's easier to use a lambda calculus.

#### Joshua Grosso (Apr 09 2021 at 20:57):

Makes sense. In that case, how do we know that a polynomial A exists? If A returns a proof of the correctness of an algorithm A', I don't think that A' being polynomial necessarily implies A is polynomial (cause proofs can get really big).

#### Joshua Grosso (Apr 09 2021 at 20:58):

(Again, please pardon any errors I am making, will make, and/or have been making; I'm only a simple undergrad :-P)

#### Victor Porton (Apr 09 2021 at 20:59):

So, the proof idea is that it searches for the first polynomial NP-complete algorithm and it produces the result. But it may terminate earlier if we find another algorithm that isn't polynomial or NP-complete but solves the problem for a particular input data.

#### Joshua Grosso (Apr 09 2021 at 20:59):

But doesn't each algorithm we run during the interleaving step actually return a proof, rather than just "yes"/"no"?

#### Victor Porton (Apr 09 2021 at 21:00):

We assume existence of some NP-complete (polynomial) algorithm by the conditions of my theorem.

#### Joshua Grosso (Apr 09 2021 at 21:02):

I thought NP-complete only says "there exists a polynomial-time verifier" but not necessarily that the verifier returns a proof?

#### Joshua Grosso (Apr 09 2021 at 21:03):

(in which case you have to know a priori which verifier is the right one)

#### Victor Porton (Apr 09 2021 at 21:03):

On your first question. Proof size is polynomial because in our assumptions run time of the entire algorithm is polynomial

#### Victor Porton (Apr 09 2021 at 21:04):

I use proofs as certificates. I specially specialized the problem for all certificates to be proofs.

#### Victor Porton (Apr 09 2021 at 21:05):

An returns a proof. Verifier returns like yes/no

#### Joshua Grosso (Apr 09 2021 at 21:09):

Is it valid to constrain the certificates like that? I was under the impression that NP-completeness only means 1) there exists some polynomial-length certificate as well as 2) some polynomial-time algorithm to check it (in which case the certificate itself doesn't need to be a proof)

#### Victor Porton (Apr 09 2021 at 21:10):

Any finite object can be used as a certificate. Proofs are finite objects. So nothing invalid.

#### Joshua Grosso (Apr 09 2021 at 21:17):

"A certificate can be a proof" doesn't necessarily imply that "All certificates are proofs" though, unless I'm getting lost somewhere

#### Victor Porton (Apr 09 2021 at 21:18):

In general not all certificates are proofs. But in my article all certificates that I mention are proofs.

#### Victor Porton (Apr 09 2021 at 21:20):

In other words, I replaced the problem of finding an NP-complete algorithm with equivalent problem of finding an NP-complete algorithm with proofs as certificates.

#### Joshua Grosso (Apr 09 2021 at 21:22):

Couldn't it be true though that, for some NP-complete problem, no polynomial-length proof exists (instead, only a polynomial-length/-time certificate/certifier combination)?

#### Victor Porton (Apr 09 2021 at 21:23):

I'm not quite sure. I think, you are right. But there is no need to consider all NP-complete problems (I consider just one).

#### Joshua Grosso (Apr 09 2021 at 21:25):

Oh I see: Is it correct to say, then, that this decision algorithm only works for NP-complete problems which we know beforehand to have polynomial-length proofs?

#### Victor Porton (Apr 09 2021 at 21:26):

No. My algorithm always solves my problem. The only question if it's polynomial. I proved it's polynomial if p=np.

#### Victor Porton (Apr 09 2021 at 21:29):

I consider only one NP-complete problem

#### Joshua Grosso (Apr 09 2021 at 21:31):

So is the overall statement, then, that there exists at least one NP-complete problem for which this algorithm is correct?

#### Victor Porton (Apr 09 2021 at 21:32):

Yes, and moreover I proved it's polynomial if p=np

#### Victor Porton (Apr 09 2021 at 21:33):

You are a Christian. I have a theological theory: the mind of Jesus is an NP complete algorithm

#### Joshua Grosso (Apr 09 2021 at 21:35):

Victor Porton said:

Yes, and moreover I proved it's polynomial if p=np

Is P=NP even required for the overall algorithm to be polynomial, then? Couldn't the algorithm just search through all possible proofs even if P<>NP, since a polynomial-length proof must exist by the original assumptions?

#### Victor Porton (Apr 09 2021 at 21:37):

If p!=np, then my algorithm isn't polynomial, as the inverse statement proves p=np

#### Victor Porton (Apr 09 2021 at 21:38):

P=np if and only if my algorithm is polynomial

#### Joshua Grosso (Apr 09 2021 at 21:39):

Suddenly I'm wondering: Doesn't the existence of this algorithm imply that the NP-complete problem we're solving isn't actually NP-complete?

#### Joshua Grosso (Apr 09 2021 at 21:39):

because the algorithm, as far as I can tell, never actually uses the assumption that P=NP

#### Joshua Grosso (Apr 09 2021 at 21:40):

meaning that we have a polynomial-time algorithm for solving this particular problem, which implies it's not actually NP-complete to begin with

#### Victor Porton (Apr 09 2021 at 21:40):

I don't understand your logic. But I proved (unless some error) that my problem is NP-complete. The proof is that my problem subsumed proof finding.

#### Joshua Grosso (Apr 09 2021 at 21:40):

Or, summarized: I think this algorithm might actually be a proof that an NP-complete problem cannot have a polynomial-length proof

#### Joshua Grosso (Apr 09 2021 at 21:41):

Oh yeah, I've been implicitly assuming P<>NP

oops

#### Joshua Grosso (Apr 09 2021 at 21:42):

So I guess it's more a general statement, then: Any problem with a polynomial-length proof is in P.

#### Victor Porton (Apr 09 2021 at 21:42):

First, I don't know if my algorithm is polynomial. Second, p=np if and only if my algorithm is polynomial.

It's false

#### Victor Porton (Apr 09 2021 at 21:43):

Correction: it's false unless p=np.

#### Victor Porton (Apr 09 2021 at 21:57):

Will you work on formalizing this?

#### Victor Porton (Apr 09 2021 at 22:00):

Looks like I almost proved p!=np. I will tweet.

#### Victor Porton (Apr 09 2021 at 22:02):

I cannot tweet because my pc is broken. Here is my proposed p!=np proof:

#### Victor Porton (Apr 09 2021 at 22:03):

Run my algorithms An in parallel not in equal time but each two times less CPU time than the previous.

#### Victor Porton (Apr 09 2021 at 22:05):

Ignore this, my p!=np proof idea was erroneous.

#### Victor Porton (Apr 10 2021 at 05:01):

I meant: your "might be actually a proof" is false.

#### Paolo Giarrusso (Apr 10 2021 at 07:12):

FWIW: This sounds related to Levin search https://steemit.com/steemstem/@markgritter/leonid-levin-s-universal-algorithm, and especially it sounds very similar to the extension by Hutter https://arxiv.org/pdf/cs/0206022.pdf, which in addition proves optimality.

#### Paolo Giarrusso (Apr 10 2021 at 07:13):

While Hutter does not discuss NP-completeness, since his algorithm is asymptotically optimal on each given problem, if P = NP it’d also be polynomial for NP problems. (EDIT: IIUC).

#### Victor Porton (Apr 10 2021 at 08:48):

So, my discovery isn't as big as I thought?! It was known a constructive solution for p=np if p=np? Why do I see everywhere the claim that constructivity of p=np is unknown?!

#### Paolo Giarrusso (Apr 10 2021 at 09:35):

Those are good questions, I am only pointing to potential related work in case that’s helpful.

Hutter does not discuss constructivity explicitly, and his proof seems a conventional proof in classical logic, not intuitionistic logic (I have no idea how hard it’d be to adapt it).

#### Paolo Giarrusso (Apr 10 2021 at 09:55):

If I may also ask questions, I’m also confused about something, and I was unable to resolve my confusion by reading what your PDF:

Victor Porton said:

It is simpler than you can imagine: proving provability of invertibility of an algorithm is clearly an NP-complete problem. To solve it I just enumerate and run parallel all algorithms.

Why is that NP-complete, especially in an arbitrary formal system? It’s obvious that there are verifiable certificates for this problem, but that alone doesn’t restrict the problem to NP (let alone NP-complete); the certificate-checking must be polynomial in the size of the input.

In this case, the input is algorithm A, the certificate is a proof P that A is invertible, and the certificate-checker must check the proof against the formal system, in time polynomial in the size of A.

I don’t see why the size of P should be bound by the size of A, even informally.

#### Victor Porton (Apr 10 2021 at 13:14):

No, the input of the algorithm, whose NP-completeness we check is X, A processes this input X. An is an intermediary data not the input data, maybe you confuse that A is an input of V. It's really so, but we don't check if V is NP-complete, so that's irrelevant.

#### Paolo Giarrusso (Apr 11 2021 at 10:34):

Well, I wasn't using the symbols in the paper...

#### Paolo Giarrusso (Apr 11 2021 at 10:35):

My point was just, it's not clear to me that "proving provability of invertibility of an algorithm is clearly an NP-complete problem"

#### Paolo Giarrusso (Apr 11 2021 at 10:39):

in fact, I'm skeptical that problem is in NP: I don't think the size of the certificate is polynomial in the input algorithm (nevermind the proof of completeness)

#### Paolo Giarrusso (Apr 11 2021 at 10:39):

See for instance the 2nd def. in https://en.wikipedia.org/wiki/NP_(complexity)#Formal_definition — the 2nd clause demands that the size of the certificate is polynomial.

#### Paolo Giarrusso (Apr 11 2021 at 11:17):

To be more specific, the paper says this work applies to any formal system — but it's surprising if that applies to the standard presentation of first-order logic. That logic doesn't have cut, hence proof size is blown up exponentially (see e.g. https://en.wikipedia.org/wiki/Cut-elimination_theorem#Consequences_of_the_theorem and the linked https://scholar.google.com/scholar?hl=en&q=Don%27t+Eliminate+Cut+boolos&btnG=&lr=lang_de%7Clang_en%7Clang_it).

#### Victor Porton (Apr 12 2021 at 10:09):

Paolo Giarrusso said:

in fact, I'm skeptical that problem is in NP: I don't think the size of the certificate is polynomial in the input algorithm (nevermind the proof of completeness)

It' spolynomial, because the NP-complete (by theorem assumption) algorithm B generates a polynomial-size certificate.

#### Paolo Giarrusso (Apr 12 2021 at 19:19):

Is B is producing proofs in FOL without cut? Those can't be polynomial, so maybe some assumption is unsatisfiable (maybe like https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Possible.20polynomial.20NP-complete.20solution/near/233896533, but I'm not sure if my question is on the same point)

#### Paolo Giarrusso (Apr 12 2021 at 19:24):

1. On the formalism, in fact, I already struggle seeing whether at page 1 that `X is an NP ⇒ R(X)` actually follows: `X in NP` does not imply that `X` produces a formal proof in our chosen formal system, while `R(X)` does.

#### Paolo Giarrusso (Apr 12 2021 at 19:26):

1. also, I'm not convinced by the definition of NP. IIUC, you say that `X is NP` if and only if `∀ Y, X(Y) = Z ⇒ ∃polynomial-time algorithm X' : X' (Z) = Y.`. However, `X in NP` seems closer to `∃polynomial-time algorithm X': ∀ Y, X(Y) = Z ⇒ X' (Z) = Y.`, which is strictly stronger.

#### Paolo Giarrusso (Apr 12 2021 at 19:30):

On 1, the first problem seems that FOL certificates might be exponentially bigger than the actual certificates for NP completeness. The second is that R seems to demand X to produce not just a certificate, but a proof of correctness of itself — possibly on all inputs depending on the actual statement ("for every algorithm Y" means "∀ Y" but I can't guess where that goes, relative to all other quantifiers described informally)

Last updated: Sep 30 2023 at 06:01 UTC