Timeline for Is P=NP relevant to finding proofs of everyday mathematical propositions?
Current License: CC BY-SA 2.5
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 2, 2023 at 8:14 | comment | added | Gregory Morse | Quadratic runtime would likely solve every known mathematical problem if the constant were reasonable. Proofs of size 2^56 are easily possible on supercomputers considering squaring raises the exponent by only one. So if it's not a galactic algorithm, it would make mince meat out of just about every formulation that exists. | |
| Jun 5, 2011 at 20:43 | comment | added | porton | cl.cam.ac.uk/research/hvg/Isabelle mizar.org | |
| Jun 5, 2011 at 20:42 | comment | added | porton | @Andreas Blass: You've mentioned "system in which proofs are done should, for these purposes, not be simply an axiomatic system like ZFC with its traditional axioms and underlying logic. It should be a system that allows you to formally introduce definitions. In fact, it should closely approximate what mathematicians actually write." There are two such practically usable systems (including automatic proof checkers): <a href="cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle</a> and <a href="mizar.org">Mizar</a>. | |
| Mar 8, 2011 at 18:35 | comment | added | Peter Shor | Although I can't remember any of the details offhand, I've seen a few algorithms that output an exponentially long list in polynomial time/item on it. | |
| Jan 31, 2011 at 0:27 | comment | added | Timothy Chow | @gowers: Output. The length of the permanent is polynomial in the input size so we can't expect an algorithm that runs in time polynomial in the length of the output. | |
| Dec 3, 2010 at 18:25 | comment | added | gowers | @Tim: Are you talking about output or output <em>length</em>? | |
| Dec 3, 2010 at 0:22 | comment | added | Tom Church | @Adam: any algorithm which outputs a proof (if it exists) of a given proposition has running time bounded below by the length of the shortest proof—it needs time to write down the answer! And an algorithm which runs faster but does not output a proof would not be very satisfying to mathematicians; if a computer told me "the twin primes conjecture is true" without giving a proof, that wouldn't affect my life at all. | |
| Dec 2, 2010 at 23:37 | comment | added | Adam | I didn't say it was uncommon for algorithms to be polynomial in their output; I said it was unusual to use that as the primary metric [of an algorithm's merit]. | |
| Dec 2, 2010 at 22:51 | comment | added | Timothy Chow | @Adam: It's actually not so uncommon to have algorithms that run in time polynomial in the output rather than the input. For example, computing the permanent is #P hard, but it can be computed in time polynomial in its value. | |
| Dec 2, 2010 at 21:28 | comment | added | Adam | I should also add that it feels a bit peculiar: the proposition is the input to the process, and the convention is usually to measure asymptotic time in the size of the input rather than the size of the output. But the argument is still correct; it's just using an unusual metric. | |
| Dec 2, 2010 at 21:28 | comment | added | Adam | Thank you, Andreas. Allow me to paraphrase the insight you've provided: nobody is trying to claim that anything will happen in time polynomial in the size of the proposition. The only claims being made are about things happening in time polynomial in the size of the shortest proof, if any. This side-steps the question of formal independence if we pretend that "no proof" means "shortest proof is infinitely long". This change-of-claim definitely leaves us with something which is objectively correct (although, I must say, subjectively less satisfying). | |
| Dec 2, 2010 at 21:09 | vote | accept | Adam | ||
| Dec 2, 2010 at 19:10 | comment | added | Robin Kothari | A very interesting observation: "people might like my proof better than the lexicographically first one" | |
| Dec 2, 2010 at 18:51 | history | answered | Andreas Blass | CC BY-SA 2.5 |