diff --git a/data/courses.yaml b/data/courses.yaml index c73936f79e..5c8cfea132 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -47,6 +47,15 @@ Mathematics in Lean with weekly homework assignments. Students have to do a small independent project at the halfway point, and a larger one at the end. year: 2023 +- name: Fondements du raisonnement + instructor: Iro Bartzia and Pierre Boutry and Julien Narboux + institution: University of Strasbourg, France + website: https://moodle.unistra.fr/course/view.php?id=1906 + lean_version: 4 + tags: ['French', 'intro to proof', 'mathematics', 'Deaduction', 'Lean-Verbose'] + summary: > This an introduction to proof course, for about 200 first year students in maths and computer-science. 10 hours of lab sessions. + We used Deaduction with three groups and Verbose-Lean with three other groups (and Edukera with another group). This experiment is part of the French ANR project APPAM. + year: 2024 - name: Démontrer avec un ordinateur instructor: Riccardo Brasca and Antoine Chambert-Loir institution: Université Paris Cité, France