Skip to content

Commit

Permalink
update institutions
Browse files Browse the repository at this point in the history
  • Loading branch information
robertylewis committed Oct 18, 2023
1 parent b246929 commit 36bf8e8
Showing 1 changed file with 23 additions and 22 deletions.
45 changes: 23 additions & 22 deletions data/courses.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -71,15 +72,15 @@
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']
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
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
Expand All @@ -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']
Expand All @@ -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.
Expand All @@ -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']
Expand All @@ -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: >
Expand All @@ -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:
Expand All @@ -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.
Expand All @@ -194,31 +195,31 @@
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']
lean_version: 4
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']
year: 2023
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']
lean_version: 4
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.
Expand All @@ -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']
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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']
Expand All @@ -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
Expand All @@ -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
Expand Down

0 comments on commit 36bf8e8

Please sign in to comment.