Printable Version of this PageHome PageRecent ChangesSearchSign In

:13 July 2016

Extreme theorem-proving!!! Researchers have solved a single math problem (boolean Pythagorean Triples problem) using brute-force (SAT solvers on supercomputers, yay!), producing the largest proof ever - over 200 terabytes in uncompressed length. How did they check it? If a computer generated proof is too big for humans to check, what can be said of its epistemic status? That aside, this is big deal. It shows how far we have come since the time when the SAT problem's NP-completeness was understood in the early 1970's. We seem to be readily embracing SAT solvers instead of avoiding them like plague for tractability reasons. The solver community is optimistic that they can solve most SAT problems arising in practical applications. Confused? An explanation for this gap is provided by Dick Lipton in one of his blog entries.

Last modified 6 November 2016 at 1:26 am by svattam