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?