Do you know of a "beginner mathematics" using Coq or some other proof assistant? The audience would be people with no formal training in mathematics at all, covering the basics. The first volume of Software Foundations partially covers this, but only very partially.

Have you seen Kevin Buzzard's Natural Number Game https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

I hadn't, and just did. It's nice, but it looks rather targeted to people who know mathematics and have to learn proof assistants. (You wouldn't teach induction this quickly for the first time ever.)

There is a formalization of the french high school exams by caterine lelay.

Is there a link to that?

Do you know about Edukera? https://www.edukera.com/

@Cody Roux Can't find it at the moment, but @Sylvie Boldo and @Guillaume Melquiond will certainly know more.

Those are the "Bac S 2013" examples from Coquelicot : https://gitlab.inria.fr/coquelicot/coquelicot/-/tree/master/examples

But they do not qualify as a course. They are just an exam done using Coq in real time.

I know about Edukera, but I think it's a properietary service you have to pay for? (I just looked at the website and I'm amused by the slightly broken English.)

You may look at MPCTT, https://github.com/uds-psl/MPCTT for inspiration. It works well for 2nd semester students at Saarland University, after courses on functional programming and mathematics (calculus) in the first semester (in both of which they see induction).

Gabriel Scherer said:

I know about Edukera, but I think it's a properietary service you have to pay for? (I just looked at the website and I'm amused by the slightly broken English.)

Unfortunately yes. They are talking of redoing it as an open source project but I don't know when this will happen.

Just to pick up on this, at sorbonne paris nord we will replace the "methodology in maths" lessons by hands-on session using Coq. It will consists in 18 hours taught to first year student in CS and Maths, given by Pierre Rousselin, Micaela Mayero and myself. The goal is to understand what can and can't be done in a proof, and not to teach maths or type theory. If anyone has any experience in that kind of course we would be happy to hear about it !

Last updated: Dec 01 2023 at 07:01 UTC