From 820e77332d1c3e3f5d6b3a3c92075d13780dcb29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Sun, 22 Oct 2023 15:29:31 +0200 Subject: [PATCH] feat (Lean courses around the world): add M&M (#348) Co-authored-by: Eric Wieser --- data/courses.yaml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/data/courses.yaml b/data/courses.yaml index da1bdb96cc..e3d010388a 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -312,6 +312,22 @@ The students are willing and able to learn Lean. Including Lean showcases logic as a vibrant rather than dormant area of study. As projects in 2022 students created formalizations of exercise solutions for my book "Automatic complexity", some of which are included at https://github.com/bjoernkjoshanssen/diophantine-lemma +- name: Programování a dokazování v Leanu + instructor: Martin Dvorak + location: online + website: https://mam.mff.cuni.cz/ + repo: https://github.com/madvorak/lean-mam + tags: ['functional programming', 'intro to proofs'] + summary: > + We are a [korespondenční seminář](https://cs.wikipedia.org/wiki/Koresponden%C4%8Dn%C3%AD_semin%C3%A1%C5%99) (lit. "correspondence seminar" in the sense of + a seminar arranged by exchanging letters and emails) called [M\&M](https://cs.wikipedia.org/wiki/M%26M_\(%C4%8Dasopis\)), which is something like + an online course for math-olympiad highschoolers, under the hood of the Faculty of Mathematics and Physics of Charles University in Prague. + All our texts are written in Czech; it is also the language of our in-person meetings. Lean is one of our three topics for the school year 2023/2024. + There will be five volumes with Lean assignments, six volumes in total. We use Lean 4. + Syllabus: (1) the very basics of functional programming; (2) lists; (3) elementary algebraic manipulations; (4) logic; (5) induction. + experiences: > + We currently have 41 active participants (counting students who solved at least three Lean exercises). + Grading solutions doesn't take much time. Creating materials does. year: 2022 - name: Formal Proof instructor: Jim Fowler @@ -346,7 +362,6 @@ the `trylean` bundle, but will reconsider this decision next year. Students seem to be uninterested and/or scared at the beginning, but as i had shown how to use it to prove some example exercises, some have shown more interest. We plan to do an introductory seminar for those that want to learn how to use it. year: 2023 - - name: Formalized Mathematics in Lean instructor: Floris van Doorn institution: University of Bonn @@ -357,3 +372,4 @@ lean_version: 4 summary: > This course is for bachelor and master math students that want to learn formalization and Lean. In the first half of the course I will go through the book Mathematics in Lean, and in the second half each student will choose a formalization project to work on and give a presentation about the formalization. +