6 ms·
If only we had a way to make finding the flaw as easy as verifying the flaw
by GenerocUsername 9y ago
If only we had a way to make finding the flaw as easy as verifying the flaw
- Filligree 9y agoI don't think it would be possible to make finding it as easy as verifying it, but how can we prove that?
- liberte82 9y agoSomeone should research and write a paper about it.
- Halved 9y agoBut then how will we know that paper is correct?
- deleted 9y ago[deleted]
- KGIII 9y agoI'm pretty sure that the answer to that question involves a cat.
- PrunJuice 9y agoSounds hard.
- spinsser 9y agono problem
- TimTheTinker 9y agoNP-hard. /dodge
- petters 9y agoThat was the joke. :-)
- EGreg 9y agoBy using the algorithm!
- azeirah 9y agoThis is getting a bit too meta for my tastes :')
- deleted 9y ago[deleted]
- soberhoff 9y agoFinding flaws in proofs is as easy as verifying them. After all, finding a flaw amounts to just checking a proof. Finding a proof is the truly hard challenge.
- evincarofautumn 9y agoChecking a proof isn’t necessarily easy, of course, in the sense of both human hardness—such as requiring a lot of background, using dense notation, or being very long—and computational hardness, such as using a logic whose decision procedure takes exponential time.
- soberhoff 9y agoWhat kind of esoteric logic yields proofs that require exponential time to check?
- fmap 9y agoProof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexity theory for you...
- soberhoff 9y agoWell, I'm sure we can all agree that the mathematical paper we're discussing could be formalized into a proof that could be checked in linear time.
- Blaisorblade0 9y agoThat's only obvious in a vacuous sense. As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians: https://mathoverflow.net/q/226966/36016 https://mathoverflow.net/q/226966/36016 Of course, your claim is vacuously true, since you can add a trace of all steps of a proof verifier. It's also vacuously true because you can add a dump of the Internet to the proof. Neither thing is insightful. > what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step Also, for the record: actual formal proofs for (say) standard ZFC are exponentially bigger than anything you want to work with. EDIT: To clarify, I didn't mean to imply I'm some authority, just to suggest I'm not so obviously* an idiot. Which was maybe stupid anyway.
- manyoso 9y agoMy favorite comment. By far.