4 ms·

If there already is a proof of P-NP which is correct but not yet recognized it can probably be found on this page: https://www.win.tue.nl/~gwoegi/P-versus-NP.ht

by zaik 5y ago

If there already is a proof of P-NP which is correct but not yet recognized it can probably be found on this page: https://www.win.tue.nl/~gwoegi/P-versus-NP.htm https://www.win.tue.nl/~gwoegi/P-versus-NP.htm (If you can verify any proof using Isabelle or Coq PM me.)

sasaf5 5y ago
Whenever I end up in this list I always wonder whether all these proofs have been refuted. I assume they must have been, considering the problem is still open. But it would be nice if the author had linked to the refutation of at least a few of them. Edit: I now noticed that a few of them have: 3.[Equal]:... Zhu Daming, Luan Junfeng and M. A. Shaohan (all affiliated with Shandong University, China) refute these claims in their paper "Hardness and methods to solve CLIQUE" (Journal of Computer Science and Technology 16, 2001, pp 388-391).
- zaik 5y ago
  > I always wonder whether all these proofs have been refuted Sadly, no. I have talked to the author of one of those papers and apparently there is not a lot of motivation to check new proof attempts from the relevant people anymore.
  - fjfaase 5y ago
    It is probably because the proof is either relativizing, natural or algebrizing. It has been proven that those types of proofs are not going to work. The people who submit these kind of proofs often do not understand that they are never going to work. Why would you, as a serious mathematician that understands this to spend your energy to refute some proof for which you know that it already has been refuted. It is the same why designs of peperpetium mobilium devices are not being refuted.
bawolff 5y ago
> (If you can verify any proof using Isabelle or Coq PM me.) Rofl. Yep, if i write a machine checkable proof of the most famous open problem in all of computer science, that's definitely the first thing i'll do.
- baq 5y ago
  If it indeed points to a n^100 algorithm (or p!=np), I’d do it. It’d greatly expedite collecting the Clay’s prize money to have someone recognizable validate the proof ;) If it was n^10, well, likely different story, involving three letter agencies, I’m afraid.
  - bryanrasmussen 5y ago
    >I’d do it. It’d greatly expedite collecting the Clay’s prize money to have someone recognizable validate the proof yeah, but in my case (and presumably the previous commenter's case) I don't know who Zaik on HN is and if they are recognizable in the field. That they asked increases my feeling that it is likely they are recognizable but surely anyone who solves p!=np isn't going to just follow something as irrational as a feeling.
    - bawolff 5y ago
      I mean its still a million dollars, and money makes people do crazy things. I'd, i don't know, figure out some way to cryptographically timestamp a hash of the proof first at least.
      - bryanrasmussen 5y ago
        finally the killer app for the blockchain! Before I release my proof I will of course have to develop my ethereum app to verify origins of mathematical proofs.
        BoorishBears 5y ago
        or like... tweet the SHA256 of the proof text.
        bawolff 5y ago
        Not really a new application for bitcoin. Trusted timestamping has been considered a secondary use case for bitcoin for a ling time. There's even services lìke https://en.m.wikipedia.org/wiki/OpenTimestamps https://en.m.wikipedia.org/wiki/OpenTimestamps
jhanschoo 5y ago
Presumably such a formalization is precluded by easy formalizations of executions of Turing machines; already computer scientists describe Turing machines and their executions in most proofs in extremely informal ways because of their tediousness. It would already be a miracle if we had clear formalizations of proofs of major complexity results regarding Turing machines.
- zaik 5y ago
  You might be interested in this: https://github.com/uds-psl/coq-library-complexity https://github.com/uds-psl/coq-library-complexity
  - jhanschoo 5y ago
    TIL!
cevi 5y ago
Sadly, this page hasn't been updated since 2016. I'd love to see some of the more recent attempts at proofs collected somewhere!

by zaik 5y ago

sasaf5 5y ago

Whenever I end up in this list I always wonder whether all these proofs have been refuted. I assume they must have been, considering the problem is still open. But it would be nice if the author had linked to the refutation of at least a few of them. Edit: I now noticed that a few of them have: 3.[Equal]:... Zhu Daming, Luan Junfeng and M. A. Shaohan (all affiliated with Shandong University, China) refute these claims in their paper "Hardness and methods to solve CLIQUE" (Journal of Computer Science and Technology 16, 2001, pp 388-391).

zaik 5y ago
> I always wonder whether all these proofs have been refuted Sadly, no. I have talked to the author of one of those papers and apparently there is not a lot of motivation to check new proof attempts from the relevant people anymore.
- fjfaase 5y ago
  It is probably because the proof is either relativizing, natural or algebrizing. It has been proven that those types of proofs are not going to work. The people who submit these kind of proofs often do not understand that they are never going to work. Why would you, as a serious mathematician that understands this to spend your energy to refute some proof for which you know that it already has been refuted. It is the same why designs of peperpetium mobilium devices are not being refuted.

bawolff 5y ago

> (If you can verify any proof using Isabelle or Coq PM me.) Rofl. Yep, if i write a machine checkable proof of the most famous open problem in all of computer science, that's definitely the first thing i'll do.

baq 5y ago
If it indeed points to a n^100 algorithm (or p!=np), I’d do it. It’d greatly expedite collecting the Clay’s prize money to have someone recognizable validate the proof ;) If it was n^10, well, likely different story, involving three letter agencies, I’m afraid.
- bryanrasmussen 5y ago
  >I’d do it. It’d greatly expedite collecting the Clay’s prize money to have someone recognizable validate the proof yeah, but in my case (and presumably the previous commenter's case) I don't know who Zaik on HN is and if they are recognizable in the field. That they asked increases my feeling that it is likely they are recognizable but surely anyone who solves p!=np isn't going to just follow something as irrational as a feeling.
  - bawolff 5y ago
    I mean its still a million dollars, and money makes people do crazy things. I'd, i don't know, figure out some way to cryptographically timestamp a hash of the proof first at least.
    - bryanrasmussen 5y ago
      finally the killer app for the blockchain! Before I release my proof I will of course have to develop my ethereum app to verify origins of mathematical proofs.
      - BoorishBears 5y ago
        or like... tweet the SHA256 of the proof text.
      - bawolff 5y ago
        Not really a new application for bitcoin. Trusted timestamping has been considered a secondary use case for bitcoin for a ling time. There's even services lìke https://en.m.wikipedia.org/wiki/OpenTimestamps https://en.m.wikipedia.org/wiki/OpenTimestamps

jhanschoo 5y ago

Presumably such a formalization is precluded by easy formalizations of executions of Turing machines; already computer scientists describe Turing machines and their executions in most proofs in extremely informal ways because of their tediousness. It would already be a miracle if we had clear formalizations of proofs of major complexity results regarding Turing machines.

zaik 5y ago
You might be interested in this: https://github.com/uds-psl/coq-library-complexity https://github.com/uds-psl/coq-library-complexity
- jhanschoo 5y ago
  TIL!

cevi 5y ago

Sadly, this page hasn't been updated since 2016. I'd love to see some of the more recent attempts at proofs collected somewhere!