AlphaProof's Greatest Hits

Probably a bad example, P vs NP is the most likely of the millennium problems to be unsolvable, so the answer may be "never".

I'll bet the most technical open problems will be the ones to fall first. What AIs lack in creativity they make up for in ability to absorb a large quantity of technical concepts.

Thank you for the response. I have a follow-up question: Could these AIs contribute to advancements in resolving the P vs NP problem? I recall that the solution to Fermat’s Last Theorem relied on significant progress in elliptic curves. Could we now say that these AI systems might play a similar role in advancing our understanding of P vs NP?

Just my guess as a mathematician. But if LLMs are good for anything it will be for finding surprising connections and applying our existing tools in ways beyond human search. There's a huge space of tools and problems, and human intuition and brute force searching can only go so far. I can imagine that LLMs might start to find combinatorial proofs of topological theorems, maybe even novel theorems. Or vice versa. But I find it difficult to imagine them inventing new tools and objects that are really useful.

Do you have a past example where this already-proven theorem/new tools/objects would have been only possible by human but not AI? Any such example would make your arguments much more approachable by non-mathematicians.

Ok, then the AI should formally prove that it's "unsolvable" (however you meant it).

Unsolvable would mean that no proof exists, and no disproof exists, in whatever axiom system (eg ZF). While in some cases you can hack around this by proving eg "no proof and no disproof exist in ZF, if ZF is consistent", IIUC that's not always possible. It's like asking "when will AI be strong enough that it can always decide correctly whether a given computer program halts?"

Then again, it's fairly likely that P=?NP is decidable but we just don't have any idea how to prove it. In that case the question is more or less "what's the time horizon until AI is vastly better than humans at formal math?", to which the answer is certainly "we don't know, there may be obstacles, just wait and see".