Wednesday, November 04, 2026

Another Step Towards Optiland

When the Clay Mathematics Institute announced the Millennium Prize Problems back in 2000, we joked that if you proved P = NP, you wouldn't only get the $1 million prize for solving P v NP, but you would get $7 million since you could use P = NP to solve the rest.

In theory, if P = NP, then you could efficiently find the proof of any theorem, provided its formal proof was not too long. In practice, we don't have P = NP, and back then we didn't even have a good way to formalize a proof. Fast forward to today and we have a computer generated formalized proof of Navier-Stokes and a number of other important problems.

In my 2022 CACM article, I argued that we were heading towards Optiland, where we got all of the goodies of P = NP, without losing cryptography. But some challenges remained.
Machine learning seems to fail learning simple arithmetic—for example, summing up a large collection of numbers or multiplying large numbers. One could imagine combining machine learning with symbolic mathematical tools. While we’ve seen some impressive advances in theorem provers, we sit a long way from my dream task of taking one of my research papers, with its informal proofs, and having an AI system fill in the details and verify the proof.

I failed to imagine that in less than five years AI models would not just fill in the details of my proofs but find the proofs themselves.

Still plenty of math problems that AI hasn't solved, including P v NP itself. I've given up predicting what AI will prove next, though I still believe P v NP requires new techniques that AI won't come up with on its own.

I watch discussions on whether we could find some version of the ETH-refutation algorithm that would help solve SAT problems in practice. Spoiler alert: It will never beat CDCL.

We are running out of examples of real-world problems we still need P = NP to tackle. Outside of breaking codes, what could you do with P = NP that you couldn't do today using other means?

7 comments:

  1. Perhaps another viewpoint: ETH refutation result is really a counting algorithm and does have some syntactic similarity with that of exiting model counters; it would be great if some of the insights can be translated to improve component caching.

    ReplyDelete
  2. One of the central goals of computational complexity theory is to characterize the intrinsic difficulty of solving computational problems. The P vs. NP question was an important first step toward this goal. Looking back, however, the distinction seems rather coarse.

    Suppose P ≠ NP, so that 3-SAT has no polynomial-time algorithm. But how difficult is 3-SAT really? Does it require quasipolynomial, subexponential, or exponential time? These possibilities represent enormous differences in computational difficulty, yet P ≠ NP does not distinguish among them.

    In this sense, P ≠ NP may substantially underestimate the difficulty of 3-SAT, while ETH may have overestimated it.

    Perhaps what we are missing is not another technical breakthrough, but a more precise hypothesis about the intrinsic complexity of computational problems.

    ReplyDelete
  3. I think you should provide an explanation of why reinforcement learning is successful without P is NP.

    ReplyDelete
  4. P vs NP is the poster child, but it doesn't mean it is the goal of complexity theory

    What we actually care about is algorithms for solving problems efficiently in practice or proving that they cannot be solved efficiently

    I don't like Lance's repeated statement that AI is solving NP-hard problems. It is not. That is the kind of hype we should avoid and is harmful.

    There is not much progress on solving combinations problems much faster than we were able to before AI. The best algorithms for many problems are the same as what they were 10 years ago.

    ML is solving problems which are of a different nature and were not even the main topic of complexity theory or algorithms.

    Most of the progress so far in ML is towards showing that they can do tasks that humans can do almost as good as top humans in those fields.

    ML being as good as humans in these cognitive tasks doesn't mean they are solving any hard complexity problems.

    I mean we already had humans doing these tasks, why would one think that they are NP-hard or intractable at all?

    We lacked the ability to have machines solve them, and now we can do it more efficiently because of computer scaling and speed.

    Is AI able to solve SAT instances much faster than CDCL algorithms and I missed that paper?

    Lance keeps repeating that AI gives us optiland. This is not a scientific attitude, but hyper misleading language.

    If we are in optiland, please give me either a fast algorithm, much better than what we had before AI, for SAT, or give me a proof that P=NP, or give me a proof that there is no proof for P=NP in lean that would fit my laptop's RAM.

    As computer scientists we should hold ourselves to a much higher standard than this kind of sloppy language.

    ReplyDelete
  5. I think it is more important to understand what is making the AI work. There is no guarantee, imho, that AI could solve the next math/tcs problem. It is important to understand what it is capable of, why, and equally important to understand what it cannot be. I believe computational complexity should consider this as a central problem. I do see important results are getting are published, but really what is the limit of threshold circuits?

    ReplyDelete
  6. "Let's jump to the year 2026 and explore this beautiful world, almost surely a fantasy world, the world of P = NP." (from "The golden ticket", 2013)

    ReplyDelete