feat (Lean courses around the world): add M&M (#348)

Co-authored-by: Eric Wieser <[email protected]>

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