🔢 mathématiques

Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

Cet article emploie un cadre sémiotico-culturel pour analyser comment les assistants de preuve, spécifiquement Verbose Lean, fonctionnent comme des révélateurs épistémiques dans l'enseignement des mathématiques de premier cycle en reconfigurant les pratiques de démonstration et en rendant explicites les hypothèses implicites à travers la formalisation nécessaire des objets mathématiques et des étapes inférentielles.

Auteurs originaux : Carola Manolino, Cécile Ouvrier-Buffet

Publié 2026-10-21

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Carola Manolino, Cécile Ouvrier-Buffet

Article original sous licence CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Dans le monde des mathématiques universitaires, l'acte de prouver un énoncé est bien plus que la simple résolution d'un problème ; c'est une pratique culturelle. C'est une manière spécifique de penser, d'écrire et de valider des idées que les étudiants doivent apprendre lorsqu'ils passent du lycée à l'enseignement supérieur. Depuis des décennies, les éducateurs observent les étudiants lutter pour combler le fossé entre les arguments intuitifs et informels appris précédemment et les normes rigides et explicites exigées au niveau universitaire. Récemment, un nouvel outil est entré dans ce paysage : l'assistant de preuve. Ce sont des programmes informatiques conçus pour vérifier les arguments mathématiques avec une précision absolue, forçant celui qui écrit à ne laisser aucune étape inexpliquée. Si certains voient ces outils comme un moyen de rendre les mathématiques plus rigoureuses, d'autres craignent qu'ils ne puissent étouffer la créativité ou troubler les étudiants qui luttent déjà. La question n'est pas simplement de savoir si ces programmes aident ou entravent, mais comment ils changent la nature même de la façon dont une preuve est écrite et comprise.

Une équipe de chercheurs de deux universités françaises a décidé d'examiner de près cette interaction. Ils ne se sont pas contentés de demander si les étudiants apprenaient mieux ; ils ont observé comment le programme informatique remodelait le processus de pensée des étudiants. L'étude s'est concentrée sur un cours de première année où les étudiants utilisaient un type spécifique d'assistant de preuve appelé Verbose Lean. Contrairement aux langages de programmation standard qui ressemblent à du code, Verbose Lean permet aux étudiants d'écrire dans une forme contrôlée de langage naturel, ce qui donne l'impression d'être plus proche de la manière dont les mathématiciens parlent et écrivent sur papier. Les chercheurs ont observé une paire d'étudiants travaillant sur un problème classique : prouver que si une suite de nombres se rapproche de plus en plus d'une valeur positive, les nombres de cette suite doivent finir par être eux-mêmes positifs. En enregistrant les conversations des étudiants, leurs gribouillis sur papier, leur frappe au clavier et les retours de l'ordinateur, les chercheurs ont créé une carte détaillée du voyage d'une idée mathématique, de la pensée brute jusqu'au fait vérifié par l'ordinateur.

Ce que les chercheurs ont découvert, c'est que l'ordinateur ne se contentait pas de vérifier la réponse finale ; il agissait comme un miroir, révélant les hypothèses cachées que les étudiants considèrent généralement comme acquises. Dans un cours de mathématiques normal, un étudiant peut omettre de petits détails ou s'appuyer sur un « sentiment » qu'une étape est évidente. L'ordinateur, cependant, exige que chaque objet, chaque condition et chaque saut logique soit explicitement nommé et justifié. L'étude a montré que cette exigence impose une sorte de changement culturel. Les étudiants devaient traduire leurs idées fluides et intuitives en une structure rigide que la machine puisse comprendre. Ce processus n'était pas fluide. Il impliquait un va-et-vient constant entre les notes sur papier des étudiants, leurs paroles prononcées, les messages d'erreur de l'ordinateur et les explications de l'enseignant.

Les chercheurs ont suivi une expression mathématique spécifique qui apparaissait tout au long du travail des étudiants. Au début, les étudiants traitaient cette expression comme un nombre utile pour leur raisonnement. Cependant, lorsqu'ils ont tenté de la taper dans l'ordinateur, le programme l'a rejetée. L'ordinateur n'a pas dit que le nombre était mathématiquement faux ; il a dit que le nombre n'était pas au bon endroit. Les étudiants avaient essayé de l'utiliser comme une étiquette pour une position dans une suite, mais l'ordinateur avait besoin d'un nombre entier pour ce rôle, alors que leur expression était une fraction. Ce moment fut un tournant. Cela a forcé les étudiants à réaliser que, dans le monde de l'assistant de preuve, le rôle qu'un nombre joue est aussi important que le nombre lui-même. Ils ont dû repenser leur stratégie, déplaçant l'expression d'une partie de leur argument à une autre, là où elle s'insérait enfin dans les règles strictes de l'ordinateur.

Cette difficulté n'a pas été résolue par l'ordinateur seul. L'enseignant, travaillant au tableau noir dans la même salle de classe, a dessiné un diagramme pour expliquer le concept visuellement. Il a décrit une « fenêtre » de taille qui aidait les étudiants à comprendre pourquoi leur nombre devait être plus petit que la valeur cible. Cette explication visuelle, combinée au rejet de leur première tentative par l'ordinateur, a aidé les étudiants à réorganiser leurs pensées. Ils ont fini par réaliser que le nombre avec lequel ils se battaient n'était pas la position dans la suite, mais la taille de l'écart qu'ils devaient mesurer. Une fois ce changement opéré, l'ordinateur a accepté leur argument. La preuve finale n'était pas une ligne droite de l'idée vers la solution ; c'était un voyage complexe où la signification d'un symbole unique changeait selon qu'il était parlé, écrit sur papier, expliqué par un enseignant ou vérifié par une machine.

L'étude suggère que les assistants de preuve agissent comme des « révélateurs épistémiques », un terme utilisé par les auteurs pour décrire des outils qui rendent le visible visible. Ils révèlent les « non-dits » des mathématiques — les parties d'une preuve que les experts et les étudiants laissent habituellement de côté car elles semblent évidentes. Dans une salle de classe traditionnelle, ces lacunes pourraient passer inaperçues. Dans une salle de classe avec un assistant de preuve, l'ordinateur force l'étudiant à combler chaque vide, exposant les règles cachées qui régissent la validité mathématique. Les chercheurs soutiennent que cela ne signifie pas que l'ordinateur est meilleur que l'humain, ou que l'humain est meilleur que l'ordinateur. Au contraire, les deux systèmes travaillent ensemble pour créer un nouvel espace où différentes manières de concevoir la preuve entrent en collision et fusionnent.

Les conclusions indiquent que l'introduction de ces outils modifie la culture de la preuve dans l'enseignement supérieur. Il ne s'agit pas seulement d'ajouter une couche de rigueur technique ; il s'agit de reconfigurer la compréhension qu'ont les étudiants de ce que signifie « avoir raison ». L'étude montre que les étudiants n'apprenent pas simplement à écrire du code ; ils apprennent à naviguer entre différents mondes de sens. Ils doivent apprendre à traduire leur compréhension intuitive en un langage qu'une machine peut vérifier, tout en écoutant l'explication humaine de l'enseignant. Les messages d'erreur de l'ordinateur ne sont pas de simples obstacles ; ce sont des signaux qui indiquent à l'étudiant où sa compréhension est incomplète. En forçant les étudiants à rendre explicites leurs hypothèses implicites, ces outils offrent une occasion unique d'étudier comment la connaissance mathématique est construite et validée.

Enfin, l'article conclut que les assistants de preuve ne sont pas des outils neutres. Ils portent en eux des idées spécifiques sur ce qui constitue un argument valide. Lorsque les étudiants les utilisent, ils n'apprennent pas seulement les mathématiques ; ils apprennt un nouvel ensemble de règles culturelles sur la façon de penser et de communiquer. Les chercheurs suggèrent que ce changement offre un lieu privilégié pour étudier la continuité et les ruptures entre la façon dont la preuve est enseignée, la façon dont elle est pratiquée par les experts et la façon dont elle est vérifiée par les machines. Le parcours des étudiants dans cette étude, de leur confusion initiale à leur succès final, illustre que l'apprentissage de la preuve avec un ordinateur est un processus de traduction. C'est un processus où la signification d'une idée mathématique est testée, remodelée et, finalement, stabilisée à travers l'interaction de l'intuition humaine, de l'accompagnement de l'enseignant et de la précision de la machine.

Résumé technique : Les assistants de preuve au carrefour des cultures mathématiques

Problématique
L'article traite des défis épistémologiques et didactiques soulevés par l'introduction des assistants de preuve (AP) dans l'enseignement des mathématiques au premier cycle universitaire. Alors que la littérature existante évalue souvent les AP en fonction de leur capacité à faciliter ou à entraver l'apprentissage, cette étude postule que les AP fonctionnent comme des « artefacts culturels » qui incorporent des engagements épistémologiques spécifiques concernant la validité, la formalisation et l'explicitation. Le problème central est de comprendre comment l'utilisation des AP reconfigure les « pratiques culturelles de la preuve » dans l'enseignement supérieur. Plus précisément, les auteurs étudient comment la transition de la preuve mathématique « ordinaire » (souvent tolérante envers les étapes implicites) vers la preuve vérifiée par machine (exigeant une explicitation totale) crée des frictions, révèle des présupposés cachés (« non-pensés ») et nécessite une traduction à travers différents systèmes sémiotiques. L'étude interroge la manière dont ces artefacts numériques rendent visibles les normes implicites de la preuve qui passent habituellement inaperçues dans les environnements traditionnels papier-crayon.

Méthodologie
La recherche emploie une analyse sémiotico-culturelle qualitative fondée sur un cadre théorique combinant la Transposition Culturelle (Mellone et al., 2019) et la Sémiosphère de Lotman (1990).

Contexte : L'étude s'inscrit dans un cours de première année d'université (« Logique et preuves assistées par ordinateur ») au sein d'un double cursus mathématiques et informatique en France.
Outil : Les étudiants ont utilisé Verbose Lean, une interface de langage naturel contrôlé pour l'assistant de preuve Lean, conçue pour combler le fossé entre le discours mathématique ordinaire et la syntaxe formelle.
Source de données : L'analyse se concentre sur un épisode didactique unique impliquant deux étudiants (S. et M.) travaillant sur une preuve démontrant que « si une suite réelle tend vers une limite strictement positive, alors ses termes sont finalement positifs ». Les données comprennent des enregistrements vidéo/audio des interactions des étudiants, des inscriptions sur papier, du code Verbose, des messages d'erreur, ainsi qu'une correction publique parallèle de l'enseignant au tableau.
Unité d'analyse : Les auteurs définissent une « Unité d'Analyse » (UA) comme un épisode de transposition sémiotico-culturelle où un « texte » mathématique doit être transformé pour passer entre différents systèmes de validation (par exemple, de l'exploration sur papier au retour de l'AP). L'épisode a été segmenté en sept UA.
Construit clé : L'analyse se centre sur le concept de « signe-pont » — un objet mathématique (spécifiquement l'expression $l/2$ ) qui circule à travers les frontières sémiotiques, changeant de rôle, de statut et de conditions de légitimité à mesure qu'il passe du raisonnement de l'étudiant au discours de l'enseignant et à la validation computationnelle.

Contributions clés et cadre théorique
L'article apporte un nouveau prisme théorique pour analyser la preuve dans les environnements technologiques :

Les AP comme révélateurs épistémiques : Les auteurs soutiennent que les AP ne font pas qu'ajouter de la rigueur, mais agissent comme des « révélateurs épistémiques » qui rendent observables les « non-pensés » de la preuve. Ces « non-pensés » sont des hypothèses ou des étapes opérationnelles (par exemple, le rôle spécifique d'une définition, la gestion des quantificateurs) qui fonctionnent implicitement dans la preuve ordinaire mais doivent être thématisées pour une machine.
Transposition culturelle et sémiosphère : En articulant la transposition culturelle avec la sémiosphère, l'étude traite la classe comme un espace sémiotique hétérogène où coexistent et interagissent plusieurs cultures de la preuve (pratiques du secondaire, pratiques de recherche universitaire, didactique institutionnelle et vérification computationnelle).
Le signe-pont : L'article opérationnalise le « signe-pont » pour suivre la transformation du sens mathématique à travers les frontières. Il démontre que la pertinence mathématique d'un signe ne garantit pas sa validité formelle ; le signe doit être re-fonctionnalisé pour occuper le rôle structurel correct au sein de la logique de l'AP.

Résultats
L'analyse des sept Unités d'Analyse (UA) concernant l'expression $l/2$ révèle les dynamiques suivantes :

Exploration initiale (UA1-2) : Les étudiants traitent initialement $l/2$ comme une quantité mathématiquement prometteuse sur papier. Lorsqu'ils tentent de l'utiliser dans Verbose comme témoin d'un nombre naturel ( $N$ ), l'AP le rejette en raison d'une erreur de type (réel vs nombre naturel). Cela souligne la distinction entre utilité mathématique et rôle formel.
La définition comme opérateur (UA3) : Les étudiants peinent à passer d'un traitement de la définition de la convergence comme un texte statique à copier, à un traitement de celle-ci comme un opérateur qui doit être spécialisé avec des paramètres spécifiques pour générer de nouveaux éléments de contexte.
Médiation institutionnelle (UA4) : La correction publique de l'enseignant introduit une métaphore de la « fenêtre » (visualisant la limite sur une droite réelle) et coordonne explicitement le choix de $l/2$ avec la définition de la convergence. Ce discours agit comme une ressource sémiotique institutionnelle disponible dans la sémiosphère de la classe.
Re-fonctionnalisation (UA5-6) : Les étudiants construisent initialement une structure de preuve utilisant $l$ comme paramètre, ce qui échoue à produire une positivité stricte. Finalement, ils re-fonctionnalisent $l/2$ , passant de son rôle rejeté de témoin ( $N$ ) au rôle correct de paramètre réel positif ( $\epsilon$ ) utilisé pour spécialiser l'hypothèse de convergence.
Redistribution de la validation (UA7) : La preuve finale n'est acceptée qu'après que la chaîne algébrique a été localement justifiée étape par étape pour l'AP. La validation est montrée comme étant distribuée : elle repose sur l'exploration de l'étudiant, le discours institutionnel de l'enseignant, les définitions mathématiques et, enfin, la vérification computationnelle.

Signification et affirmations
L'article affirme que l'introduction des AP reforme fondamentalement l'épistémologie de la preuve dans l'enseignement supérieur en :

Révélant les pratiques implicites : Les AP forcent les étudiants à rendre explicites les objets, les types, les quantificateurs et les étapes inférentielles qui sont souvent implicites dans les preuves « ordinaires », exposant ainsi les « non-pensés » de la pratique mathématique.
Redistribuant la validation : L'étude démontre que la validité dans un environnement médiatisé par un AP n'est pas un état binaire atteint à la fin, mais un processus distribué impliquant plusieurs autorités (étudiants, enseignants, normes institutionnelles et la machine).
Soulignant la friction de traduction : La recherche montre que la transition entre les cultures de preuve n'est pas une progression linéaire mais un processus complexe de traduction où les signes doivent changer de statut. Le concept de « signe-pont » permet aux chercheurs d'observer là où ces traductions réussissent ou échouent.
Conclusion modeste : Les auteurs ne prétendent pas que les AP améliorent automatiquement l'apprentissage ou que les étudiants intègrent de manière fluide le discours de l'enseignant aux exigences formelles. Ils soulignent plutôt que si les AP rendent les pratiques culturelles visibles, le « non-alignement » entre le discours de l'enseignant et l'activité de l'étudiant au sein de l'AP demeure un défi structurel. L'étude appelle à un changement de focus de la recherche, passant de l'évaluation de l'efficacité des AP à la compréhension de la manière dont ces outils reconfigurent fondamentalement l'enseignabilité et l'épistémologie de la preuve mathématique.

Articles similaires