There are two ways to look at the P v NP problem, as a formal mathematically defined conjecture as a Clay Millennium Prize Problem, and as the more intuitive notion that everything efficiently verifiable is efficiently computable and the implications that has on our ability to compute.
I've written considerably about how artificial intelligence has affected the latter. In particular, how AI and other advances in computing have brought us to this Optiland of getting most of the good implications of P=NP while our cryptographic codes remain unbreakable.
But now with the recent advances in AI-created and assisted proofs, will AI change what we know about the formal mathematical statement? Is an AI-generated proof of P ≠ NP around the corner?
No, it isn't. I do not believe we will see a P v NP proof in my lifetime proven by man or machine, separately or working together.
While the disproof of the Erdős unit distance problem is an impressive AI achievement, keep in mind that for every AI math proof there are hundreds of problems that we have tried to solve with AI where we haven't seen progress. And there is a huge chasm between Erdős combinatorial conjectures and the Clay Millennium problems. AI will continue to improve, but there are limits.
People, particularly those outside of computational complexity, don't realize how difficult a mathematical challenge this is. Polynomial-time algorithms can work in strange and mysterious ways. They don't have to respect the semantics of an NP-search problem or do any searching at all. Bill gave me the following "algorithm" for clique: Take the eigenvalues of the adjacency matrix. For all we know, if there are two primes p and q such that the pth eigenvalue and the qth eigenvalue differ by more than 1/k then the graph has a k-clique. Of course this doesn't work. But to prove P ≠ NP, you need to prove not only that this algorithm doesn't work, but neither do any of the infinitely other potential algorithms for solving NP-complete problems.
We simply know of no way to manage general polynomial-time algorithms other than by simulating them. We know by relativization that simulation and diagonalization will not work to settle P v NP. Other attempts to understand polynomial time, like circuit complexity, proof complexity and algebraic geometry have gotten bogged down well below the full power of polynomial-time. At this time we don't even have a viable approach to settling the P v NP problem.
Don't waste your time trying a formal approach via Lean. (I'm looking at you Dmitry Khanukov) Computational complexity is very messy to formulate technically. I can't get an AI willing to give me a full Lean-verified proof of something trivial like P closed under complement, forget the PCP theorem. If someone or something does come up with a P ≠ NP, it'll be following the right intuitive approach, not a formalistic one.
At least start with something simpler, like showing BPP is in subexponential time, or SAT doesn't have quadratic algorithms. You won't succeed there either, even though these questions should be galactically simpler than P ≠ NP.
The lack of "mathematical structure" in a lot of computational complexity + lack of copious amounts of results is a deadly combination for any (even heuristic) proof search techniques to get good. On the other hand, designing algorithm .... maybe?
ReplyDeleteYou commented that complexity theory is messy to formulate. If I were to formalize it, I'd go with the Bellantoni & Cook characterization of P. Do you know in what mess I'd be getting into?
ReplyDeleteThere are a lot of pieces there so it will be more tedious than you getting into trouble. Still, it will be tricky to even completely formulate P closed under complement.
Deletemy favorite way of formalizing P is through Circuit Value Problem, which is not too bad, and then defining the AC0 closure over it. Proving the closure under complement becomes also relatively easy.
ReplyDeleteThe tricky part in formalizing is that often proving the equivalence of two different formulations is often non-trivial.
TM formulation, you can use the computation history as a strong, plus functions and predicates for working with strings. It is not too bad, for closure, given machine M, you can manipulate M to M' which would have the same valid computation history as the original, except the last state now not being the accepting state.
The main difficulty often is building the machinery required to do the intuitive manipulation of objects, that was also the technical part of Godel's theorem, but once you overcome that, the rest of formalizing is not too difficult.
Your point is valid though, compared to many other areas of math, formalizing complexity theory is quite more challenging.
I was hoping you would say because AI will solve all easy problems, more humans can focus on the more difficult problems like P vs NP but alas.
ReplyDeleteWe have so many very very hard problems in complexity that no one, even the sooner of the smartest people in the world have been able to make much progress on them. If Sasha and Russell and ... have not been able to make progress on a problem they have worked for over a year, I would be really impressed if an AI was able to make meaningful progress on them. I mean an unconditional super-poly NC^1 lower bound for an NP problem would be really impressive. Or even for TC^0. It is maddening that for almost 40 years we have not been able to solve these despite some of the smartest people in the field spending considerable amount of time thinking about them.
I agree that a proof is not around the corner for P ≠ NP but I don't agree with your arguments about the obstacles. It is true that complexity theory hasn't been formalized yet, but I see no reason why it should be particularly hard to formalize it. Arguing that proving P ≠ NP needs to consider every possible algorithm feels certainly scary, but in decision tree complexity and communication complexity we have managed to beat them all, not to mention that the Cook-Levin theorem also reduces all NP-problems to SAT in one stroke. And don't forget that maybe P = NP after all.
ReplyDeleteIndependently of AI, aren't people working on formalizing computational complexity stuff in Lean?
ReplyDeleteYes
DeleteRegarding Dmitry Khanukov's post: That sounds incredibly uninformed on the surface ("I just need to prove a couple of lemmas and we'll be done"). But I can't read Lean fluently, and he never comments on his approach. What is his strategy for proving this? I thought in the rest of the world, we don't even have a potential strategy outline that hasn't already been refuted.
ReplyDelete"But to prove P ≠ NP, you need to prove not only that this algorithm doesn't work, but neither do any of the infinitely other potential algorithms for solving NP-complete problems." --- this is not a convincing argument. To prove that there is no algorithm for checking whether a given Turing machine halts, we need to prove that not only "this" algorithm doesn't work, but neither do any of the infinitely other potential algorithms - polynomial-time, exponential-time, or whose complexity grows really astronomically. And still there is a simple proof. For P ≠ NP, the proof is unlikely to be so simple, but the shortest proof may combine ideas from the 3-4 very different areas of math, and there may be no human who is expert in all of them. Enter AI...
ReplyDeleteTM halting := no algorithm will never ever succeed
Deletevs.
P != NP := no algorithm will succeed within poly time
the former being resource unbounded is much easier to prove.
Yup, starting with something simpler is a time-honored strategy...
ReplyDeleteIn, like, 2009, I was trying to prove circuit bounds for finding triangles ("$K_3$s") in tiny graphs. I came up with a possible proof (linked to in the post below) that finding triangles in 6-vertex graphs requires 21 unbounded fan-in NAND gates. (I say "unchecked"; but it's a weak enough statement that I think the proof is possibly correct.)
Bill posted about this; he titled the post: Are results about actual constants interesting?. (I think that's debatable; I definitely think bounds for graphs of any size are more interesting, than bounds for tiny graphs.)
On that thread, someone mentioned Ryan William's paper Applying Practice to Theory.
That paper argued for using automated tools to find minimal circuits for various problems (such as SAT and matrix multiplication). The tools available then (around 2008) were things like sKizzo, a solver for quantified Boolean formulas.
In a similar vein, now that AIs can find checked proofs (in a language like Lean), possibly it makes sense to formalize a question like "Finding 4-vertex cliques in 8-input graphs requires ___ gates"?
It's arguably not that interesting a question. But, if you can just burn tokens to get such bounds, and whatever bounds you get are machine-checked, maybe it's slightly more worth trying? (I would do this myself. However, I'm not fluent in Lean, and so I don't know how hard this would be to do.)