Zulip Chat Archive

Stream: Lean for teaching

Topic: Lean courses around the world

Johan Commelin (Mar 13 2023 at 18:45):

I am planning to make an overview website of Lean courses as part of our community website. If you've taught a course using Lean and you have some resources available, please write a reply in this thread. It doesn't have to be long, just an itemized list including things like:

  • website for the course
  • repository for the course
  • pdf with course notes
  • some tags (algebra, analysis, logic, intro to proofs, software verfication, automated proofs, ...)
  • if you want: a short abstract/summary
  • if you want: a reflection (would you teach this course again, or were there problems with it that you want to avoid, did you learn general lessons about "teaching Lean" that others should be aware of)

All those items are optional, but the more data the merrier.

Floris van Doorn (Mar 13 2023 at 18:50):

You're aware of the following webpage maintained by @Jeremy Avigad, right? https://avigad.github.io/formal_methods_in_education/
I don't know if it is up-to-date or complete, but it is definitely a good place to start.

Floris van Doorn (Mar 13 2023 at 18:51):

Although I guess that's about resources, not exactly courses

Kevin Buzzard (Mar 13 2023 at 18:54):

Course: formalising mathematics 2023.

Website (under construction): 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
Short abstract/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.

Jeremy Avigad (Mar 13 2023 at 18:56):

Thanks, Floris! I started that page during the summer at the Isaac Newton Institute in 2017. But I haven't touched it in a few years now. It is worth a quick look to see if there is anything still relevant, but I don't think there is much.

Johan, later today I'll add data on courses I have taught at CMU: Interactive Theorem Proving (based on MIL), Logic and Mechanized Reasoning, and the old course based on Logic and Proof.

Jeremy Avigad (Mar 13 2023 at 23:39):

Course: Interactive Theorem Proving (Department of Mathematical Sciences, Carnegie Mellon University)
Website: https://leanprover-community.github.io/mathematics_in_lean/
Repository: https://github.com/leanprover-community/mathematics_in_lean (lectures and assignments are in a private repository)
PDF with course notes: https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf
Tags: formalization of mathematics
Abstract: 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.

Course: Logic and Mechanized Reasoning (Department of Computer Science, Carnegie Mellon University)
Website: https://www.cs.cmu.edu/~mheule/15217-f21/, https://avigad.github.io/lamr/
Repository: https://github.com/avigad/lamr
PDF with course notes: https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf
Tags: logic, automated reasoning, SAT, SMT, first-order theorem provers
Abstract: 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.

Course: Logic and Proof (Department of Philosophy, Carnegie Mellon University)
Website: https://leanprover.github.io/logic_and_proof/
Repository for the course: none
PDF with course notes: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf
Tags: introduction to logic, introduction to proof
Abstract: This is an introduction to logic and mathematical reasoning for a general audience.

Siddhartha Gadgil (Mar 14 2023 at 02:16):

Course: Proofs and Programs (Department of Mathematics, Indian Insititute of Science, Bangalore)
Website: http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/
Repository: https://github.com/siddhartha-gadgil/proofs-and-programs-2023 (both course code and website source).
Docs: http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023.html (generated by docgen4).

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.

Experience so far: 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.

Jakob von Raumer (Mar 14 2023 at 15:20):

Course: Theorem Prover Lab -- Applications in Programming Languages (Faculty of Informatics, KIT)
Repository: https://github.com/IPDSnelting/tba-2022 (includes slides and exercises)
Website: https://pp.ipd.kit.edu/lehre/SS2022/tba/?lang=de (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.

Experience: 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.

Heather Macbeth (Mar 14 2023 at 23:06):

Course: Discrete Mathematics (Fordham University)
Lecture notes/website: https://hrmacbeth.github.io/math2001
Repository: 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.

Reflection: 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!"

Johan Commelin (Mar 15 2023 at 04:20):

Thanks for all the replies so far! I will collect them into a .yaml file in a couple of days.

Frédéric Tran Minh (Mar 16 2023 at 13:35):

Hi Everyone and thank you for all this work & sharing. (1st time I'm posting in Zulip!). I'm quite new with proof assistants, here is my small experience.

Esisar_MA121_HA_lean_2023

  • Course : Complement to general Analysis/Algebra 1st year undergraduate course
  • Context : Esisar engineering school, 1st year students, 6 x 1,5h
  • Website: https://github.com/ftranminh/Esisar_MA121_HA_lean_2023
  • Repository : 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.

  • Experience :

    • 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

Thanks Johan Commelin for your initiative.

Gabriel Ebner (Mar 16 2023 at 23:38):

Thank you Johan! You might also be interested in this thread from last year: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/List.20of.20Lean.20.28university.29.20courses/near/305068451

Patrick Massot (Mar 17 2023 at 08:42):

My course is called "Logique et démonstrations assistées par ordinateur" (Logic and computer assisted proofs)

Johan Commelin (Mar 18 2023 at 17:58):

A first version of the yaml file is available here: https://gist.github.com/8499d85596230c3b412fdf439c84f76d

Johan Commelin (Mar 18 2023 at 17:59):

It will need a bit more curation. And eventually it will generate a nice website on the community home page

Johan Commelin (Mar 18 2023 at 17:59):

I have not yet gone through the thread that Gabriel linked to.

Sina (Apr 12 2023 at 21:30):

I taught an Introduction To Proofs course at Johns Hopkins in Fall 2022 entirely in Lean (teaching and assessment) culminating in the proof of Yoneda Lemma.

Here's the course website:
https://sinhp.github.io/teaching/2022-introduction-to-proofs-with-Lean

and here's the github repo for lectures and homework problem sets:
https://github.com/sinhp/ProofLab

Matthew Ballard (Apr 19 2023 at 19:26):

Late to the party:

  • Fall 2020: Transition to Advanced Mathematics. Our intro to proofs course. Lean was about 1/3 of the course. Unfortunately, I put all course materials in the university Office 365 account so it is difficult to share.
  • Fall 2022: Transition to Advanced Mathematics A second iteration using Lean 4.
  • Spring 2023: Formalization and mathematics More a hybrid math-CS course that was focused on building ability with Lean and expanding students perspectives on math and programming.
  • Spring 2023: Formalization of mathematics 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.

Patrick Kinnear (May 12 2023 at 15:26):

Also late to the party, as we just finished our course.

Course: Lean learning group 2023

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.

Reflections: 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).

Kevin Buzzard (May 12 2023 at 15:58):

A common theme on Lean-related courses in maths departments is that they seem to steer well clear of any type theory. I tell my students that a type is just what Lean calls a set, and Patrick doesn't even mention the word in his course (which is about \R and \N).

Patrick Kinnear (May 12 2023 at 16:18):

Yes, we basically said "types are like sets" in this course, which was mostly fine but we did brush up against some minor issues when we tried to formalise things which do use actual sets and not types. Not insurmountable but I think next time I'd want to think a bit more about how to say something more about types. But in the above tradition of maths Lean courses, we'll try to steer clear of mentioning them, at least to start with.

Tyler Josephson ⚛️ (May 13 2023 at 14:51):

Kevin Buzzard said:

A common theme on Lean-related courses in maths departments is that they seem to steer well clear of any type theory. I tell my students that a type is just what Lean calls a set, and Patrick doesn't even mention the word in his course (which is about \R and \N).

Is this also what folks are recommending in CS or proofs courses, or is this specific to math courses? #TPIL leads with types in chapter 2, after all

Krystal Maughan (May 17 2023 at 18:51):

I don't know if this is the right place, but I joined this Quantum Formalism group, and they're starting a Software Verification / Lean course. The repo is here: https://github.com/quantumformalism/software-verification and Benedikt Ahrens is facilitating it (we do the leg work, and we come each week with questions). It's supposed to focus on functional programming, lean and software verification (starting around May 22nd-ish?). Week 1 has already been released, reading LeanProver chapters 1-4 and working through assigned problem sets. At the end of six weeks, the goal is to work on a project, also.

Kevin Buzzard (May 17 2023 at 19:41):

What is "LeanProver chapters 1-4"? Edit: looking at the web page it might be Logical Verification.

Matthew Ballard (May 18 2023 at 17:41):

What is the Zaiku Group?

Krystal Maughan (May 18 2023 at 17:46):

@Kevin Buzzard :yes: it's the Logic and Proof chapter! @Matthew Ballard it's a group I heard about through a Quantum Computing Meetup I was attending online based in the Bay area. A couple people in that Meetup study together and have been doing the Quantum Formalism workshop (see https://quantumformalism.substack.com/), and they usually have the sessions on YouTube each week: https://www.youtube.com/@ZaikuGroup/videos

Krystal Maughan (May 18 2023 at 17:48):

I joined the Quantum Computing Meetup group because we are going through (currently at Chapter 5) the Quantum Computation and Quantum Information book by Nielsen and Chuang together, but the Discord is a larger one with people who have intersecting interests in Quantum Mechanics, Category Theory and other stuff like that. I heard about the Zaiku group through that and the people seem nice so far, but I just started by signing up for the Software Verification workshop.

Martin Dvořák (Jun 08 2023 at 09:38):

I teach Lean 4 as a part of M&M, which is something like an online course for math-olympiad highschoolers:
https://cs.wikipedia.org/wiki/M%26M_(%C4%8Dasopis)

Repository here:
https://github.com/madvorak/lean-mam

README will contain links to all texts that will have been published.
It is entirely in Czech (an obscure Slavic language).

PS: Riki is the name of the fox (our mascot). Say hi to him!

Johan Commelin (Jun 28 2023 at 07:21):

Thanks for providing all the data. There is now a website collecting these courses: https://leanprover-community.github.io/courses.html
In the near future, it should be added to the menu of the website.

To add a new course to this page, please PR data for the course to https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/data/courses.yaml

Johan Commelin (Jun 28 2023 at 07:22):

cc @Phil Wood and @Bjørn Kjos-Hanssen who have been teaching with Lean afaik.
If you like the idea of having your course listed on this page, please make a PR :smiley:

Heather Macbeth (Jun 28 2023 at 15:55):

ditto @Gihan Marasingha: I think your course is also not in the list collected so far.

Bjørn Kjos-Hanssen (Jun 28 2023 at 18:26):

Johan Commelin said:

cc Phil Wood and Bjørn Kjos-Hanssen who have been teaching with Lean afaik.
If you like the idea of having your course listed on this page, please make a PR :smiley:

Thanks @Johan Commelin, request sent!

Jeremy Avigad (Jun 28 2023 at 19:39):

Should @Dan Velleman's How to Prove it With Lean (https://djvelleman.github.io/HTPIwL/) go on this list, or should we wait until the Lean Resources page is updated? (As far as I know, the materials have not yet been used for a course, but they are ready to go for that purpose.)

Johan Commelin (Jun 28 2023 at 19:41):

I think this list should be for actual courses taught in front of actual students. So HTPIwL as a resource itself should go on the page of resources / learning materials. But if someone uses it in the classroom then that course should go on this list.

Dan Velleman (Jun 28 2023 at 19:44):

HTPIwL is not quite ready to go, but it's getting close--I'm still working on the last chapter, and then there will probably be some cleaning up to do. I don't think anyone has used it in a course, but that may happen next year.

Gihan Marasingha (Jul 03 2023 at 15:40):

Heather Macbeth said:

ditto Gihan Marasingha: I think your course is also not in the list collected so far.

Thanks Heather! I think I've made a PR now.

I should also say that I've been writing up a book to go with the interactive resource and have been talking to an editor a Springer. The draft version is in Lean 3 (as that's what I've been using with my students), but I should be updating to Lean 4 over the summer. It would be great to get some feedback from the community.

Miguel Marco (Oct 08 2023 at 15:03):

I just sent a pull request with a course I am currently teaching. It is not about Lean, we just use Lean as an optional complementary tool to teach general topology. I hope it fits.

Patrick Massot (Oct 08 2023 at 15:15):

As long as the use of Lean is not infinitesimal then it fits.

Patrick Massot (Oct 08 2023 at 15:15):

Assuming the description is clear.

Patrick Massot (Oct 08 2023 at 15:16):

Could you explain whether only the instructor is using Lean or students are expected to write Lean code? Both are interesting uses, but very different.

Miguel Marco (Oct 08 2023 at 15:31):

So far I just showed some examples to the students. They are not expected to touch lean at all if they don't want to (that was something we had very clear from the beginning: the usage of lean should be totally optional). However, several students have shown interest in it, so we will do some introductory seminars. So we sill see what happens from there.

Patrick Massot (Oct 08 2023 at 15:41):

Ok, so this is similar to how Kevin Buzzard used Lean in the very beginning. This is a very valid use case. Could you add this information to your PR?

Kevin Buzzard (Oct 08 2023 at 15:53):

It's how I'm still using lean now in one of the courses I'm teaching. I'll be playing the natural number game live in lectures a week tomorrow but the students don't have to play if they don't want to

Miguel Marco (Oct 08 2023 at 16:35):

I just updated the PR.

Last updated: Dec 20 2023 at 11:08 UTC