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 | |
|---|---|---|---|---|---|
| Dec 3, 2010 at 1:40 | comment | added | user5810 | Reeaallyy? Then what is the n in "problem(2n) := 'There is a proof of length n that the original statement is false.'" and "problem(2n+1) := 'There is a proof of length n that the original statement is true.'"? It sure seems like proof size to me. | |
| Dec 2, 2010 at 22:08 | comment | added | Adam | "and my proof size is..." not listed as an input to your algorithm. | |
| Dec 2, 2010 at 14:51 | comment | added | arsmath | Adam, the vast majority of proofs found by humans are short. There's the occasional gigantic 100-page proof, but if the vast majority of proofs could be generated by machine, then the impact on mathematical practice would be large. | |
| Dec 2, 2010 at 5:24 | comment | added | user5810 | "Choose your axioms to be ZFC and your proposition to be the Continuum Hypothesis" and my proof size as ... ? Once it checks all potential proofs of the given size, it will halt on "no short proof" (if ZF is consistent). | |
| Dec 2, 2010 at 4:08 | comment | added | Adam | Ricky, your algorithm will not always halt. Choose your axioms to be ZFC and your proposition to be the Continuum Hypothesis. Your algorithm will run forever since there is no proof of either CH or $\neg$CH from ZFC, let alone one which is polynomial in the length of CH! Regarding your other question: if the size $|p|$ of a proof $p$ is polynomial in $n$, then $|p|\leq\underset{0\leq i<k}\sum a_i\cdot n^{b_i}$; the $a_i$ are the coefficients and the $b_i$ are the exponents (I should have written "coefficients and exponents as inputs"). | |
| Dec 2, 2010 at 3:26 | comment | added | user5810 | What are "the proof-size's coefficients"? The algorithms, including mine, take the proof's size as an additional input and always halt, with the answer "True", "False", or "no short proof" (or "inconsistency"). | |
| Dec 2, 2010 at 2:53 | comment | added | Adam | I should also add that any algorithm which always halts would necessarily need knowledge of the proof-size's coefficients as an additional input (the algorithm in Ricky's answer may fail to halt, which is why it doesn't need the coefficients as inputs). | |
| Dec 2, 2010 at 2:51 | comment | added | Adam | David, the algorithm would only work if a polynomial-sized proof existed. If one didn't, the algorithm would simply fail to terminate, but you'd never know the difference between "will never terminate" and "needs to run just a bit longer". So the algorithm would be useless without prior knowledge of the proof size. It still appears that the ramifications are being over-hyped. | |
| Dec 2, 2010 at 0:37 | history | answered | David Harris | CC BY-SA 2.5 |