Timeline for Is P=NP relevant to finding proofs of everyday mathematical propositions?
Current License: CC BY-SA 2.5
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 2, 2023 at 8:05 | comment | added | Gregory Morse | Any reference to a real world attempt at showing mathematical proofs being converted to and from SAT? The encoding would be very interesting | |
| Oct 21, 2015 at 11:34 | comment | added | Thomas Klimpel | @RyanWilliams ZFC is rich enough to express the proof of the independence of the Continuum Hypothesis from ZFC. But you have to encode the statement (of independence) in the language of ZFC (as a single proposition). So I agree with Adam that it is a fault of your algorithm, not a fault of ZFC. | |
| Dec 3, 2010 at 2:48 | comment | added | Ryan Williams | @Adam, of course, you'd need to use a proof system rich enough to express the proof of the independence of the Continuum Hypothesis from ZFC. But I'm not sure what your point is. One can find many other examples of theorems you can't prove within a given proof system; how does that show P=NP is irrelevant to finding proofs of everyday math propositions? | |
| Dec 2, 2010 at 21:19 | comment | added | Timothy Chow | +1. Regarding the constants, it might be worth mentioning that Harvey Friedman has exhibited a proposition that is provable using ZFC + "for all $n$ there exists a strongly $n$-Mahlo cardinal" with at most $10^6$ symbols but that is not provable in ZFC alone using less than $10^{1000}$ symbols (in both cases allowing abbreviations). cs.nyu.edu/pipermail/fom/2006-February/010056.html Though Friedman's proposition does not directly address Adam's question as posed, it does illustrate the subtleties of bounding the actual sizes of actual proofs (as opposed to their asymptotic growth). | |
| Dec 2, 2010 at 21:09 | comment | added | Adam | Your algorithm will fail to terminate if I choose ZFC as my axioms and the Continuum Hypothesis as my proposition. | |
| Dec 2, 2010 at 17:04 | history | answered | Ryan Williams | CC BY-SA 2.5 |