List of Lean (university) courses

Stream: general

[Gabriel Ebner]

Do we have a list of courses using Lean somewhere? I've tried to collect courses from the last year, and there's more than I thought! And I probably missed half of them, can you help me complete the list (or point me to a canonical source)? So far I've got:

• Logical Verification (VU Amsterdam)
• Formal Proof and Verification (Brown)
• Logic and Mechanized Reasoning (CMU)
• Introduction To Proofs (John Hopkins University)
• HNRS: Transition to Advanced Mathematics (University of South Carolina)
• Formalising Mathematics (Imperial College London)

[Kevin Buzzard]

@Patrick Massot certainly teaches something in Paris Saclay. I'm teaching a graduate course right now called " formalising number theory and geometry" (for graduate students at Imperial, Oxford, Warwick, Swansea, Bristol and Bath) but this is just a one off, not a regular event. My understanding was that @Phil Wood was teaching something at Harvard this semester.

[Gabriel Ebner]

Thank you for the pointers! Patrick's course was 1.5 years ago, and from what I can tell Phil Wood's course is in spring 23, so they didn't fit my list.

[Julian Külshammer]

Justin Pearson and I taught a one off non-regular thing at Uppsala University called "Summer Maths&IT Camp: Interactive theorem proving in Lean" this June, not sure whether it fits your list.

[Kevin Buzzard]

If you're also interested in workshops I ran a week long undergraduate workshop this summer (Sept) and also a two month long undergraduate summer research program (July and August)

[Sebastian Ullrich]

• Theorem prover lab: applications in programming languages (KIT) https://github.com/IPDSnelting/tba-2022

[Riccardo Brasca]

@Antoine Chambert-Loir and myself are going to teach a Lean related short course at Université Paris Cité, but we still have to figure out the details.

[Anne Baanen]

We also use Lean at Logic and Modelling at the VU (See https://studiegids.vu.nl/en/Bachelor/2020-2021/computer-science/X_401015 except the certificate is expired)

[Alex J. Best]

We also taught a project course at the VU in the mathematics department on Computer Assisted Proofs with Lean as one of the components, https://studiegids.vu.nl/en/Bachelor/2021-2022/mathematics/XB_0039#/ (roughly 20-25 students, and at least one group of 5 did a lean project full time for 3 weeks).

[Phil Wood]

Yep---my course is going to be in Spring 2023, and I am planning to follow the book Mathematics in Lean. Great to see a list here of other courses that are going on!

[Matthew Ballard]

@Mike Shulman what semester is your course?

[Anatole Dedecker]

Gabriel Ebner said:

Patrick's course was 1.5 years ago

Maybe I misunderstood you here, but Patrick is still doing his course each spring semester. So indeed there is no course going on right now, but there was this year and there will be next year

[Patrick Massot]

Gabriel Ebner said:

Thank you for the pointers! Patrick's course was 1.5 years ago, and from what I can tell Phil Wood's course is in spring 23, so they didn't fit my list.

My course happens every year from January to April.

[Mike Shulman]

I'm teaching a course right now using Lean at the University of San Diego, called "Logic and Formal Methods in Mathematics and Computer Science".

[Sebastian Ullrich]

This is an impressive list, we should put them on a map or something!

[Siddhartha Gadgil]

In January 2023 I will teach "Proofs and Programs" at the Indian Institute of Science with @Navin Goyal based largely on Lean

[Jireh Loreaux]

I taught a one-off course over the summer called "Formal verification in mathematics"

[Matthew Ballard]

An entry in the Community tab on the webpage for "Courses using Lean" would be a good idea if we are collecting this information.

[Patrick Massot]

We talked a lot about having such a page, and we even had some people volunteering to create and maintain this page, but those people seem very busy with other things.

[Matthew Ballard]

Other than a list of links is there anything people would want?