tag:blogger.com,1999:blog-3722233.post4318994903152354716..comments2020-05-31T01:14:25.681-04:00Comments on Computational Complexity: Third Poll on P vs NP and related Questions is out now! And the winner is Harambe!Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger6125tag:blogger.com,1999:blog-3722233.post-36832413288179595452020-01-13T13:31:12.532-05:002020-01-13T13:31:12.532-05:00It can't be completely non-constructive becaus...It can't be completely non-constructive because of Levin search. But the proof may not give an effective upper bound on the degree of the polynomial needed to solve SAT.Timothy Chowhttp://timothychow.netnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-52752791625820486862020-01-13T11:49:01.154-05:002020-01-13T11:49:01.154-05:00I'm late to the party because I only just hear...I'm late to the party because I only just heard about these poll results. I noticed that one respondent mentioned the consistency of NF (New Foundations) as a problem of interest. For those who are not aware, Randall Holmes has claimed a proof that NF is consistent. I've asked a couple of experts and the situation seems to be analogous to the Kepler conjecture, in that the experts believe that the proof is probably correct, but the details are extremely complicated and so they haven't been able to check everything themselves. Holmes has revised the proof a few times to try to make it easier to understand, but the constant revisions have made the task of checking the proof harder. Holmes is fluent with proof assistants and is seriously considering using one to definitively establish correctness, but it's a highly nontrivial task.<br /><br />Perhaps if more people encourage Holmes by expressing interest in the result, it will hasten the full verification of his proof.Timothy Chowhttp://timothychow.netnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-16937191297032431782019-03-21T03:52:52.810-04:002019-03-21T03:52:52.810-04:006) Wrong. Baar Baar Dekho, a British kid of Pakist...6) Wrong. Baar Baar Dekho, a British kid of Pakistani Muslim background born in 2005 growing up in the London area found a P=NP algorithm in 2031/32 making an enormous fortune for himself as the West collapsed.Anonymoushttps://www.blogger.com/profile/03281901712454837586noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-6012162861204697832019-03-19T20:32:09.940-04:002019-03-19T20:32:09.940-04:00In response to William Hoza's answer:
Even if...In response to William Hoza's answer:<br /><br />Even if we did find an algorithm that solves SAT in polynomial time, I do not know of any guarantee that we can prove the algorithm's correctness in every case (even if it is correct in every case).<br /><br />His response, of course, suggests that some finitely-expressible tautologies do not have finite proofs. This goes against my feelings that math is never arbitrary or without reason, since a proof is no more than an explanation of why the tautology is true.<br /><br />If it weren’t for the possibility of being unable to prove the supposed algorithm’s correctness, the following logic would have applied:<br /><br />Claim:<br />Defining any finitely-expressible object x, it is impossible to prove that there is no proof of whether or not x exists.<br /><br />Not quite a proof:<br />*Suppose a proof Q exists, showing that it is impossible to prove whether or not x exists.<br /><br />*We can now conclude that x does not exist because if it did, we could give x as a proof that it does, which would contradict Q. However, this still contradicts Q: we have proven that it does not exist.<br /><br />*On second thought, x must exist, otherwise we get the above contradiction. But that still contradicts Q: we have proven that x does exist.<br /><br />*Either way, you can never proof that there is no proof of whether or not x exists, knowing there are only two possibilities: it exists or it does not. We have exhausted both.<br /><br />Except, simply showing x does not prove x exists, interestingly. That is, showing an object with some property does not prove it has that property.Anonymoushttps://www.blogger.com/profile/07615136588086240691noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-78356044310992646712019-03-18T22:31:19.224-04:002019-03-18T22:31:19.224-04:00This is a fine point of view. There are indeed som...This is a fine point of view. There are indeed some cases where we can show a poly time algorithm exists but cannot find one. Abstractly we can use the knowledge that one exists to find one that involves running lots of Turing Machines, but to REALLY have one may be difficult. For example, for any g there is an O(n^3) algorithm to test of a graph has genus g since genus-g is closed under minors and hence has a finite obstruction set. But the proof that it has a finite obs set is nonconstructive (I do not know if this particular case they know more constrivelty).<br /><br />So indeed, we may one day find that P=NP but the algorithm is non-constructive. GASARCHhttps://www.blogger.com/profile/03615736448441925334noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-23039653542102657342019-03-18T04:32:36.759-04:002019-03-18T04:32:36.759-04:00nice. I looked through it. My question to Bill and...nice. I looked through it. My question to Bill and Lance,<br />how should I interpret this the following opinion voiced in the survey:<br /><br />"I can't wait for people to realize that P=?NP is only a question about the existence of a poly-nomial time algorithm, not about the knowledge of one. We already know, for example, that there exists a polynomial time algorithm to decide membership in any given minor-closed graph family; but we don’t know how to really decide it, except for a few actual families"<br /><br />And yes, that Don Knuth voicing it.Enoreply@blogger.com