From 37cdd8f7630ee4e8d3d9f16b9869b8cd5f3dee4f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 21 Nov 2024 15:07:45 +0100 Subject: [PATCH] add Lean course (#552) --- data/courses.yaml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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