Formalising Mathematics 2023

website repo
instructor
Kevin Buzzard
location
Imperial College London
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.

Interactive Theorem Proving

website repo pdf
instructor
Jeremy Avigad
location
Department of Mathematical Sciences, Carnegie Mellon University
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.

Logic and Mechanized Reasoning

website 1 website 2 repo pdf
instructor
Jeremy Avigad
location
Department of Computer Science, Carnegie Mellon University
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.

Logic and Proof

website pdf
instructor
Jeremy Avigad
location
Department of Philosophy, Carnegie Mellon University
tags
introduction to logic, introduction to proof
summary
This is an introduction to logic and mathematical reasoning for a general audience.

Proofs and Programs

website repo docs
instructor
Jeremy Avigad
location
Department of Mathematics, Indian Insititute of Science, Bangalore
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.

Theorem Prover Lab -- Applications in Programming Languages

repo website
instructor
Jakob von Raumer
location
Faculty of Informatics, KIT
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.

Discrete Mathematics

website repo
instructor
Heather Macbeth
location
Fordham University
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!"

Complement to general Analysis/Algebra 1st year undergraduate course

website repo
instructor
Frédéric Tran Minh
context
Esisar engineering school, 1st year students, 6 x 1,5h
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

Logique et démonstrations assistées par ordinateur

website repo
instructor
Patrick Massot
tags
intro to proofs, analysis, natural language input
notes
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.

Lean learning group 2023

website
instructor
Patrick Kinnear
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).