Stream: Miscellaneous

Topic: Coq course for beginner mathematics?


view this post on Zulip Gabriel Scherer (Jun 14 2021 at 19:03):

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.

view this post on Zulip Li-yao (Jun 14 2021 at 19:09):

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

view this post on Zulip Gabriel Scherer (Jun 14 2021 at 19:22):

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.)

view this post on Zulip Bas Spitters (Jun 14 2021 at 20:36):

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

view this post on Zulip Cody Roux (Jun 14 2021 at 20:54):

Is there a link to that?

view this post on Zulip Théo Zimmermann (Jun 15 2021 at 06:43):

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

view this post on Zulip Bas Spitters (Jun 15 2021 at 09:48):

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

view this post on Zulip Guillaume Melquiond (Jun 15 2021 at 09:54):

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.

view this post on Zulip Gabriel Scherer (Jun 15 2021 at 12:34):

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.)

view this post on Zulip Gert Smolka (Jun 15 2021 at 15:35):

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).

view this post on Zulip Théo Zimmermann (Jun 15 2021 at 15:41):

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.

view this post on Zulip Marie Kerjean (Jul 06 2021 at 11:14):

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: Aug 19 2022 at 20:03 UTC