Keith Devlin writes about MOOCs, or “massive open online courses”, such as those offered by udacity and coursera1. In particular he’s going to be offering a five-week “math transitions” course in October, via Coursera. Devlin writes:
Such courses typically comprise a mix of some elementary mathematical logic, proof techniques, some set theory through to an analysis of relations and functions, with a bit of elementary number theory and introductory real analysis thrown in to provide examples.
I’m a bit skeptical about this, because the coursera platform involves automated grading. This is fine for courses where problems have numerical answers, or for courses where the assignments are to program and whether a program works can be validated by an automated system. But the transition course is in some way the course where students learn how to prove things; I almost want to say it’s fundamentally a writing course. This is a problem that one runs into even when teaching in-person courses, if the course is large enough that the grading is outsourced to an inexperienced graduate student or even an undergraduate, as is common in some places; sometimes the grader is simply not experienced enough to give really high-quality feedback. Of course in many situations the grader could give such feedback but doesn’t have time to do so, which is really a different issue. But it seems like it will only be worse in the online format. I’m sure Devlin is aware of this, though, and I’ll be interested to see what he and his TAs do.
1. why is udacity a .com and coursera a .org? In both cases it looks like the company registered the “other” domain at the same time, so it’s not a question of availability of domains.
God plays dice 
Coursera has a system called DeduceIt (used in the compiler course) which works a bit like an automatic solver but done manually. That is, you start with some assumption then each line of reasonning has three parts: the input, the theorem/rule you apply to it, selected from a list, and the result you expect. You can add as many lines as you want and each line is automatically validated: given the input and the theorem, a computer can check whether the result is correct.
I haven’t used it yet, just watched the demo. It seems reasonnably easy to use for short proofs.