So here's what I'm perplexed about. There are statements in Presburger arithmetic that take time doubly exponential (or worse) in the size of the statement to reach via any path of the formal system whatsoever. These are arithmetic truths about the natural numbers. Can these statements be reached faster in ZFC? Possibly—it's well-known that there exist shorter proofs of true statements in more powerful consistent systems.
But the problem then is that one can suppose there are also true short statements in ZFC which likewise require doubly exponential time to reach via any path. Presburger Arithmetic is decidable whereas ZFC is not, so these statements would require the additional axioms of ZFC for shorter proofs, but I think it's safe to assume such statements exist.
Now let's suppose an AI model can resolve the truth of these short statements quickly. That means one of three things:
1) The AI model can discover doubly exponential length proof paths within the framework of ZFC.
2) There are certain short statements in the formal language of ZFC that the AI model cannot discover the truth of.
3) The AI model operates outside of ZFC to find the truth of statements in the framework of some other, potentially unknown formal system (and for arithmetical statements, the system must necessarily be sound).
How likely are each of these outcomes?
1) is not possible within any coherent, human-scale timeframe.
2) IMO is the most likely outcome, but then this means there are some really interesting things in mathematics that AI cannot discover. Perhaps the same set of things that humans find interesting. Once we have exhausted the theorems with short proofs in ZFC, there will still be an infinite number of short and interesting statements that we cannot resolve.
3) This would be the most bizarre outcome of all. If AI operates in a consistent way outside the framework of ZFC, then that would be equivalent to solving the halting problem for certain (infinite) sets of Turing machine configurations that ZFC cannot solve. That in itself itself isn't too strange (e.g., it might turn out that ZFC lacks an axiom necessary to prove something as simple as the Collatz conjecture), but what would be strange is that it could find these new formal systems efficiently. In other words, it would have discovered an algorithmic way to procure new axioms that lead to efficient proofs of true arithmetic statements. One could also view that as an efficient algorithm for computing BB(n), which obviously we think isn't possible. See Levin's papers on the feasibility of extending PA in a way that leads to quickly discovering more of the halting sequence.
ZFC is way worse than Presburger arithmetic -- since it is undecidable, we know that the length of the minimal proof of a statement cannot be bounded by a computable function of the length of the statement.
This has little to do with the usefulness of LLMs for research-level mathematics though. I do not think that anyone is hoping to get a decision procedure out of it, but rather something that would imitate human reasoning, which is heavily based on analogies ("we want to solve this problem, which shares some similarities with that other solved problem, can we apply the same proof strategy? if not, can we generalise the strategy so that it becomes applicable?").
> and for arithmetical statements, the system must necessarily be sound
Why do you say this? The AI doesn't know or care about soundness. Probably it has mathematical intuition that makes unsound assumptions, like human mathematicians do.
> How likely are each of these outcomes?
I think they'll all be true to a certain extent, just as they are for human mathematicians. There will probably be certain classes of extremely long proofs that the AI has no trouble discovering (because they have some kind of structure, just not structure that can be expressed in ZFC), certain truths that the AI makes an intuitive leap to despite not being able to prove them in ZFC (just as human mathematicians do), and certain short statements that the AI cannot prove one way or another (like Goldbach or twin primes or what have you, again, just as human mathematicians can't).
2 is definitely true. 3 is much more interesting and likely true but even saying it takes us into deep philosophical waters.
If every true theorem had a proof in a computationally bounded length the halting problem would be solvable. So the AI can't find some of those proofs.
The reason I say 3 is deep is that ultimately our foundational reasons to assume ZFC+the bits we need for logic come from philosohical groundings and not everyone accepts the same ones. Ultrafinitists and large cardinal theorists are both kinds of people I've met.
My understanding is that no model-dependent theorem of ZFC or its extensions (e.g., ZFC+CH, ZFC+¬CH) provides any insight into the behavior of Turing machines. If our goal is to invent an algorithm that finds better algorithms, then the philosophical angle is irrelevant. For computational purposes, we would only care about new axioms independent of ZFC if they allow us to prove additional Turing machine configurations as non-halting.
> There are statements in Presburger arithmetic that take time doubly exponential (or worse) in the size of the statement to reach via any path of the formal system whatsoever.
This is a correct statement about the worst case runtime. What is interesting for practical applications is whether such statements are among those that you are practically interested in.
I would certainly think so. The statements mathematicians seem to be interested in tend to be at a "higher level" than simple but true statements like 2+3=5. And they necessarily have a short description in the formal language of ZFC, otherwise we couldn't write them down (e.g., Fermat's last theorem).
If the truth of these higher level statements instantly unlocks many other truths, then it makes sense to think of them in the same way that knowing BB(5) allows one to instantly classify any Turing machine configuration on the computation graph of all n ≤ 5 state Turing machines (on empty tape input) as halting/non-halting.
But the problem then is that one can suppose there are also true short statements in ZFC which likewise require doubly exponential time to reach via any path. Presburger Arithmetic is decidable whereas ZFC is not, so these statements would require the additional axioms of ZFC for shorter proofs, but I think it's safe to assume such statements exist.
Now let's suppose an AI model can resolve the truth of these short statements quickly. That means one of three things:
1) The AI model can discover doubly exponential length proof paths within the framework of ZFC.
2) There are certain short statements in the formal language of ZFC that the AI model cannot discover the truth of.
3) The AI model operates outside of ZFC to find the truth of statements in the framework of some other, potentially unknown formal system (and for arithmetical statements, the system must necessarily be sound).
How likely are each of these outcomes?
1) is not possible within any coherent, human-scale timeframe.
2) IMO is the most likely outcome, but then this means there are some really interesting things in mathematics that AI cannot discover. Perhaps the same set of things that humans find interesting. Once we have exhausted the theorems with short proofs in ZFC, there will still be an infinite number of short and interesting statements that we cannot resolve.
3) This would be the most bizarre outcome of all. If AI operates in a consistent way outside the framework of ZFC, then that would be equivalent to solving the halting problem for certain (infinite) sets of Turing machine configurations that ZFC cannot solve. That in itself itself isn't too strange (e.g., it might turn out that ZFC lacks an axiom necessary to prove something as simple as the Collatz conjecture), but what would be strange is that it could find these new formal systems efficiently. In other words, it would have discovered an algorithmic way to procure new axioms that lead to efficient proofs of true arithmetic statements. One could also view that as an efficient algorithm for computing BB(n), which obviously we think isn't possible. See Levin's papers on the feasibility of extending PA in a way that leads to quickly discovering more of the halting sequence.