Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
cleanup website/repo/materials
Browse files Browse the repository at this point in the history
robertylewis committed Oct 18, 2023
1 parent fb04976 commit 24a7641
Showing 1 changed file with 6 additions and 9 deletions.
15 changes: 6 additions & 9 deletions data/courses.yaml
Original file line number Diff line number Diff line change
@@ -7,7 +7,7 @@
# `tags`: a list of tags (see below)
# `website` (optional): the course's home page
# `material` (optional): a link to a textbook, course notes, etc
# `repository` (optional): a link to the course's project repository, e.g. on GitHub
# `repo` (optional): a link to the course's project repository, e.g. on GitHub
# `experiences` (optional): a reflection about how the course went, things that could be done differently, etc
# `language` (optional): if the instruction language was not English, what language was it?
#
@@ -45,7 +45,6 @@
- name: Interactive Theorem Proving
instructor: Jeremy Avigad
location: Department of Mathematical Sciences, Carnegie Mellon University
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', 'lean3']
@@ -58,7 +57,7 @@
- name: Logic and Mechanized Reasoning
instructor: Jeremy Avigad
location: Department of Computer Science, Carnegie Mellon University
website: ['https://www.cs.cmu.edu/~mheule/15217-f21/', 'https://avigad.github.io/lamr/']
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']
@@ -68,8 +67,7 @@
- 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
material: https://leanprover.github.io/logic_and_proof/
tags: ['introduction to logic', 'introduction 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
@@ -120,7 +118,7 @@
- name: Discrete Mathematics
instructor: Heather Macbeth
location: Fordham University
website: https://hrmacbeth.github.io/math2001
material: https://hrmacbeth.github.io/math2001
repo: https://github.com/hrmacbeth/math2001
tags: ['intro to proofs', 'number theory', 'combinatorics', 'lean4']
summary: >
@@ -141,7 +139,6 @@
instructor: Frédéric Tran Minh
location: Esisar, Grenoble Institute of Technology
notes: 1st year students, 6 x 1,5h
website: https://github.com/ftranminh/Esisar_MA121_HA_lean_2023
repo: https://github.com/ftranminh/Esisar_MA121_HA_lean_2023
summary: >
Short module introducing proof to 1st year undergraduates using Lean3 - in French.
@@ -238,7 +235,7 @@
location: Brown University
website: https://browncs1951x.github.io/
material: https://lean-forward.github.io/hitchhikers-guide/2023/
repository: https://github.com/BrownCS1951x/fpv2023
repo: https://github.com/BrownCS1951x/fpv2023
tags: ['formalization of mathematics', 'logic', 'verification', 'lean4']
summary: >
This is an upper level undergraduate/graduate course that teaches the theory and practice of proof assistants using Lean.
@@ -255,7 +252,7 @@
instructor: Robert Y. Lewis
location: Brown University
website: https://cs22.io/
repository: https://github.com/brown-cs22/CS22-Lean-2023
repo: https://github.com/brown-cs22/CS22-Lean-2023
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.

0 comments on commit 24a7641

Please sign in to comment.