From f4ee60d2e184a25a670dd70cd17cb47007b7c12a Mon Sep 17 00:00:00 2001 From: Julien Narboux Date: Fri, 1 Mar 2024 15:55:04 +0100 Subject: [PATCH 1/3] Update courses.yaml Add experiment in Strasbourg --- data/courses.yaml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/data/courses.yaml b/data/courses.yaml index c73936f79e..8d4a1dfd21 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 student in maths and computer-science. 10 hours of lab sessions. + We used Deaduction with three groups and Lean-Verbose 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 From 0c52bf2c49ed4fea163987e5affba81eef6d31b9 Mon Sep 17 00:00:00 2001 From: Julien Narboux Date: Sat, 2 Mar 2024 20:21:13 +0100 Subject: [PATCH 2/3] Update courses.yaml Co-authored-by: Patrick Massot --- data/courses.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/data/courses.yaml b/data/courses.yaml index 8d4a1dfd21..088358c124 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -53,7 +53,7 @@ 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 student in maths and computer-science. 10 hours of lab sessions. + 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 Lean-Verbose 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 From b0e64543a25162b7891f31c619afc7afb1211d68 Mon Sep 17 00:00:00 2001 From: Julien Narboux Date: Sat, 2 Mar 2024 20:21:28 +0100 Subject: [PATCH 3/3] Update courses.yaml Co-authored-by: Patrick Massot --- data/courses.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/data/courses.yaml b/data/courses.yaml index 088358c124..5c8cfea132 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -54,7 +54,7 @@ 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 Lean-Verbose with three other groups (and Edukera with another group). This experiment is part of the french ANR project APPAM. + 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