Papers

Stream: Lean for teaching

[Andrew Ashworth]

Somebody wrote up their experience using Coq to teach proof: https://arxiv.org/pdf/1803.01466.pdf

[Patrick Massot]

That's a very interesting paper. I wish I had it three months ago

[Patrick Massot]

It seems there are more people using proof assistants for teaching proofs than I thought, although there are all in CS department, so it's difficult to compare