3 ms·
If the certificate from the SAT solver does not count as a proof, you can't blame the popular accounts. That's the language the paper authors use: The negative
by scott_s 13y ago
If the certificate from the SAT solver does not count as a proof, you can't blame the popular accounts. That's the language the paper authors use:
The negative witness, that is, the DRUP unsatisfiability certificate, is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so one may have doubts about to which degree this can be accepted as a proof of a mathematical statement.
From http://arxiv.org/pdf/1402.2184v2.pdf http://arxiv.org/pdf/1402.2184v2.pdf
- ColinWright 13y agoI think the problem is that the general public think of "proof" as the kind of thing that mathematicians sit and work out with a pencil on paper. To use the word "proof" to refer to a certificate is technically correct and appropriate in context, but deeply misleading when used outside of that context. It certainly gives the wrong impression. I also suspect we're mostly in complete agreement.