diff --git a/data/courses.yaml b/data/courses.yaml index bfd3533ac..2d294f71f 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -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'] @@ -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