lean_teaching.yaml

---
buzzard2023:
  name: Formalising Mathematics 2023
  instructor: Kevin Buzzard
  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']
  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.
    I'm teaching the course again in 2024 and then it will be in Lean 4.
avigad1:
  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
  pdf: https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf
  tags: ['formalization of mathematics']
  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 MIL with weekly homework assignments.
    Students did a small independent project at the halfway point, and a larger one at the end.
avigad2:
  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/']
  repo: https://github.com/avigad/lamr
  pdf: https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf
  tags: ['logic', 'automated reasoning', 'SAT', 'SMT', 'first-order theorem provers']
  summary: >
    "This course does three things: 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."
avigad3:
  name: Logic and Proof
  instructor: Jeremy Avigad
  location: Department of Philosophy, Carnegie Mellon University
  website: https://leanprover.github.io/logic_and_proof/
  pdf: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf
  tags: ['introduction to logic', 'introduction to proof']
  summary: This is an introduction to logic and mathematical reasoning for a general audience.
gadgil2023:
  name: Proofs and Programs
  location: Department of Mathematics, Indian Insititute of Science, Bangalore
  website: http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/
  repo: https://github.com/siddhartha-gadgil/proofs-and-programs-2023
  docs: http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023.html
  summary: >
    This was an introduction to proving, programming and proving programs in Lean, and also the Dependent Type Theory foundations of Lean.
    The evaluation was based mainly on projects but also on labs.
  experiences: >
    My plan was to live code, then clean-up and add documentation and generate notes with DocGen4.
    This worked very well for a month, with a lot of questions and my adapting explanations.
    Once the projects started the decoupling of lectures and evaluation led to a sharp drop in attendance.
    I course corrected and made lectures into project demo/help/live-coding.
    Advanced students explaining what they had done and less advanced explained what they had,
    where they were stuck, what they needed etc and I (and their felow 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.
raumer2022:
  name: Theorem Prover Lab -- Applications in Programming Languages
  instructor: Jakob von Raumer
  location: Faculty of Informatics, KIT
  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.
  summary: >
    Masters course for computer science students with the first half of the term consisting of a hands-on introduction to Lean 4 and type theory
    and the second half consisting of the students working on either a semantics/compiler project or a formalisation of a graph theory problem.
  experiences: >
    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.
macbeth2001:
  name: Discrete Mathematics
  instructor: Heather Macbeth
  location: Fordham University
  website: https://hrmacbeth.github.io/math2001
  repo: https://github.com/hrmacbeth/math2001
  tags: ['intro to proofs', 'number theory', 'combinatorics']
  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).
    It's the standard syllabus of a US "intro to proofs" course for first/second-year undergraduates,
    covering "proof techniques" (cases/existentials/contradiction/induction), good style in proof writing,
    parity/divisibility/modular arithmetic/GCD/primes, "sufficiently large", recurrence relations,
    injective/surjective/bijective functions, reflexive/symmetric/antisymmetric/transitive relations, and set operations.
  experiences: >
    The course is ongoing, but so far so good!
    I invested a lot of energy in writing custom tactics which perform exactly one step of reasoning that I would permit on paper,
    and deliberately never mentioned several more powerful tactics.
    This is very useful if the course is explicitly supposed to teach good style in proof writing.
    It lets you off the hook in grading -- you can just say "that's not enough detail -- Lean wouldn't accept it!"
Esisar_MA121_HA_lean_2023:
  name: Complement to general Analysis/Algebra 1st year undergraduate course
  instructor: Frédéric Tran Minh
  context: Esisar engineering school, 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.
    We used proof-term style in Lean.
  experiences:
    - 1st time we use a proof assistant to teach maths
    - students globally appreciated it (feedback, autonomy, playful)
    - 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
massot:
  name: Logique et démonstrations assistées par ordinateur
  instructor: Patrick Massot
  website: https://www.imo.universite-paris-saclay.fr/~patrick.massot/enseignement/
  repo: https://github.com/PatrickMassot/MDD154/
  notes:
    - Of course there is also a private repo with solutions, and I can give solutions to interested teachers
    - 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: ['intro to proofs', 'analysis', 'natural language input']
  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.
    The main mathematical topic of this course is elementary real analysis, especially the theory of convergent sequences and continuous functions.
    Since 2021 I use a controlled natural language for input in order to facilitate transferring Lean proofs to pen and paper proofs.
  experiences: >
    This course really works well, and it will probably continue for a long time.
    The idea to use controlled natural language tactics seems a lot more efficient than the native syntax to ensure students improve at pen and paper proofs.
kinnear:
  name: Lean learning group 2023
  instructor: Patrick Kinnear
  website: https://www.maths.ed.ac.uk/~pkinnear/leancourse/
  tags: algebra
  summary: >
    A 1-semester course aimed at graduate students in algebra and related topics at Edinburgh, Heriot-Watt and Glasgow universities. Aimed to approach Lean as mathematicians and future formalisers, establishing proficiency in tactic mode. For the first part of the course we learned the basics of first-order logic in Lean using the tutorials project, before discussing some basics if types and type classes to talk about formalising algebra. Also made use of lftcm2020 exercise sheets, and MiL. Concluded with a hackathon working on some group projects.
  experiences: >
    We tried to avoid touching on too much type theory early on to get people confidently interacting with Lean quickly. In retrospect, it would have been good to cover this in more depth (albeit only later in the course, after establishing confidence interacting with Lean) to aid in dealing with the inevitable issues that arise when formalising an interesting piece of mathematics. Also, we originally aimed for the outcome of the course to be group projects working on mathlib contributions, 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).