Zulip Chat Archive

Stream: Lean for teaching

Topic: Papers

Andrew Ashworth (Mar 06 2019 at 06:57):

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

Patrick Massot (Mar 06 2019 at 09:56):

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

Patrick Massot (Mar 06 2019 at 09:57):

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

Last updated: Dec 20 2023 at 11:08 UTC