3 tag
| link
2 emphasized that I want experiences and research
source | link

I am thinking about teaching a university-level "introduction to proofs" class (mainly for math and CS majors) making use of a computer proof assistant like Coq. I feel like there is a lot of potential benefit here, in that the students can get immediate feedback about what works and what doesn't when interacting with the proof assistant, thereby learning about the "world of mathematics" in a similar way to how a gamer learns about the world of a video game by interacting with it. However, most existing proof assistants are not really targeted at this level, so I worry that the difficulty of learning to use them could outweigh the advantages.

What experiences and research have there been with this sort of thing?

Note that I am not asking about using a proof assistant in the teaching of a class about formal logic. I know that this has been done, and experiences and research on it is not totally irrelevant to what I'm asking, but the audience is very different from a class like I'm considering; students usually already have much more mathematical maturity, and an existing understanding of what a "proof" is, coming into a formal logic class.

Edit: For further clarification, while I'm certainly interested to hear opinions and suggestions, what I'm really asking about is, as I said, experiences and research. In other words, have you or someone else done this?

I am thinking about teaching a university-level "introduction to proofs" class (mainly for math and CS majors) making use of a computer proof assistant like Coq. I feel like there is a lot of potential benefit here, in that the students can get immediate feedback about what works and what doesn't when interacting with the proof assistant, thereby learning about the "world of mathematics" in a similar way to how a gamer learns about the world of a video game by interacting with it. However, most existing proof assistants are not really targeted at this level, so I worry that the difficulty of learning to use them could outweigh the advantages.

What experiences and research have there been with this sort of thing?

Note that I am not asking about using a proof assistant in the teaching of a class about formal logic. I know that this has been done, and experiences and research on it is not totally irrelevant to what I'm asking, but the audience is very different from a class like I'm considering; students usually already have much more mathematical maturity, and an existing understanding of what a "proof" is, coming into a formal logic class.

I am thinking about teaching a university-level "introduction to proofs" class (mainly for math and CS majors) making use of a computer proof assistant like Coq. I feel like there is a lot of potential benefit here, in that the students can get immediate feedback about what works and what doesn't when interacting with the proof assistant, thereby learning about the "world of mathematics" in a similar way to how a gamer learns about the world of a video game by interacting with it. However, most existing proof assistants are not really targeted at this level, so I worry that the difficulty of learning to use them could outweigh the advantages.

What experiences and research have there been with this sort of thing?

Note that I am not asking about using a proof assistant in the teaching of a class about formal logic. I know that this has been done, and experiences and research on it is not totally irrelevant to what I'm asking, but the audience is very different from a class like I'm considering; students usually already have much more mathematical maturity, and an existing understanding of what a "proof" is, coming into a formal logic class.

Edit: For further clarification, while I'm certainly interested to hear opinions and suggestions, what I'm really asking about is, as I said, experiences and research. In other words, have you or someone else done this?

1
source | link

Teaching logic with a proof assistant

I am thinking about teaching a university-level "introduction to proofs" class (mainly for math and CS majors) making use of a computer proof assistant like Coq. I feel like there is a lot of potential benefit here, in that the students can get immediate feedback about what works and what doesn't when interacting with the proof assistant, thereby learning about the "world of mathematics" in a similar way to how a gamer learns about the world of a video game by interacting with it. However, most existing proof assistants are not really targeted at this level, so I worry that the difficulty of learning to use them could outweigh the advantages.

What experiences and research have there been with this sort of thing?

Note that I am not asking about using a proof assistant in the teaching of a class about formal logic. I know that this has been done, and experiences and research on it is not totally irrelevant to what I'm asking, but the audience is very different from a class like I'm considering; students usually already have much more mathematical maturity, and an existing understanding of what a "proof" is, coming into a formal logic class.