Recrutement d’un.e post-doctorant.e / ingénieur.e de recherche
dans le cadre du projet ANR “APPAM” (2024-2028)
appam.icube.unistra.fr
Les assistants de preuve pour les apprentissages mathématiques
Diagnostiquer, analyser, concevoir, expérimenter, évaluer.
Présentation résumée du projet APPAM
La preuve est constitutive de l’activité mathématique. Elle est une composante caractéristique de son épistémologie. Fondamentale à tous les niveaux de la scolarité et de la formation, elle contribue de manière significative aux processus d’apprentissage des connaissances mathématiques. Les enquêtes internationales à grande échelle montrent qu’elle occupe une place trop marginale dans l’enseignement, à tous les niveaux de la scolarité (e.g. TIMSS), avec une formation des enseignants insuffisante voire inadéquate. La rupture entre le secondaire et le supérieur, constatée par les didacticiens à l’échelle internationale, est marquée par un changement d'exigences et de rapport aux objets et processus de preuve, plus complexes et plus formels, qui nécessite une acculturation aux pratiques des mathématiciens. Les étudiants eux-mêmes se sentent en grande difficulté avec la logique et le formalisme requis pour concevoir des preuves et écrire des démonstrations. Les nouvelles technologies influencent les pratiques des mathématiques et créent de nouvelles dynamiques apportées par l’usage d’outils informatiques, reflétant la réalité du travail sur la preuve des mathématiciens contemporains. La nécessité de développer de nouvelles approches de l’enseignement de la preuve prenant en compte les assistants de preuve est démontrée depuis peu. Ceux-ci transforment le rapport épistémologique à la preuve et la structure des démonstrations, les exemples les plus connus étant la vérification du Théorème des 4 couleurs ou de la Conjecture de Kepler. Les assistants de preuve (Coq, L∃∀N, Isabelle etc.) utilisés par les mathématiciens sont des logiciels libres open-source vérifiant mécaniquement une démonstration. Utilisés parfois dans certaines universités dans l’enseignement des fondements théoriques de l’informatique, ils sont exploités depuis peu dans l’enseignement des mathématiques, éventuellement avec des interfaces graphiques (D∃∀DUCTION & Edukera pour Lean et Coq) : ils interrogent directement mathématiciens et didacticiens sur la manière dont les processus de preuve pourraient être enseignés aujourd’hui.
Le projet APPAM a ainsi pour ambition de combler le manque avéré de recherches en France sur l’apprentissage de la preuve à la transition secondaire-supérieur avec une approche pluri et interdisciplinaire (combinant outils, résultats et méthodes des sciences et des SHS) pour développer et évaluer une nouvelle approche de l’enseignement de la preuve en mathématiques fondée sur l’adaptation et l’intégration d’assistants de preuve en début d’université.
Trois objectifs le structurent :
Diagnostiquer les difficultés des apprenants et usages existants des assistants de preuve en France ;
Analyser les assistants de preuve dans une perspective d’apprentissage en mathématiques ;
Expérimenter et évaluer les apports des assistants de preuve au début de l’enseignement supérieur dans l'enseignement des mathématiques.
Les méthodes utilisées pour atteindre ces objectifs mobilisent les cadres épistémologiques, didactiques et cognitifs sur la preuve, validés à l’international, et articulent approches quantitatives et qualitatives. Les résultats de ce projet informeront chercheurs, enseignants, formateurs, décideurs des politiques éducatives sur : les difficultés des lycéens et étudiants sur la preuve, les usages et adaptations d’assistants de preuve à des fins éducatives, l'évaluation des apports d’assistants de preuve dans l’enseignement, et préconisations didactiques pour l’enseignement de la preuve au lycée et à l’université.
Le projet APPAM regroupe 11 chercheurs en didactique des mathématiques, informatique et mathématiques, répartis sur le territoire (Ile de France, Rhône-Alpes, Strasbourg, Montpellier). Différentes expérimentations seront réalisées sur ces sites géographiques.
Travail à réaliser
Le travail de la personne recrutée sera axé sur des assistants de preuve dans une perspective d’apprentissage en mathématiques (analyse d’assistants de preuves, contributions aux expérimentations et évaluation de l’usage d’assistants de preuve et de leurs impacts au début de l’enseignement supérieur dans l’enseignement et l’apprentissage des mathématiques).
La personne recrutée participera à la construction de contenus d’enseignement de mathématiques niveau Licence en prenant en compte les spécificités des assistants de preuve étudiés dans le cadre du projet (Lean, Verbose Lean, D∃∀DUCTION, Edukera). Elle mettra en évidence des critères et une méthodologie afférente en didactique des mathématiques pour ensuite analyser :
les procédures des étudiants, aux niveaux quantitatif et qualitatif, lors de séances d’enseignements mobilisant un assistant de preuve,
et les interactions enseignant-étudiants-assistant de preuve.
La personne recrutée pourra intervenir dans certains enseignements dans lesquels s’effectueront les expérimentations. Elle contribuera au pilotage des expérimentations et au recueil de données nécessaires au projet. Les expérimentations en classe en première année de Licence seront mises en place en collaboration avec les autres membres du projet et se dérouleront sur un ou plusieurs sites géographiques.
Le travail réalisé par la personne recrutée s’articulera également avec celui de la doctorante, la thèse portant sur l’évolution des conceptions et difficultés des étudiants avant et après expérimentations avec des assistants de preuve. Une appropriation de la littérature en didactique des mathématiques (mathematics education) sur les thèmes de la preuve et de l’enseignement supérieur sera donc requise.
A partir de l’analyse des résultats des expérimentations, conduite conjointement avec des membres spécifiques du projet, des propositions d’évolution des contenus, de modalités de séances, des assistants de preuve et de leurs interfaces, ainsi que des rétroactions seront formulées.
En lien avec les expérimentations en classe en début d’université, l’extension ou l’adaptation de bibliothèques de preuves formelles existantes aux besoins de l’enseignement pourront être nécessaires. En collaboration avec les développeurs, les interfaces pour les assistants de preuve pourront être instrumentées afin de permettre la collecte de données quantitatives et qualitatives.
Environnement
Ce poste sera financé sur le projet ANR APPAM et encadré par un ou deux membres du projet en région parisienne (laboratoires de recherche : Laboratoire de Didactique André Revuz et Institut de Recherche en Informatique Fondamentale).
Des déplacements (recueils de données sur différents sites géographiques du projet, réunions de coordination, diffusion des résultats dans des conférences nationales et internationales) sont à prévoir. Ceux-ci seront financés sur le budget du projet.
Profil recherché
Une formation initiale en mathématiques et/ou informatique est requise. Un doctorat en didactique des mathématiques ou didactique de l’informatique est nécessaire. Les candidatures ayant un doctorat en mathématiques ou informatique pourront être également étudiées ; dans ce cas, une ou deux années d’expérience dans le cadre d’un contrat post-doctoral ou équivalent dans un domaine complémentaire à celui de la thèse sont bienvenues. Priorité sera donnée aux candidat.e.s ayant une expérience et/ou une formation en didactique des mathématiques et/ou une expérience concernant le développement d’interfaces pour des environnements numériques en lien avec l’enseignement et/ou dans la formalisation des mathématiques à l’aide d’assistants de preuve.
Les expérimentations seront réalisées dans le cadre d’enseignements en français. Une maîtrise de la langue française suffisante est donc nécessaire. Par ailleurs, de bonnes compétences en langue anglaise (écrit/oral) sont indispensables, en particulier pour l'appropriation de la littérature et la communication des résultats des travaux de recherche à l’international.
La personne recrutée aura à interagir régulièrement avec les autres membres du projet : autonomie, compétences développées du travail en équipe et en termes de prise d’initiative sont donc requises.
Informations complémentaires
Durée de contrat : 12 mois
Date de début de contrat : septembre 2025 (date exacte à déterminer avec la personne recrutée)
Rémunération brute mensuelle en fonction de l’expérience de la personne recrutée (entre 2270 euros et 3000 euros environ).
Pour postuler
Merci d'adresser votre dossier de candidature (CV détaillé + lettre de motivation + thèse) par mail à : Cécile Ouvriet-Buffet
Date limite de réception des candidatures : 1er juin 2025
Procédure de recrutement : sélection des candidatures sur dossier puis entretien des personnes sélectionnées (visioconférence possible).