Skip to content

Commit

Permalink
add Lean course (#552)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn authored Nov 21, 2024
1 parent 7049892 commit 37cdd8f
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion data/courses.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
year: 2024
lean_version: 4
summary: >
Students learn to formalize mathematics in Lean, including: implementation of definitions,
Students learn to formalize mathematics in Lean, including: implementation of definitions,
encoding propositions, using tactics, and developing mathematics formally. The seminar follows
the first six chapters of MIL, and culminates in a project.
tags: ['mathematics', 'beginner']
Expand Down Expand Up @@ -506,6 +506,15 @@
lean_version: 4
summary: >
This is a small seminar for master math students that took the previous Lean course and want to continue. It is a collaborative project where the students formalize some new results in analysis, this the aim to PR this to Mathlib, or make it somewhat Mathlib-ready. The topic is fourier analysis, in particular Plancherel's theorem, the interpolation theorems and their applications.
- name: Formalized Mathematics in Lean
instructor: Floris van Doorn
institution: University of Bonn
repo: https://github.com/fpvandoorn/LeanCourse24
tags: ['mathematics', 'advanced']
year: 2024
lean_version: 4
summary: >
Very similar to the course a year before, and in both cases roughly 20 students attended. Using the material from Mathematics in Lean, but mostly using my own exercises, hosted in the GitHub repository. Students will again choose a formalization project and give a presentation about the formalization.
- name: Taller de Lean 4
instructor: Enric Cosme Llópez
institution: Universitat de València
Expand Down

0 comments on commit 37cdd8f

Please sign in to comment.