AlphaProof's Greatest Hits

If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.

No one is focused on those. They're much more focused on more rote problems.

You might find them used to accelerate research math by helping them with lemmas and checking for errors, and formalizing proofs. That seems realistic in the next couple of years.

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.

The hard part is in the creation of new math to solve these problems not in the use of existing mathematics. So new objects (groups rings fields) etc have to be theorized, their properties understood, and then that new machinery used to crack the existing problems. I think we will get to a place (around 5 years) where AI will be able to solve these problems and create these new objects. I don’t think it’s one of technology I think it’s more financial. Meaning, there isn’t much money to be made doing this (try and justify it for yourself) and so the lack of focus here. I think this is a red herring and there is a gold mine in there some where but it will likely take someone with a lot of cash to fund it out of passion (Vlad Tenev / Harmonic, or Zuck and Meta AI, or the Google / AlphaProof guys) but in the big tech world, they are just a minnow project in a sea of competing initiatives. And so that leaves us at the mercy of open research, which if it is a compute bound problem, is one that may take 10-20 years to crack. I hope I see a solution to RH in my lifetime (and in language that I can understand)

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?

I understand that a group of motivated individuals, even without significant financial resources, could attempt to tackle these challenges, much like the way free and open-source software (FOSS) is developed. The key ingredients would be motivation and intelligence, as well as a shared passion for advancing mathematics and solving foundational problems.

There are some AI guys like Christian Szegedy who predict that AI will be a "superhuman mathematician," solving problems like the Riemann hypothesis, by the end of 2026. I don't take it very seriously, but that kind of prognostication is definitely out there.

Ok but how do you get around needing a 10k or 100k h100 cluster

It is well known that cloud services like Google Cloud subsidizes some projects and we don't even know if in a few years improvements will arise.

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.

I’m sure AI can “solve” the Riemann hypothesis already, since a human proved it and the proof is probably in its training data.

No, nobody has proved it.

Side point, there is no existing AI which can prove - for example - the Poincaré conjecture, even though that has already been proved. The details of the proof are far too dense for any present chatbot like ChatGPT to handle, and nothing like AlphaProof is able either since the scope of the proof is well out of the reach of Lean or any other formal theorem proving environment.

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

Possible but unlikely given how much demand there is and the pressure to deliver returns to shareholders, however sure it is possible. Right now search is very inefficient, the search space is massive. That is the main problem. You can have many sequences of text that sound plausible, but of them a much smaller number will be logically valid. This is the main challenge. Once we can search efficiently not just in semantically valid space but I suppose what you can call syntactically valid space then we will be able to crack this.

I think there's significant financial incentives for big tech given the scarcity of benchmarks for intelligence which are not saturated

link to this prediction? The famous old prediction of Szegedy was IMO gold by 2026 and that one is basically confirmed right? I think 2027/2028 personally is a breakeven bet for superhuman mathematician.

what does this even mean? Surely an existing AI could reguritate all of Perelman's arxiv papers if we trained them to do that. Are you trying to make a case that the AI doesn't understand the proof it's giving? Because then I think there's no clear goal-line.

You don't even need AI to regurgitate Perelman's papers, you can do that in three lines of python.

What I meant is that there's no AI you can ask to explain the details of Perelman's proof. For example, if there's a lemma or a delicate point in a proof that you don't understand, you can't ask an AI to clarify it.

I consider it unconfirmed until it happens! No idea where I saw it but it was probably on twitter.

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".

> I think we will get to a place (around 5 years) where AI will be able to solve these problems and create these new objects.

For all we know, buried deep in AlphaProof's attempts to solve these toy problems, it already tried and discarded several new ideas.