Timeline for Is P=NP relevant to finding proofs of everyday mathematical propositions?
Current License: CC BY-SA 2.5
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2017 at 12:32 | history | edited | CommunityBot |
replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
|
|
| Dec 2, 2010 at 7:09 | comment | added | Sridhar Ramesh | In other words, I agree... establishing P = NP (i.e., the existence of a polytime algorithm for bounded size proof search [where polytime means polynomial in the size of the proofs searched over]) isn't the thing that'd revolutionize (the formal proof search aspect of) mathematics. Finding a fast algorithm for proof search is the thing that'd revolutionize mathematics. But, naturally, the notion of a fast algorithm is much less concrete than the notion of a polytime algorithm. | |
| Dec 2, 2010 at 7:01 | comment | added | Sridhar Ramesh | The polynomial-time bit isn't really important, for supporting this point of view, so much as the conflation of "polynomial-time" with "fast, in all the instances I care about". The point being, brute force search for a proof of size <= 10^12 is much, much slower than one expects a general polynomial-time algorithm for bounded size proof search to be. But, of course, the conflation of "polynomial-time" with "fast, in all the instances I care about" is, well, leaky... | |
| Dec 2, 2010 at 6:05 | comment | added | Adam | If you're ignoring the input size, why bother using an algorithm whose one and only virtue is its running time as a function of the input size? If we assume that proofs bigger than $10^{12}$ don't matter, then brute-force search is also constant-time, so it is asymptotically just as good as any other algorithm. Worse, if your algorithm has a constant which is $2^{2^{2^{10^{12}}}}$ iit is actually worse than brute-force search not only in asymptotic terms but absolute terms as well! These are the perils of using asymptotic analysis in a situation where everything is constant | |
| Dec 2, 2010 at 5:15 | comment | added | Preyas | @Adam: A "short" proof as defined by Joseph is clearly polynomially bouned. It is in fact constant! I believe the statement "a proof could be found in time polynomial in the length of the statement and the length of the shortest proof" does a very good job of summarizing. | |
| Dec 1, 2010 at 23:59 | comment | added | Joseph O'Rourke | @Adam: I see your focus, and you are right that, in general, proof lengths cannot be bounded. Concerning the practicality of the assumption on short proofs: If short is defined, say, by fewer than $10^{12}$ symbols in some formalization, it is not clear humans can comprehend long proofs. | |
| Dec 1, 2010 at 23:40 | comment | added | Adam | (By the way, your answer would have made a good comment) | |
| Dec 1, 2010 at 22:56 | comment | added | Adam | Thanks Joseph, but my question is different -- you write "restrict attention to polynomially-long proofs", whereas I am questioning the practicality of that assumption. I actually considered posting to the complexity theory stackexchange, but ultimately the subjective part ("the propositions mathematicians care about") is the most delicate part, which is why I asked mathematicians instead of complexity theorists. | |
| Dec 1, 2010 at 22:49 | history | answered | Joseph O'Rourke | CC BY-SA 2.5 |