This is really more of an extended comment than an answer, but I couldn't resist.
First of all, I don't know of any proof assistant that would be helpful in an "introduction to proofs" class. I would guess that no such proof assistant exists.
However, I agree that such an assistant would have the potential to be very helpful. My experience with teaching introductory proofs is that students use the following algorithm to write proofs:
Write an incorrect proof.
Turn it in, unaware of the problem
Find out later that it was wrong.
If I plead with the students enough to attend my office hours, this algorithm can be improved to:
Write an incorrect proof.
Show it to me. I point out that's its wrong.
Write a slightly better proof.
Show it to me. I point out that it's better but still wrong.
Write a correct proof.
Show it to me. I verify it.
Turn it in.
This second algorithm is of course much better, since the students actually learn to write proofs! (I cannot stress enough how important office hours are for an introductory proofs class.) Unfortunately, it's hard to have enough office hours to help all of the students through this process. What they need is an automated assistant that can check their proofs. This should be possible to program --- if there's one thing a computer ought to be able to understand, it's a proof.
To illustrate, here is a little snippet of I/O depicting a student interacting with a machine using this hypothetical program.
>>> import BasicNumberTheory
>>> begin theorem1
>> suppose m is even
Error: Variable 'm' not recognized!
>> let m be an integer
>> suppose m is even
>> let n be an integer
>> suppose n is even
>> then m+n is even
>> end theorem
>>> print theorem1
Let m be an integer.
Let n be an integer.
Suppose m is even.
Suppose n is even.
Then m+n is even.
>>> prove theorem1
1: m is an integer
2: n is an integer
3: m is even
4: n is even
>> By (3), m = 2j
Error: Variable 'j' is not recognized.
>> By (3), there exists an integer j so that m = 2j
5: There exists an integer j so that m = 2j
>> Let j be such
6: j is an integer
7: m = 2j
>> By (4), there exists an integer k so that n = 2k
8: There exists an integer k so that m = 2k
>> Let k be such
9: k is an integer
10: n = 2k
>> By (7) and (10), m + n = 2j + 2k
11: m + n = 2j + 2k
>> So m+n is even
Error: How does this follow?
>> So m+n = 2(j+k)
12: m+n = 2(j+k)
>> So m+n is even.
Error: Missing hypothesis -- is it true that j+k is an integer?
>> By (6) and (9), j+k is an integer
13: j+k is an integer
>> So m+n is even
Proof accepted: theorem1
>>> save theorem1
I think the idea is that students would only be required to use the software for the first month or so, but I would encourage them to use it throughout the semester to check their reasoning. I'm not absolutely convinced that this would work well, but I'd love to try it!