The Coq mailing list

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

On 09/17/2012 05:31 PM, Andrej Bauer wrote:
> are you aware of the ForMath project,
> http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath ? It
> seems relevant to what you are talking about. See for example the math
> classes library at http://math-classes.org. In general, formalization
> of mathematics is a non-trivial issue.
>    

I've been vaguely aware of that project.  I believe it deals with the 
math of real mathematicians, which, complexity-wise, is far beyond what 
we teach computer science majors, at least in the schools I've been 
involved with, where only a small fraction of the students will go on to 
apply mathematics regularly in their careers.

Certainly formalizing any subject well is a non-trivial undertaking, and 
that is why I am looking around for collaborators. :)

> It would be interesting to see an experiment in teaching math through
> a proof assistant. I think it is quite hard to do so well. It may be
> the case that a Coq library for research-level math, or
> "system-building" math is not appropriate for teaching. Who knows,
> nobody has ever tried!
>    

Right, that's my assumption, i.e., that different tools are appropriate 
for professionals vs. beginning students.

To be concrete about the sort of class I want to target first, here it 
is at MIT:
    http://courses.csail.mit.edu/6.042/fall12/

It's an introduction to the language of math and proof techniques, plus 
time spent on such CS literacy areas as number theory, graph theory, 
combinatorics, and probability.