Add lean3 and lean4 tags

data/courses.yaml

@@ -3,7 +3,7 @@
   location: University of Freiburg, Germany
   website: https://github.com/pfaffelh/schulmathematik_mit_lean/
   material: https://github.com/pfaffelh/schulmathematik_mit_lean/blob/master/Manuskript/skript.pdf
-  tags: ['intro to proofs', 'formalization of mathematics','divisibility']
+  tags: ['intro to proofs', 'formalization of mathematics','divisibility', 'lean3']
   summary: >
     The aim of the course is to learn some Lean 3 using easy mathemtics (such as divisibility, \sqrt 2 \notin \Q, and the 
     pigeonwhole principle). The course is in German and was taught in summer 2023 for one full semester with weekly homeworks. We met once a week, discussed upcoming topics and 
@@ -17,7 +17,7 @@
   location: Imperial College London
   website: https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/index.html
   repo: https://github.com/ImperialCollegeLondon/formalising-mathematics-2023
-  tags: ['algebra', 'analysis', 'geometry', 'topology', 'logic', 'sets', 'functions', 'groups', 'lattices', 'finiteness', 'filters', 'vector spaces', 'measure theory', 'number theory', 'commutative algebra']
+  tags: ['algebra', 'analysis', 'geometry', 'topology', 'logic', 'sets', 'functions', 'groups', 'lattices', 'finiteness', 'filters', 'vector spaces', 'measure theory', 'number theory', 'commutative algebra', 'lean3']
   summary: >
     The course is project-based; the students must write three projects on undergraduate mathematics.
     The lectures are me live Lean coding, solving the sorrys in the repo.
@@ -28,7 +28,7 @@
   website: https://leanprover-community.github.io/mathematics_in_lean/
   repo: https://github.com/leanprover-community/mathematics_in_lean
   material: https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf
-  tags: ['formalization of mathematics']
+  tags: ['formalization of mathematics', 'lean3']
   summary: >
     This was taught as a third-year undergraduate course.
     We spent a little more than half the semester working through the first 6 chapters of
@@ -40,15 +40,15 @@
   website: ['https://www.cs.cmu.edu/~mheule/15217-f21/', 'https://avigad.github.io/lamr/']
   repo: https://github.com/avigad/lamr
   material: https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf
-  tags: ['logic', 'automated reasoning', 'SAT', 'SMT', 'first-order theorem provers']
+  tags: ['logic', 'automated reasoning', 'SAT', 'SMT', 'first-order theorem provers', 'lean3']
   summary: >
     This course introduces students to the theory of propositional and first-order logic, shows them how to implement fundamental logical algorithms in Lean 4, and shows them how to use automated reasoning tools.
 - name: Logic and Proof
   instructor: Jeremy Avigad
   location: Department of Philosophy, Carnegie Mellon University
   website: https://leanprover.github.io/logic_and_proof/
   material: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf
-  tags: ['introduction to logic', 'introduction to proof']
+  tags: ['introduction to logic', 'introduction to proof', 'lean3']
   summary: This is an introduction to logic and mathematical reasoning for a general audience.
 - name: Proofs and Programs
   instructor: Siddhartha Gadgil
@@ -67,11 +67,12 @@
     Advanced students explaining what they had done and less advanced explained what they had,
     where they were stuck, what they needed etc and I (and their fellow students) helped them get unstuck.
     This is working well. Next time I teach I will transition earlier and in a more planned way to this mode.
+  tags: ['lean4']
 - name: Modern Mathematics with Lean
   instructor: Gihan Marasingha
   location: University of Exeter
   website: https://gihanmarasingha.github.io/modern-maths-pages/
-  tags: ['proof', 'logic', 'sets', 'functions', 'real numbers', 'sequences', 'groups']
+  tags: ['proof', 'logic', 'sets', 'functions', 'real numbers', 'sequences', 'groups', 'lean3']
   summary: >
     This is a game-based introduction to undergraduate pure mathematics, starting with equations, natural numbers, logic,
     sets, function, real numbers and sequences with draft sections on groups. A book is being written to accompany the
@@ -94,7 +95,7 @@
   location: Fordham University
   website: https://hrmacbeth.github.io/math2001
   repo: https://github.com/hrmacbeth/math2001
-  tags: ['intro to proofs', 'number theory', 'combinatorics']
+  tags: ['intro to proofs', 'number theory', 'combinatorics', 'lean4']
   summary: >
     I have written this as a course which is completely bilingual between English and Lean,
     with every example presented both ways (students also have to solve every homework problem both ways).
@@ -123,6 +124,7 @@
     - some of them think it helped them with maths
     - most of them found the Lean syntax difficult (they also tended to attribute their shortcomings in maths to a programming difficulties)
     - many of them found the Lean error messages helpless
+  tags: ['lean3']
 - name: Logique et démonstrations assistées par ordinateur
   instructor: Patrick Massot
   location: Université Paris-Saclay
@@ -133,7 +135,7 @@
     - no single pdf but lecture notes at https://www.imo.universite-paris-saclay.fr/~patrick.massot/mdd154/,
     - tactic cheat sheets at https://www.imo.universite-paris-saclay.fr/~patrick.massot/mdd154/aide-memoire.pdf,
     - full tactic reference at https://www.imo.universite-paris-saclay.fr/~patrick.massot/mdd154/reference.pdf
-  tags: ['intro to proofs', 'analysis', 'natural language input']
+  tags: ['intro to proofs', 'analysis', 'natural language input', 'lean3']
   summary: >
     Since January 2019, I am using Lean to teach first year undergrad double major maths/CS students how to find and write mathematical proofs.
     I first did it alone and then with Frédéric Bourgeois and Christine Paulin.
@@ -148,21 +150,25 @@
   website: https://sinhp.github.io/teaching/2022-introduction-to-proofs-with-Lean
   repo: https://github.com/sinhp/ProofLab
   summary: An Introduction To Proofs course at Johns Hopkins in Fall 2022 entirely in Lean (teaching and assessment) culminating in the proof of Yoneda Lemma.
+  tags: ['lean3']
 - name: Transition to Advanced Mathematics
   instructor: Matthew Ballard
   location: University of South Carolina
   website: https://300.f22.matthewrobertballard.com/
   summary: Our intro to proofs course. (Fall 2020) Lean was about 1/3 of the course. (Fall 2022) A second iteration using Lean 4.
+  tags: ['lean4']
 - name: Formalization and mathematics
   instructor: Matthew Ballard
   location: University of South Carolina
   website: https://411.s23.matthewrobertballard.com
   summary: Spring 2023. More a hybrid math-CS course that was focused on building ability with Lean and expanding students perspectives on math and programming.
+  tags: ['lean4']
 - name: Formalization of mathematics
   instructor: Matthew Ballard
   location: University of South Carolina
   website: https://github.com/UofSC-Spring-2023-Math-768-001
   summary: Spring 2023. A graduate course where we spent about 2/3's of the course working through exercises from one of Kevin's classes in Lean 3 and then switched to bounding the edge chromatic number of graphs in Lean 4.
+  tags: ['lean4']
 - name: Lean learning group 2023
   instructor: Patrick Kinnear
   location: Glasgow-Maxwell School
@@ -182,12 +188,13 @@
     but would now say that re-framing the goal as formalising something new in a format that is useful to you as a learner
     (e.g. as a worksheet/interactive part of a textbook) is a better goal pedagogically
     (and could still lead to, e.g., a mathlib contribution in the process even if that isn't the explicit goal).
+  tags: ['lean3']
 - name: Logic and Modelling
   instructor: Robert Y. Lewis, Jasmin Blanchette, Anne Baanen
   location: Vrije Universiteit Amsterdam
   website: https://studiegids.vu.nl/en/2022-2023/courses/X_401015
   material: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf
-  tags: ['introduction to logic', 'modal logic']
+  tags: ['introduction to logic', 'modal logic', 'lean3']
   summary: >
     This course introduces computer science students to propositional logic, predicate logic and modal logic.
     The course uses two formal proof systems: natural deduction (exam) and Lean (homework assignments).
@@ -196,7 +203,7 @@
   location: Brown University
   website: https://browncs1951x.github.io/
   material: https://github.com/BrownCS1951x/fpv2022
-  tags: ['formalization of mathematics', 'logic', 'verification']
+  tags: ['formalization of mathematics', 'logic', 'verification', 'lean3']
   summary: >
     This is an upper level undergraduate/graduate course that teaches the theory and practice of proof assistants using Lean.
     Topics covered include verification of functional programs, PL semantics, mathematical structures, metaprogramming,
@@ -212,7 +219,7 @@
   location: Brown University
   website: https://cs22.io/
   material: https://github.com/brown-cs22/CS22-Lean-2023
-  tags: ['intro to proofs', 'number theory', 'combinatorics']
+  tags: ['intro to proofs', 'number theory', 'combinatorics', 'lean4']
   summary: >
     This is a large introductory course that is taken by most computer science students at Brown.
     It teaches logic, combinatorics, number theory, and probability, focusing on concepts that are important in computer science.
@@ -228,7 +235,7 @@
   location: University of Hawaii at Manoa
   website: https://math.hawaii.edu/wordpress/bjoern/math-654-fall-2022/
   material: https://github.com/bjoernkjoshanssen/math654
-  tags: ['mathematical logic']
+  tags: ['mathematical logic', 'lean3']
   summary: >
     A graduate course in mathematical logic taken mostly by MA and PhD students in mathematics and offered every other year (Fall 2016+2n, n=0,1,2,3,4).
     Model theory, computability theory, set theory. In particular syntax and semantics of first order logic; incompleteness, completeness, and compactness theorems;
@@ -244,7 +251,7 @@
   location: The Ohio State University
   website: https://github.com/math4345
   repo: https://github.com/math4345/lectures
-  tags: ['formalization of mathematics']
+  tags: ['formalization of mathematics', 'lean4']
   summary: >
     This course provides an introduction to formal proof in mathematics. It is designed for math
     majors who seek a comprehensive understanding of how to use proof assistants and how to encode
@@ -259,7 +266,7 @@
   location: Universidad de Zaragoza, Spain
   website: https://sia.unizar.es/doa/consultaPublica/look[conpub]MostrarPubGuiaDocAs?entradaPublica=true&idiomaPais=es.ES&_anoAcademico=2023&_codAsignatura=27008
   repo: https://github.com/miguelmarco/topologia_general_lean
-  tags: ['topology']
+  tags: ['topology', 'lean3']
   summary: >
     It is a standard course on general topology in the Mathematics degree. It is taught in spanish, so the material in the repo uses spanish too.
     It is not a course about Lean: Lean is only used as a complement, to help students grab the steps of rigourous proofs. The usage of Lean is totally