That's the loophole. There is mathematics without infinity.[1] Until recently, it was considered somewhat fringe. But there's been enough development that it's now clear you can do mathematics without infinity. In that view, infinities are a labor-saving device to get rid of special cases. They're not essential. Mathematicians used to hate special cases, but now that the active ones all grew up with computers, they're not so scared of IF statements.
You can have "arbitrarily large" but not "infinite". Boyer-Moore theory is like that. It starts out like Peano arithmetic. There is (ZERO) and (ADD1 (ZERO)) and (EQUALP A B) and (LESSP A B) as predicates. That's the axiomatic basis. Numbers are (ADD1 (ADD1 (ADD1 (ZERO)))), etc.
You can have recursive functions, but they must terminate. They must have a value which, for each recursion, is LESSP than the previous iteration. That's how you prove termination.
You can do most of mathematics that way. But not infinitesimals. You never can get to
1 + 1/2 + 1/4 + 1/8 ... = 2
in that kind of constructive mathematics. That requires an infinite recursion, which is not allowed.[1] https://engtechnica.com/rethinking-mathematics-without-infin...
Note that the article itself is not as careful as you are here about correctly stating what Godel's Incompleteness Theorem actually says. The article states it this way: "any set of rules powerful enough to handle basic arithmetic will contain true statements it cannot prove". But that's wrong, because, when you take into account Godel's Completeness Theorem, you realize that, for any formal system complex enough for the proof of Godel's Incompleteness Theorem to go through, there must be a semantic model of that system in which the Godel sentence for that system is false! The article's misstatement is unfortunately very common, but it's still a misstatement.
"One!" "Two!" "Three!" "Infinity!" "Infinity plus one!" "Infinity plus two!" "Infinity plus infinity!" "Infinity times infinity!" "Infinity to the power of infinity!" "Infinity to the power of infinity to the power of infinity!" "The supremum of all ordinals that can be expressed in a finite sequence of symbols!" "The supremum of all ordinals that can be expressed in a finite sequence of symbols plus one!"
There’s a sense in which the set of natural numbers is too big to be practically useful, but no smaller set makes sense when writing proofs. The set of numbers you can reach without using induction (say, by using a computer to check) isn’t well-defined.
And that has nothing to do with AI’s limitations.
The Church-Turing thesis throws cold water on this: since the human body (including brain) is describable by a finite system of Schrödinger equations, and these equations can be solved numerically by a Turing machine, the human process of creating an axiom scheme should be Turing-computable. But some recent results on very large finite numbers (busy beaver) suggest there may be a subtlety here, e.g. complexity blows up to the point that it takes far more energy than the sun to simulate one human.
The more interesting subtlety: for a physically meaningful result you would need to define configuration space very carefully, e.g. not screwing up the boundary consitions or causal order of subsystems. Perhaps defining this is actually not computable, and after every delta(t) in a computer simulation, a human has to check the physics and redefine certain parameters of the system. Solving the Schrodinger equation numerically is certainly Turing-computable, but the process of ensuring that solution is physically meaningful isn't even slightly formalized. It may be unformalizable.