The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 09/20/2012 04:50 AM, Julien Narboux wrote: In France, André Hirschowitz and Loic Pottier and Xiao Gang have performed some experiments about using Coq to teach mathematics. see:http://math.unice.fr/~ah/div/bghp.pdf

Thanks.  Someone pointed me to those slides before, but what I'd really like to see are example interactions.  I had a hard time understanding what the student proof experience would be.

Christophe Raffalli is also using his own tool called Phox to teach maths:
http://www.lama.univ-savoie.fr/~raffalli/?page=cours&lang=fr

Even the "English version" is in French, so unfortunately the page isn't very helpful to me. ;)