Stage Math C2+ ≪ Du Coq aux maths ou l'art de la preuve ≫

Stage de 9h avec des élèves de seconde du lycée Joséphine Baker de Pierrefitte-sur-Seine, encadrés par Marie Kerjean, Micaela Mayero, Houda Moucine et Pierre Rousselin

Transparents introductifs de Micaela Mayero pdf
Bases de logique avec Coq source (.v) ou web
Problèmes de logique source (.v) ou web
Fonctions affines sur les nombres réels source (.v) ou web
Logique classique avec Coq source (.v) ou web

Pour utiliser ces fichiers, vous pouvez soit :

installer Coq depuis Coq platform (sur Linux, nécessite le paquet snap ou passer directement par opam) et éditer les fichiers sources donnés ci-dessous avec un éditeur de texte compatible (par exemple CoqIDE, qui est fourni avec).
éditer et exécuter directement dans votre navigateur, mais la sauvegarde et le chargement de votre travail n'est pas encore prise en charge (vous devez sauvegarder à côté ce que vous avez écrit).
copier-coller les fichiers dans le scratchpad de jscoq et vous pourrez alors sauvegarder et charger comme avec un éditeur de texte classique.