diff --git a/data/courses.yaml b/data/courses.yaml index c134ad5aac..f3718efeda 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -2,6 +2,7 @@ # # `name`: the title of the course # `instructor`: the name of the person or people who taught the course +# `institution`: the name of the institution at which the course was taught # `year`: the most recent year the course was taught # `lean_version`: 3 or 4, the Lean version of the most recent iteration of the course # `summary`: a description of what was covered and done in the course @@ -19,7 +20,7 @@ - name: Some high-school mathematics in Lean instructor: Peter Pfaffelhuber - location: University of Freiburg, Germany + institution: 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 lean_version: 3 @@ -35,7 +36,7 @@ year: 2023 - name: Formalising Mathematics 2023 instructor: Kevin Buzzard - location: Imperial College London + institution: 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 lean_version: 3 @@ -47,7 +48,7 @@ year: 2023 - name: Interactive Theorem Proving instructor: Jeremy Avigad - location: Department of Mathematical Sciences, Carnegie Mellon University + institution: 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 lean_version: 3 @@ -60,7 +61,7 @@ year: 2022 - name: Logic and Mechanized Reasoning instructor: Jeremy Avigad - location: Department of Computer Science, Carnegie Mellon University + institution: Carnegie Mellon University 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 @@ -71,7 +72,7 @@ year: 2021 - name: Logic and Proof instructor: Jeremy Avigad - location: Department of Philosophy, Carnegie Mellon University + institution: Carnegie Mellon University material: https://leanprover.github.io/logic_and_proof/ lean_version: 3 tags: ['logic', 'intro to proof'] @@ -79,7 +80,7 @@ year: 2017 - name: Proofs and Programs instructor: Siddhartha Gadgil - location: Department of Mathematics, Indian Institute of Science, Bangalore + institution: Indian Institute of Science, Bangalore website: http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/ repo: https://github.com/siddhartha-gadgil/proofs-and-programs-2023 material: http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023.html @@ -99,7 +100,7 @@ lean_version: 4 - name: Modern Mathematics with Lean instructor: Gihan Marasingha - location: University of Exeter + institution: University of Exeter website: https://gihanmarasingha.github.io/modern-maths-pages/ lean_version: 3 tags: ['intro to proof', 'logic', 'mathematics'] @@ -110,7 +111,7 @@ year: 2022 - name: Theorem Prover Lab -- Applications in Programming Languages instructor: Jakob von Raumer - location: Faculty of Informatics, KIT + institution: Karlsruhe Institute of Technology repo: https://github.com/IPDSnelting/tba-2022 website: https://pp.ipd.kit.edu/lehre/SS2022/tba/?lang=de notes: The website is partially German, includes more slides and the project descriptions. @@ -126,7 +127,7 @@ year: 2022 - name: Discrete Mathematics instructor: Heather Macbeth - location: Fordham University + institution: Fordham University material: https://hrmacbeth.github.io/math2001 repo: https://github.com/hrmacbeth/math2001 tags: ['intro to proof', 'mathematics'] @@ -147,7 +148,7 @@ year: 2023 - name: Complement to general Analysis/Algebra 1st year undergraduate course instructor: Frédéric Tran Minh - location: Esisar, Grenoble Institute of Technology + institution: Esisar, Grenoble Institute of Technology notes: 1st year students, 6 x 1,5h repo: https://github.com/ftranminh/Esisar_MA121_HA_lean_2023 summary: > @@ -164,7 +165,7 @@ year: 2023 - name: Logique et démonstrations assistées par ordinateur instructor: Patrick Massot - location: Université Paris-Saclay + institution: Université Paris-Saclay website: https://www.imo.universite-paris-saclay.fr/~patrick.massot/enseignement/ repo: https://github.com/PatrickMassot/MDD154/ notes: @@ -185,7 +186,7 @@ year: 2023 - name: Introduction to Proofs with Lean Proof Assistant instructor: Sina Hazratpour - location: Johns Hopkins University + institution: Johns Hopkins University 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. @@ -194,7 +195,7 @@ year: 2022 - name: Transition to Advanced Mathematics instructor: Matthew Ballard - location: University of South Carolina + institution: 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: [ 'intro to proof', 'mathematics'] @@ -202,7 +203,7 @@ year: 2022 - name: Formalization and mathematics instructor: Matthew Ballard - location: University of South Carolina + institution: 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: ['mathematics', 'computer science', 'advanced'] @@ -210,7 +211,7 @@ lean_version: 4 - name: Formalization of mathematics instructor: Matthew Ballard - location: University of South Carolina + institution: 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: ['mathematics', 'advanced'] @@ -218,7 +219,7 @@ year: 2023 - name: Lean learning group 2023 instructor: Patrick Kinnear - location: Glasgow-Maxwell School + institution: Glasgow-Maxwell School website: https://www.maths.ed.ac.uk/~pkinnear/leancourse/ summary: > A 1-semester course aimed at graduate students in algebra and related topics at Edinburgh, Heriot-Watt and Glasgow universities. @@ -239,7 +240,7 @@ year: 2023 - name: Logic and Modelling instructor: Robert Y. Lewis, Jasmin Blanchette, Anne Baanen - location: Vrije Universiteit Amsterdam + institution: 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 proof', 'logic', 'computer science'] @@ -250,7 +251,7 @@ year: 2023 - name: Formal Proof and Verification instructor: Robert Y. Lewis - location: Brown University + institution: Brown University website: https://browncs1951x.github.io/ material: https://lean-forward.github.io/hitchhikers-guide/2023/ repo: https://github.com/BrownCS1951x/fpv2023 @@ -269,7 +270,7 @@ year: 2023 - name: Discrete Structures and Probability instructor: Robert Y. Lewis - location: Brown University + institution: Brown University website: https://cs22.io/ repo: https://github.com/brown-cs22/CS22-Lean-2023 lean_version: 4 @@ -287,7 +288,7 @@ year: 2023 - name: Graduate Introduction to Logic instructor: Bjørn Kjos-Hanssen - location: University of Hawaii at Manoa + institution: University of Hawaii at Manoa website: https://math.hawaii.edu/wordpress/bjoern/math-654-fall-2022/ material: https://github.com/bjoernkjoshanssen/math654 tags: ['logic', 'mathematics', 'advanced'] @@ -305,7 +306,7 @@ year: 2022 - name: Formal Proof instructor: Jim Fowler - location: The Ohio State University + institution: The Ohio State University website: https://github.com/math4345 repo: https://github.com/math4345/lectures lean_version: 4 @@ -322,7 +323,7 @@ year: 2023 - name: Topoloía general instructor: Miguel Marco - location: Universidad de Zaragoza, Spain + institution: Universidad de Zaragoza 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 lean_version: 3