update tags

data/courses.yaml

@@ -21,7 +21,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: ['German', 'intro to proofs', 'formalization of mathematics','divisibility', 'lean3']
+  tags: ['German', 'intro to proof', 'mathematics', '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 
@@ -36,7 +36,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', 'lean3']
+  tags: ['mathematics', 'lean3', 'advanced']
   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.
@@ -47,7 +47,7 @@
   location: Department of Mathematical Sciences, Carnegie Mellon University
   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', 'lean3']
+  tags: ['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
@@ -60,15 +60,15 @@
   website: https://www.cs.cmu.edu/~mheule/15217-f21/
   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', 'lean3']
+  tags: ['logic', 'automated reasoning', 'lean3', 'advanced']
   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.
   year: 2021
 - name: Logic and Proof
   instructor: Jeremy Avigad
   location: Department of Philosophy, Carnegie Mellon University
   material: https://leanprover.github.io/logic_and_proof/
-  tags: ['introduction to logic', 'introduction to proof', 'lean3']
+  tags: ['logic', 'intro to proof', 'lean3']
   summary: This is an introduction to logic and mathematical reasoning for a general audience. It was taught in the philosophy department at CMU twice.
   year: 2017
 - name: Proofs and Programs
@@ -89,12 +89,12 @@
     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.
   year: 2023
-  tags: ['lean4']
+  tags: ['intro to proof', 'computer science', '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', 'lean3']
+  tags: ['intro to proof', 'logic', 'mathematics', '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
@@ -113,14 +113,14 @@
     This was already the second year we used Lean 4 and it was good to do it in person again after teaching exclusively online due to Covid the year before.
     We had different levels of learning speed among the students but in the end everybody go the point where they intuitively could use Lean.
     Some students were really eager to golf every proof.
-  tags: ['German', 'computer science']
+  tags: ['German', 'computer science', 'advanced']
   year: 2022
 - name: Discrete Mathematics
   instructor: Heather Macbeth
   location: Fordham University
   material: https://hrmacbeth.github.io/math2001
   repo: https://github.com/hrmacbeth/math2001
-  tags: ['intro to proofs', 'number theory', 'combinatorics', 'lean4']
+  tags: ['intro to proof', 'mathematics', '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).
@@ -149,7 +149,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', 'French']
+  tags: ['lean3', 'French', 'mathematics', 'intro to proof']
   year: 2023
 - name: Logique et démonstrations assistées par ordinateur
   instructor: Patrick Massot
@@ -161,7 +161,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: ['French', 'intro to proofs', 'analysis', 'natural language input', 'lean3']
+  tags: ['French', 'intro to proof', '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.
@@ -177,28 +177,28 @@
   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']
+  tags: ['lean3', 'intro to proof', 'mathematics']
   year: 2022
 - 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']
+  tags: ['lean4', 'intro to proof', 'mathematics']
   year: 2022
 - 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']
+  tags: ['lean4', 'mathematics', 'computer science', 'advanced']
   year: 2023
 - 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']
+  tags: ['lean4', 'mathematics', 'advanced']
   year: 2023
 - name: Lean learning group 2023
   instructor: Patrick Kinnear
@@ -218,14 +218,14 @@
     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']
+  tags: ['lean3', 'mathematics', 'advanced']
   year: 2023 
 - 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', 'lean3']
+  tags: ['introduction to proof', 'logic', 'computer science', '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).
@@ -236,7 +236,7 @@
   website: https://browncs1951x.github.io/
   material: https://lean-forward.github.io/hitchhikers-guide/2023/
   repo: https://github.com/BrownCS1951x/fpv2023
-  tags: ['formalization of mathematics', 'logic', 'verification', 'lean4']
+  tags: ['logic', 'computer science', 'lean4', 'advanced']
   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,
@@ -253,7 +253,7 @@
   location: Brown University
   website: https://cs22.io/
   repo: https://github.com/brown-cs22/CS22-Lean-2023
-  tags: ['intro to proofs', 'number theory', 'combinatorics', 'lean4']
+  tags: ['intro to proof', 'computer science', '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.
@@ -270,7 +270,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', 'lean3']
+  tags: ['logic', 'mathematics', 'lean3', 'advanced']
   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;
@@ -287,7 +287,7 @@
   location: The Ohio State University
   website: https://github.com/math4345
   repo: https://github.com/math4345/lectures
-  tags: ['formalization of mathematics', 'lean4']
+  tags: ['mathematics', 'lean4', 'advanced']
   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
@@ -303,7 +303,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: ['Spanish', 'topology', 'lean3']
+  tags: ['Spanish', 'mathematics', '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