Gabriel Scherer (Jun 14 2021 at 19:03): 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.
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/
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.)
Bas Spitters (Jun 14 2021 at 20:36):There is a formalization of the french high school exams by caterine lelay.
Cody Roux (Jun 14 2021 at 20:54):Is there a link to that?
Théo Zimmermann (Jun 15 2021 at 06:43):Do you know about Edukera? https://www.edukera.com/
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.
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.
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.)
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).
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.
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: Apr 20 2024 at 15:01 UTC