The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

Hello,

I just discovered this discussion about teaching maths and using coq.  I 
also feel attracted by this idea.

Here are a few ideas that can be debated.

- We don't need to restrict to discrete maths.  Reasoning about real 
numbers is a good playground for learning mathematics. Epsilon-delta 
proofs, as can be seen in elementary calculus are a good example of 
where rigor is provided by the proof system.

- If the point is about teaching mathematics, then we should stay away 
from the need to restart everything from scratch.  For each course, we 
should provide a set of basic axioms (or a module interface) that gives 
all the knowledge that will be used for this course.  This is already 
said in Adam's initial mail, although he concentrates on "course 
specific tactics libraries".

- Now, there is a question of where the computer enters into play. Coq 
does not like to compute about axiomatic numbers, but we can make it 
compute about natural numbers, integers, or rational numbers.  For a 
student, being able to compute is important: it gives opportunity for 
her to build up her intuition, but having to cope with the fact the 
world is divided between numbers that you can compute with (and in Coq 
there are too many different types in this category: nat, Z, N, Q, not 
counting the efficient versions) and "real" numbers will probably be 
overwhelming.

- For a long time, we have been trying to understand how little you can 
teach about Coq so that people start using it without thinking about the 
basics of the system.  Pierre Courtieu mentioned the work of Frédérique 
Guilhot and Loïc Pottier, who were members of my team.  It has to be 
said that Frédérique is a high school Math teacher and understanding 
what could be shown to a high-school kid was part of our dream.  Loïc 
just left our team to take a full time math teacher job, at freshman 
level.  One of the issues raised by Frédérique was that we should not 
require from users that they need to type, because questions of syntax 
can be utterly vexing.  But maybe this makes sense for high-school kids 
but not for freshmen.

- Concerning automatic grading, I have a few doubts.  What do you want 
to verify?  The capacity to make a complete proof?  Okay, but what about 
nearly good proofs?  I fear you cannot measure progress if you only have 
the "yes/no" answer of whether the students has completed the proof at 
all.  It is more important to see the student learn to build her 
understanding of where to use a proof by induction or not, how to load 
inductions, etc...  This is still too qualitative to be captured by any 
interactive theorem prover, I fear.  I believe that the main reason why 
interactive theorem provers have not been adopted by the mathematical 
community is that they cannot measure "essentially good mathematical 
proofs".  Still, I have always dreamed that students are happy to verify 
their own work on their own by seeing that they are able to get the 
interactive prover's assent.

- My current thinking revolves around the Pi number.  There are several 
ways to look at it and most of them provide a good playground to learn 
some mathematics.  What I am studying currently is "how far are the 
libraries from what you can explain to a freshman".  So in a way, I 
would like to teach about Pi, not about the computer tool, hoping that 
in the process the student would actually get accustomed to the tool.  
The same way as kids learn a natural language by just using it.

Is Mizar more adapted for this kind of endeavor?  The advantage for Coq 
might be the ability to experiment with computation, but this comes at a 
cost (the need to understand that you have several types of numbers).