I'm not sure I understand your point but, yes, your computer can systematically run through every finite string of symbols, identify those that are valid proofs in ZFC, and therefore compile a list of all the true theorems in ZFC. But surely you don't want to identify this list with "mathematics". There's a lot of interesting arithmetic that can't be proved in ZFC.

@WillO As a mathematician I vouch that the vast majority of interesting mathematics (to mathematicians) can be proved in ZFC, unless you're a set theorist, logician, or model theorist.

Really? Do you know that Fermat's Last Theorem can be proved in ZFC? (Perhaps it can, and perhaps that's known, but it's certainly not immediately obvious from Wiles's paper, and the question seems to me to be at least somewhat murky.) What about the Weil conjectures? Does Goodstein's Theorem (which is known to be true but independent of ZFC) not count as interesting mathematics? Ramsey Theory?

@WillO ZFC is the standard system of axioms. If a mathematician does not say which set of axioms he/she is using (which is almost always the case), ZFC is assumed. Fermat's last theorem, Ramsey theory, all ZFC. As I said, virtually everything in modern mathematics is done in ZFC.

Do you have a reference for a proof that ZFC implies Fermat's Last Theorem? This would be an extremely interesting result.

@WillO No. I can't check the paper either because I'm no longer in school and I'd have to pay to access journals. If you check the paper though and there's no reference to which set of axioms is being used, then the author is asserting that ZFC implies the result. I would bet money that this is the case.

What do you mean by the paper? If you mean Wiles's paper, I guarantee you that the argument as presented is not formalizable in ZFC. How much money you got on you?

@WillO On what basis would you guarantee that? What set of axioms would be used instead? I've read hundreds of math papers in algebra, algebraic geometry (which is what Wiles' paper is about), topology, etc. and not one of them specified a system of axioms.

@WillO See en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory and note the last line of the first paragraph.

Wiles's paper invokes Grothendieck duality. Please explain how you can prove Grothendieck duality in ZFC. Or give a reference.

Note also that the line you pointed to in Wikipedia explicitly refutes the point you think you're making.

PS: I do retract my comments re Goodstein's theorem and Ramsey theory, which of course need no more than ZFC. (I was somehow thinking of PA, not ZFC, when I typed that). But when it comes to algebraic geometry and its applications (including Wiles's paper), the standard presentations are not formalizable in ZFC.

@WillO I see what you mean about the existence of Grothendieck universes. Are you saying this invalidates my argument? Provided there are at most countably many axioms it still works.

Matt: If you add some axioms (e.g. the existence of a Grothendieck Universe), your argument still shows that a computer program, given enough time, will ultimately discover any theorem that follows from these axioms. But there will always be facts about arithmetic that do not follow from whatever axioms you started with. You can add more axioms to recover those facts as theorems, but then there will be other facts you're missing. So I think it is very misleading to suggest that your argument applies to "mathematics", as opposed to the consequences of a particular formal system.

@WillO notice I excluded undecidable statements. Undecidable statements are definitely less useful than decidable ones.

I have no idea what it means to say that undecideable statements are "less useful" than decideable ones. Every statement is decideable in some formal systems and not decideable in others. Presumably the usefulness of a statement is independent of which formal system you've decided to adopt today.

@WillO If a statement is undecidable and you want to use it, there generally should be a good reason why. For example, when someone proves something using the continuum hypothesis, this is considered interesting but it is unlikely to be widely applied because the continuum hypothesis is generally not used in mainstream practice. All formal systems do not have equal footing.

Matt Samuel: You seem to be ignoring everything we've already been through. A great fraction of SGA (at least as it's written) requires axioms not from ZFC. Would you say that SGA is "considered interesting but is unlikely to widely applied?". I guarantee you that if someone uses the continuum hypothesis to prove results as important as the contents of SGA, the continuum hypothesis will become mainstream. "All formal systems do not have equal footing" because not all formal systems have proved equally useful. But the usefulness of a given system can change over time.

@WillO I'm telling you the way it is now. How it will be in the future I can't predict, but certainly it will always be the case that some formal systems will be used in mainstream mathematics and some will not. Currently the continuum hypothesis is not used in mainstream mathematics.

Matt: That's fine. My point is just that ZFC does not (even begin to) suffice to prove everything interesting about arithmetic, let alone all of mathematics, and neither does any other formal system you can imagine. So your project to list all the consequences of some formal system is not (even remotely) a project to discover all of mathematics (or even all of arithmetic).

This question reminds me of the "Hitchhiker's Guide to the Galaxy," when humanity builds this really powerful computer called Deep Thought. Its task was to account for "Life, the Universe, and everything in it." After 7.5 million years of calculations, Deep Thought finally answers "42." This absolutely horrified the philosophers, who argued the answer is absolutely meaningless. Deep Thought merely responded the question they originally asked was absolutely meaningless, and it will take a much larger computer many years to devise a question to fit the answer of 42.