You're rather condescending. Why do you need to to do physics to do a maths degree? There are lots of Uni's that'll accept you into such a degree without Physics. I'll list a few at the top of my head - Princeton, Harvard, Standford, UCLA, Oxford, Cambridge, Warwick, Australian National Uni, etc etc. Physics is important on a set of measure zero. Ie., why should someone interested in, say, Model theory do physics. It's ridiculous to ask that. I've got a few degrees, but in my Science my minor was in Astro. At heart, I'm a pure mathematican, that's what I'm starting my PhD on next year. But there is really very little relevance to even the physics kind of stuff I've done in pure (ie., even in PDE theory, the physics is of very little importance). Rigourous mathematics is very different from the way things are done in the physics world. This guy is actually approaching things from a good perspective - having the mathematical machinery before attacking the physics is a much better thing. The physics is relatively easy to learn, the maths is the hard part. There's nothing wrong with asking Slashdot. I mean, he could ask his supervisor, but maybe his supervisor doesn't honestly know. What's wrong with reaching out to the broader community.

Yes, he's correct in this. If you have a system which only contains integers 0 to n, then that doesn't satisfy the Peano axioms.

Infinity isn't a concept in mathematics, it is what we call an entire class of sets. If a set S cannot be put into a one-one correspondence with a finite number (a number itself is a set), then we say that S is infinite. The existence of such sets is given by the "Axiom of Infinity." This is all just a part of the formalisation of Set theory. Such a formalisation is simply a set of "beliefs." A theorem prover is simply an AI which has the axioms (or synonomously the beliefs) of set theory at it's core. What I'm trying to get at is that there is no difference in the way we produce proofs compared to a computer. Just as we can never truly realise an infinite process (because we'll be going on forever), we can formalise it, and then prove results about. The point is that a theorem prover is given knowledge that "infinity" exists, because at the core, all you have is a set of beliefs, and your proofs are simply formal derivations from those beliefs. In actual fact, the Turing machine idea of computability was really created to understand the process of mathematical proof. The fundamental difference is that Turing machines had infinite memory. But for any single program which terminates, only finite amount of tape is used. A proof, by definition, is a finite "program" - so this idea of theorem proving goes way back to the 1920's! So, given any proof, we can accommodate a finite amount of memory for that and run it to check that the proof is indeed correct. Hope this clarifies things! :)

Some answers, but first, hang on! What do you mean "what makes Arithmetic complicated ... is the inclusion of infinity?" Anyway, What Godel tells you is that if you have any system which is strong enough, ie., satisfies the Peano Axioms, then indeed, incompleteness applies. I suspect that by what you mean by "inclusion of infinity" is that collection of all natural numbers is a set? In proving this (it's been a while since I looked at the proof), you don't really need the natural numbers to be a "set", because you can construct the Godel sentence in logic. The quantification is over the natural numbers, but I think that it's okay for it to be a proper class. But don't quote me.

When checking proofs, you don't need to have computers explicitly handle infinity. The very idea of "proof" is that it takes you from the theorems you've proved so far, to the statement you're trying to prove, in a finite number of steps. Most mathematicians don't write out every line of a proof explicitly, so this is a very important purpose of proof checkers - to be able to formalise every step of the proof. There are a few things. Although the most common set of Axioms used for Mathematics (Zermelo-Frankel Axioms + Axiom of Choice or BNF if you want to do Category Theory) actually has infinitely many axioms, you can write them down as finite number of sentences in logic. So certainly, you can equip your program with that. Ie., you can give you computer "knowledge" of these axioms. Then we bootstrap. The first step would be to prove all the basic theorems of your favourite set theory. Then you keep adding results that are positively proved by the system, increasing the complexity of your genome. You can enter more and more results. In effect, your prover becomes a huge database of theorems. In most cases (which probably doesn't mimic the way the Four Colour Theorem was proven) the idea is that the mathematicians go off and produce a proof. So, you have good belief that the proof works, so what you really have is an outline. You really should be able to enter the outline of the proof into the computer, and it should be able to formalise and fill in the details, and actually verify the proof is correct. In any case, everything here happens in a finite number of steps. So there's no issue about computers being unable to handle infinity. I mean, we really can't either, otherwise, it would have been simply possible to check Fermat's Last Theorem for every n... Hope this helps!