6 ms·
And even though it may be hard to find the flaw, it will be easy to verify that it is a flaw.
by jl6 9y ago
And even though it may be hard to find the flaw, it will be easy to verify that it is a flaw.
- deleted 9y ago[deleted]
- deleted 9y ago[deleted]
- GenerocUsername 9y agoIf 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.
- jacquesm 9y agoThis lines up perfectly with most software bugs. Hard to find, but once you have them easy to prove they are the cause of the problem. The difference is that in software bugs are usually fairly easy to fix, a math proof with a bug in it might not be fixable at all.
- ouid 9y agoI think you missed the joke