From 686c039018ea0f2af1636835fdf0ec65e4ff0391 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Wed, 18 Oct 2023 14:10:04 -0400 Subject: [PATCH] update tags --- data/courses.yaml | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/data/courses.yaml b/data/courses.yaml index fdffb4e664..7c897b9dc7 100644 --- a/data/courses.yaml +++ b/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,7 +60,7 @@ 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 @@ -68,7 +68,7 @@ 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