Agree with everything you say about Godel. I'm not sure what your last line means, though. Speaking strictly in terms of axioms and derived theorems, that see

Agree with everything you say about Godel. I'm not sure what your last line means, though. Speaking strictly in terms of axioms and derived theorems, that seems fine, but in thinking of, say, Wiles' proof of Fermat's Last Theorem, which wended broadly through various branches of math, extending them or perhaps inventing them as needed, it seems incorrect to say this. I'm not sure whether you want to characterize Wiles as introducing new axioms, but he certainly wasn't simply deriving new theorems that could have been computationally enumerated. Perhaps I'm wrong; I'm not a mathematician. But my understanding of Godel, axiomatic systems, and proof engines is that what they do simply isn't comparable to, say, what Mochizuki did with the ABC Conjecture.