Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update courses.yaml #445

Open
wants to merge 3 commits into
base: lean4
Choose a base branch
from
Open

Update courses.yaml #445

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f4ee60d
Update courses.yaml
jnarboux Mar 1, 2024
0c52bf2
Update courses.yaml
jnarboux Mar 2, 2024
b0e6454
Update courses.yaml
jnarboux Mar 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions data/courses.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unfortunately this requires login into your moodle.

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
Expand Down