alt Hacker NewsBeing able to solve NP hard optimization problems would enable progress in many areas of science and technology. For example it would allow us to find poly-sized Lean proofs for theorems efficiently, since proof verification can be done in polynomial time.
It would also be amusing to annihilate nearly six decades of proofs that assume P!=NP.
Replies
manquer • today at 3:25 AM
Could also break the basic principles underlying most encryption approaches. I would rather have my bank account not stolen and internet working
➕ show 2 replies
charcircuit • today at 3:33 AM
Even if P=NP it doesn't mean that the P approach will be better than the heuristic approach we already do today.
➕ show 1 reply
Leans proof checker is not polynomial time, unfortunately. It is super exponential. Basically, because it can verify the result of any function it can prove to be total.