In previous cases of automating mathematical activities, we’ve usually known very explicitly exactly what we were doing: computing trig tables, enumerating and checking graphs for the 4-colour map theorem, etc. This makes it relatively easy to understand the time and memory resources required, and how far they can be scaled up before hitting computational complexity limits.
It’s much less clear what LLMs are doing when arriving at these kinds of proofs, but it would be helpful if the people building and studying LLMs could make it equally transparent.
My guess is that the “algorithm” being effectively performed here (though of course not explicitly programmed as such) is something roughly along the lines of:
• extract a set P of relevant / related proofs from the literature
• break P down into a set of suitably fine-grained steps, S
• iterate through subsets of S looking for any collection of steps that will solve the problem
It’s impressive that it’s possible to automate these three things at all, even as imperfectly as LLMs do them, but if this description is more or less correct then it will eventually hit the same kind of scaling issues as any other combinatorial approach.
It might be possible to make this kind of smart-brute-force search more smart and less brutish in the manner of Alpha Go etc., but strategically pruning the decision trees for assembling valid proofs is likely to be much tougher than it was for Go.
