ColinsMum, Thanks for all the sources of problems. That's very useful. We really haven't tried this, but we need to. DS7 does edutain himself with lots of maths stuff on the internet, but he hasn't really been exposed to a lot of challenging problems.
As for "mathematical maturity", I guess your right that it's okay to have some false starts when they're way ahead anyway, although I wouldn't want a false start to happen in his school courses. If a competition or AoPS course doesn't work out, it's not the end of the world. Better to try, as long as it's not so traumatic that it instills fear in trying very difficult things (aka "perfectionism").
[ETA and to answer the later question about eIMACS, I thought this course was OK, but not great. Understandably, not many of the exercises were automatically graded, so he definitely needed someone there to check he was understanding; well, there are answers available, but since other correct answers are possible, that's of limited use. Pedagogically it was not bad, but there was a fair bit of "in the AP exam you can expect" to be ignored.]
FWIW I think software can be pretty sophisticated at recognizing equivalent answers.
Another question, anyone know of a good resource (especially online) for learning very basic logic (and, or, not, quantifiers) and the same for set theory. These topics are totally absent from the school curriculum, so this void needs to be filled.
As kcab said,
Language Proof and Logic - for the software (more than just Tarski's World here, though that's good), more than for the book, which obviously isn't written to be appealing to children and isn't particularly so to DS. And this other resource that I can't point you at yet!
Is the software appealing to 7yo children. I'm looking for the most extremely elementary parts of set theory and logic (and maybe graph theory) just to be aware that these topics exist at all, because they're just not in his courses at all.
