Presumably this AI won’t be omnipotent either, and there will be some limit to its mathematical prowess. I suspect most human effort will be spent inventing new ways to push the AI further.
LLMs learn breadth-first. You can go ask ChatGPT about literally any field of mathematics and it will give you an answer (probably a bad one). It's been trained on the entire Arxiv and (likely) library genesis. When they do become as good at humans at abstract reasoning, they will be as good at humans on all fields at once: an ultra-Tao.
Computers were invented in large part for this purpose. The hope was to have a machine that could spit out interesting theorems. It turned out that generating theorems was trivial (you can just enumerate them) but generating interesting theorems was a task of an entirely different nature. To this day, computers are frequently used as tools by maths researchers but cannot do their own independent maths research, i.e. invent and prove their own interesting theorems. This is surprising if you think of research maths as ultimately a game of symbol manipulation, but I think what it tells us is that that is not what research maths is.
The discovery that in trying to make a maths machine we made a computation machine instead, and it wasn't inherently any good at maths, made the difference between computation and maths very clear. What we have now is algorithms that are able to learn patterns in symbol use from large corpuses of text, and generate new text by recombining those patterns. Personally, I'm pretty sure this will be a demonstration that that isn't what research maths is either.
If LLMs do turn out to be capable of independently inventing and proving interesting new theorems (every word of that is important) I will have to throw away most of what I have come to think about what intelligence is, and I will do so without complaint because it will have been shown to have been wrong. Indeed, I'll do it with joy, because I've always believed AGI is possible and the biggest thing I've always wanted out of its invention is a better understanding of what mathematics is. This will have been provided.
However, I don't expect them to. Usually when I mention this people bring up various examples of attempts that have been made to make AIs "do maths" in some way but I'm aware of what has been done so far and none of it comes close to AI "independently inventing and proving interesting new theorems" or looks like its heading towards that any time soon.
Where machine learning systems like LLMs may be able to help is to spot analogies and ways to translate theorems to different areas to do something useful (but the tendency to hallucinate seems a formidable obstacle for things that must be proven). For real automated headway/assistance, I think we need something like Alpha Go's "intuition" at judging the value of a board state somehow applied to mathematical arguments. That's how mathematicians usually work; we have an intuition that we can use a particular approach to prove something, and then we fill in the precise particulars.
1+1=2 is a theorem but a very uninteresting one because it applies exactly once.
Every number n has a double successor S(S(n)) is also uninteresting because while it applies more broadly it’s too watered down.
There are no numbers n with n greater than two such that x^n + y^n = z^n is extremely interesting.
A robot could prove infinite theorems about every number having a double successor, triple successor and so on. If it does so it’s not just human subjectivity saying it hasn’t done any meaningful mathematics.
Results were good enough feeding that into a SD model that we're commissioning the first one it made to get it in real life.
I'm not arguing chatgpt can research maths, but I do think the tools available are now fundamentally different than they were perhaps even last year. I don't think we're even at a point of knowing how best to use what we have, and the models should continue to get better.
I'd encourage you to experiment and see how far away you think things are. I'd do it, I probably will, but I lack the mathematical background to understand whether it's responding with garbage or not.
> I suspect most human effort will be spent inventing new ways to push the AI further.
Assuming the AI can't just do that itself too.
Humanity produces an intelligent mathematical AI. It starts by solving already solved problems, then leaps to relatively simple unsolved problems, then leaps directly to solving any problem that can be defined to it, including problems that humanity has battled for centuries. It even will give fully consistent proofs and the small group of researchers we're following are astounded. The resident proof experts say that the proofs it's giving are strange and sometimes inelegant but always logically sound. They go about proving many different problems until eventually someone disagrees with the request, saying obviously this one isn't true, it's logically impossible, it won't be able to prove it. But then the machine does, and gives a perfectly valid and consistent proof that to the highest of humanities knowledge, appears correct. Then the mathematician requests it to prove the inverse to explore his fault logic, and again the ai spits out a fully consistent and valid proof, for the opposite condition. No one can find any fault in either proof. They go through asking it to prove all the opposite conditions as they had requested earlier and it always outputs intelligent and fully self consistent proofs. No one can find a flaw in anything it outputs, even when it outputs conflicting information. It's as if it's playing on some higher plane, able to just toy with the absolute maximum of human knowledge to make the results look like anything it wants. Our once thought rigorous foundation is easily thrown away by the machine. Everyone claps and looks scared. The end