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.
replyThat's fine, we just change the problem from "find a lean proof of length < f(n)" to "find a lean proof that can be validated in time < f(n)".
replyOh that’s unfortunate.
replyCould also break the basic principles underlying most encryption approaches. I would rather have my bank account not stolen and internet working
replyto depress you even more, it is consistent with everything that we know that P != NP and that cryptography does not exist. So there is a worst of both worlds, and we cannot rule it out.
replyI've had enough Internet for one lifetime.
replyAs long as we also get low order polynomial solutions to important problems, it'll be worth it.
Besides, unencrypted wifi was funny.
Even if P=NP it doesn't mean that the P approach will be better than the heuristic approach we already do today.
replyOf course, if we get ridiculous polynomials it doesn't mean much in practice. People who hope for P=NP generally hope for nice polynomials O(n^3) or something like that at worst.
reply