Update course list

data/courses.yaml

@@ -611,3 +611,16 @@
     About half of the course will cover standard material of mathematical logic, with an emphasis on model theory, as taught in a first-year graduate course.
     The course will be limited to graduate students in computer science and mathematics. 
     The material for the course will combine sections in the book "Theorem Proving in Lean 4" and the book "The Hitchhiker's Guide to Logical Verification", in addition to lecture notes by the instructor on model theory. 
+- name: Logique et démonstrations assistées par ordinateur
+  instructor: Patrick Massot, Valérie de Clippel, Christine Paulin
+  institution: Université Paris-Saclay
+  website: https://www.imo.universite-paris-saclay.fr/~patrick.massot/enseignement/
+  tags: ['French', 'intro to proof', 'natural language input']
+  lean_version: 4
+  summary: >
+    The main mathematical topic of this course is elementary real analysis, especially the theory of convergent sequences and continuous functions.
+    Since 2021 I use a controlled natural language for input in order to facilitate transferring Lean proofs to pen and paper proofs: the Verbose Lean library that can be found on GitHub.
+  experiences: >
+    This course really works well, and it will probably continue for a long time.
+    The idea to use controlled natural language tactics seems a lot more efficient than the native syntax to ensure students improve at pen and paper proofs.
+  year: 2025