5 ms·
New Short Cut Found for Long Math Proofs (1992)
- jimhefferon 11y agoNot sure why this is on the front page today.
- ajkjk 11y agoConsidering it's 23 years old, I think it has a roughly equal chance of being submitted on every day - and today's the day.
- akkartik 11y agoIs this the paper they're talking about? http://people.csail.mit.edu/madhu/papers/1992/almss-conf.pdf http://people.csail.mit.edu/madhu/papers/1992/almss-conf.pdf
- strong_ai 11y agoYes. Note both the article and the paper are from 1992.
- brinker 11y agoThese types of articles are always frustrating, in that they very rarely provide an even halfway decent explanation of the math or science involved (if they do, it is buried deep), and are instead little more than a repetitive explanation of the importance of the work, judged by quotes from as many people as humanly possible. This article (which says very little) is still probably too long with all the fluff added around the actual discovery.
- klipt 11y agoIf only there were a way to check the accuracy of a long article by scrutinizing it in only a few spots...
- kazinator 11y agoUnfortunately, there is only a way to check the accuracy of a long article by scrutinizing a complicated mathematical transformation of it in a few spots.
- pramodliv1 11y agoFlipboard Engineering published a blog post on solving this problem http://engineering.flipboard.com/2014/10/summarization/ http://engineering.flipboard.com/2014/10/summarization/
- murbard2 11y agoThis is about the PCP theorem https://en.wikipedia.org/wiki/PCP_theorem https://en.wikipedia.org/wiki/PCP_theorem An interesting application are SNARKs, a fully generic type of non interactive zero knowledge proof of knowledge. They can be used to preserve transaction privacy and fungibility in cryptocurrencies for instance.
- deleted 11y ago[deleted]
- deepsun 11y agoSo it's 23 years passed and are there any practical implementations that mathematicians would use? Since this work can be applied only to proofs that were recorded in machine-readable format (like Mizar), I suppose it's much harder _to record_ a proof in machine-readable format, than to really go ahead and check all the pages manually.
- pmiller2 11y agoNot that I know of, for the reasons you suggest. AFAIK nobody is seriously using formats like Mizar when we have actual proof assistants available that can check the proof, which kind of obviates the need to use the PCP theorem at all.
- nickpsecurity 11y agoWould there be any remaining value for such a tool in checking proofs if already using a standard, proof-checker? Sort of a "get's it done faster/easier" argument or perhaps like in software a "catch obvious problems in ill-specified work earlier" sort of thing?
- cozzyd 11y agoI never had Motwani as a professor but I've only heard good things about him. RIP.
- plonh 11y ago>As is the custom in mathematics and theoretical computer science, the result gains credibility not by having been sent to a journal and reviewed by other scientists but by having been vouched for by leaders in the field WTF?
- sriku 11y agoI hate to admit my inability to convince myself that this wasn't an April fool's joke!