# Instrumentation de l'association de registres sémiotiques dans un assistant de preuve

Emmanuel Beffara, Martin Bodin, Nadine Mandran, Rémi Molinier

► To cite this version:

Emmanuel Beffara, Martin Bodin, Nadine Mandran, Rémi Molinier. Instrumentation de l'association de registres sémiotiques dans un assistant de preuve. EIAH2023 - 11ème Conférence sur les Environnements Informatiques pour l'Apprentissage Humain, Association des Technologies de l'Information pour l'Éducation et la Formation, Jun 2023, Brest, France. pp.1-5. hal-04096240

HAL Id: hal-04096240

https://hal.science/hal-04096240

Submitted on 12 May 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Instrumentation de l'association de registres sémiotiques dans un assistant de preuve

Emmanuel Beffara<fnref n="1" />, Martin Bodin<fnref n="2" />, Nadine Mandran<fnref n="1" />, and Rémi Molinier<fnref n="3" />

**Résumé** Les assistants de preuve sont des outils informatiques conçus pour accompagner l'écriture de démonstrations mathématiques formalisées et leur utilisation pour l'enseignement de la preuve fait l'objet de diverses expérimentations en université. Leur mode d'interaction se limite habituellement au registre textuel, à l'opposé de la pratique courante sur papier qui exploite souvent différents registres visuels. Ce travail propose la conception et l'évaluation d'un prototype d'interface qui permette d'associer des registres textuels et visuels pour améliorer la flexibilité de l'outil et faciliter l'apprentissage de la preuve en mathématiques.

**Mots-clefs** : enseignement des mathématiques · registres sémiotiques · instrumentation · assistant de preuve

## 1 Introduction

La preuve mathématique est un objet d'un haut niveau d'abstraction dont l'acquisition est un enjeu d'enseignement majeur à l'entrée à l'université. La didactique met en évidence le rôle crucial de l'articulation entre les différents rôles qu'elle joue [8] : au delà de la validation des assertions (vérification, explication), la preuve a un rôle de communication (présentation systématique des résultats et transmission à une communauté) et elle intervient dans le processus de recherche (exploration des conséquences d'une hypothèse, élaboration de conjectures, découverte de résultats). À chaque rôle correspondent des savoir-faire différents, ce qui fait de la preuve un objet dont la compréhension et l'enseignement restent difficiles. De plus, au passage du secondaire à l'université correspond un saut dans le niveau d'exigence formel quant à la production de démonstrations, avec un passage de l'argumentation à du raisonnement essentiellement déductif [1].

Au vu de ces difficultés, il est naturel de vouloir instrumenter la preuve comme on instrumente d'autres objets fondamentaux des mathématiques. En effet, calculatrices, tableurs, traceurs de courbes, logiciels de géométrie ou de calcul formel sont présents en classe et intégrés aux usages. Des assistants de preuve, logiciels dédiés à l'élaboration interactive de démonstrations, ont été développés depuis la fin des années 1960, initialement pour la recherche. Ils visent principalement des experts, mais le besoin d'élargir le public visé a conduit au développements d'assistants (cf. Mizar, CalcCheck) dont la syntaxe est lisible par des mathématiciens qui ne connaissent pas l'outil.

Après des premières expériences dans les années 2000 [16,4], l'intégration d'assistants de preuve dans l'enseignement supérieur est expérimenté depuis quelques années

<footnote n="1">¹ Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, 38000 Grenoble, France</footnote>

<footnote n="2">² Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France</footnote>

<footnote n="3">³ Univ. Grenoble Alpes, CNRS, Institut Fourier, F-38000 Grenoble, France</footnote>
dans différentes universités [10]. On observe généralement un meilleur engagement des étudiants dans la recherche de preuve avec l'outil que dans une modalité classique sur papier, ce qui s'explique notamment par la présence de rétroactions immédiates, et la facilitation du tâtonnement. Les assistants de preuve semblent favoriser l'utilisation correcte de la logique et du symbolisme mais peuvent aussi conduire les étudiants vers de la preuve très formelle, renforçant les aspects syntaxiques au détriment du sens. En effet, du fait de leur grande technicité, ces outils peuvent faire obstacle à l'apprentissage des notions visées, au risque que l'enseignement instrumenté par assistant de preuve devienne un enseignement de l'outil et de ses spécificités plutôt que de la preuve mathématique en tant que telle. Face à ce problème, plusieurs outils (cf. Edukera, DΞVduction) ont été conçus en simplifiant l'interface proposée à l'étudiant, au prix d'une limitation des possibilités offertes en termes de démonstration.

Une autre difficulté est liée à l'écart entre la pratique courante de la preuve et le cadre formel imposé par les assistants. Dans la pratique experte, la preuve exploite souvent des changements de registre sémiotique [6] avec l'emploi de figures, schémas, diagrammes, etc. Chaque registre a ses règles et conventions propres qui en font un outil de compréhension et de communication et l'association de différents registres enrichit la compréhension en variant les représentations d'un même objet. Dans l'enseignement, l'articulation entre le schéma et la preuve textuelle est centrale, dès le collège avec la géométrie, puis au lycée avec par exemple l'emploi de courbes ou de tableaux, puis à l'université dans différentes branches des mathématiques. L'utilisation pertinente des différents registres fait donc partie des enjeux de l'enseignement des mathématiques.

Pourtant, en dehors de la géométrie où le registre visuel est intrinsèque à l'objet d'étude, les assistants de preuve sont généralement focalisés sur la production de démonstrations purement textuelles, sous forme de programmes (pour les outils experts) ou de rédactions idéalisées (pour les outils à visée pédagogique) et les registres visuels restent alors au brouillon et à la charge de l'apprenant, sans statut explicite au sein de la preuve. Dans l'optique d'une instrumentation de l'apprentissage de la preuve, il semble donc important de prendre en compte cette nécessaire association de différents registres.

## 2 Travaux connexes

En géométrie, où la dimension visuelle est inhérente au sujet, beaucoup de travaux ont été menés en EIAH et en didactique, depuis l'introduction de la géométrie dynamique [11] où la préoccupation pour la preuve a conduit à la réalisation de micro-mondes pour le raisonnement géométrique [12]. Des travaux plus récents ont formalisé la géométrie euclidienne dans des assistants de preuve et fourni des interfaces exploitant des outils existants de géométrie dynamique [7,13]. En dehors de la géométrie, peu de développements exploitent l'association de différents registres. Des expériences existent, comme ProofWeb [9] qui affiche la preuve en cours sous forme d'arbre de dérivation (cf Figure 1) ou Alectryon [14] qui permet de représenter visuellement des objets manipulés par l'assistant de preuve Coq [17], ce qui permet d'incorporer des éléments graphiques dans l'affichage au lieu de notations lourdes ou inhabituelles.

Ces éléments viennent en support visuel, afin de mieux comprendre l'état interne de l'assistant de preuve : il est toujours nécessaire d'utiliser des commandes textuelles
pour interagir. En cela, ces approches ne changent pas radicalement le registre utilisé pour l'interaction avec l'outil.

La communauté Coq s'est montrée intéressée par ces différents outils, même en mettant de côté leur intérêt pédagogique. En effet, ajouter un support graphique (même partiel) aide à mieux communiquer sur des résultats certifiés. De plus, certains domaines s'appuient naturellement sur des diagrammes, et ce support pourrait faciliter le développement des bibliothèques associées (notamment en théorie des catégories [3]).

## 3 Proposition de contribution

Notre premier objectif est de construire un prototype pour assister l'enseignement de la preuve en exploitant l'articulation entre plusieurs registres. Une attention particulière est portée sur l'objectif de faire de l'assistant de preuve un instrument d'apprentissage appropriable par l'étudiant, dans un mécanisme de genèse instrumentale [15]. Nous nous basons pour cela sur la Théorie des situations didactiques [5] et notamment le modèle cKc [2] qui vise à l'opérationnaliser : ce cadre permet d'identifier les caractéristiques de l'EIAH en tant que milieu et les variables didactiques qu'elles induisent (complexité des raisonnements nécessaires, possibilités d'interaction, degré d'automatisation, etc.) et par la suite permettra une modélisation des connaissances de l'apprenant par l'analyse des stratégies de résolution qu'il adpote. En conséquence, un second objectif est de valider la pertinence de ces modèles dans le contexte particulier des assistants de preuve.

Dans cette première version, nous concevons une implémentation avec Coq des tableaux de variation (voir Figure 2) destinée à être manipulée par des étudiants de début d'université. Il s'agit d'une représentation visuelle d'un ensemble d'assertions logiques associées à une méthode de démonstration, l'agencement de l'information dans le tableau est porteur de sens et sa construction guide et structure le raisonnement. Par ailleurs, il fait partie de la pratique courante au sortir du lycée, ce qui permet de s'appuyer sur un savoir-faire existant chez les étudiants.

L'outil envisagé permettra de naviguer librement entre le registre visuel du tableau, où l'étudiant peut dialoguer avec l'assistant dans une interface graphique, et le registre textuel habituel de l'assistant. On peut alors envisager un spectre d'utilisations de l'outil, du purement graphique (avec restitution éventuelle d'une preuve écrite) au purement textuel (où l'outil produit une illustration graphique évoluant à chaque étape). La Figure 3 illustre ainsi deux interactions possibles : des conjectures associées à des preuves textuelles, ou une interaction purement graphique avec des étapes de raisonnement.

## 4 Méthode de conduite de la recherche

Nous conduisons nos recherches selon les principes du Design-Based Research [18] ainsi que les guides associés (citation d'auteur). Cette méthode propose, entre autres, de construire les connaissances et les outils associés de manière itérative en intégrant les acteurs du terrain. Ainsi, nous organiserons des focus-groups avec des étudiants pour évaluer le prototype et ensuite nous mènerons des études in situ en début de cycle à l'université. Nous nous interrogerons sur l'utilisabilité de l'outil, l'engagement des étudiants dans cette activité et leur utilisation de l'association des registres. Les
premiers résultats attendus sont une version du prototype et les avis des étudiants ayant participé au focus-group.

Références

1. Balacheff, N. : L'argumentation mathématique, précurseur problématique de la démonstration. In : XXVIe Colloque CORFEM. Strasbourg, France (Jun 2019)

2. Balacheff, N., Margolinas, C. : cK¢ Modèle de connaissances pour le calcul de situations didactiques. In : XIIᵉ école d'été de didactique des mathématiques. p. 1. La Pensée Sauvage éditions (Aug 2003)

3. Behr, N. : ANR CoREACT. https://coreact.wiki/

4. Blanc, J., Giacometti, J., Hirschowitz, A., Pottier, L. : Proofs for freshmen with Coqweb. In : International Workshop on Proof Assistants and Types in Education (2007)

5. Brousseau, G. : Théorie des situations didactiques. La Pensée Sauvage, Grenoble (1998)

6. Duval, R. : Registres de représentation sémiotique et fonctionnement cognitif de la pensée. Annales de didactique et de sciences cognitives 5, 37-65 (1993)

7. Guilhot, F. : Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée. Techniques et sciences informatiques 24(9), 1113-1138 (Nov 2005). https://doi.org/10.3166/tsi.24.1113-1138

8. Hanna, G. : Proof, Explanation and Exploration : An Overview. Educational Studies in Mathematics 44(1/2), 5-23 (2000). https://doi.org/10.1023/A:1012737223465

9. Hendriks, M., Kaliszyk, C., van Raamsdonk, F., Wiedijk, F. : Teaching logic using a state-of-the-art proof assistant. Acta Didactica Napocensia 3(2), 35-48 (2010)

10. Kerjean, M., Le Roux, F., Massot, P., Mayero, M., Mesnil, Z., Modeste, S., Narboux, J., Rousselin, P. : Utilisation des assistants de preuves pour l'enseignement en L1. Gazette de la Société Mathématique de France 174 (Oct 2022)

11. Laborde, C., Capponi, B. : Cabri-géomètre constituant d'un milieu pour l'apprentissage de la notion de figure géométrique. Recherches en didactique des mathématiques 14(1.2), 1-15 (1994)

12. Luengo, V. : Analyse et prise en compte des contraintes didactiques et informatiques dans la conception et le développement du micromonde de preuve Cabri-Euclide. Sciences et Techniques Educatives 6(2), 27 (1999)

13. Pham, T.M., Bertot, Y. : A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. Electronic Notes in Theoretical Computer Science 285, 43-55 (Sep 2012). https://doi.org/10.1016/j.entcs.2012.06.005

14. Pit-Claudel, C. : Untangling mechanized proofs. In : Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering. pp. 155-174. ACM, Virtual USA (Nov 2020). https://doi.org/10.1145/3426425.3426940

15. Rabardel, P. : Les Hommes et Les Technologies; Approche Cognitive Des Instruments Contemporains. Armand Colin (1995)

16. Raffalli, C., David, R. : Computer Assisted Teaching in Mathematics. In : Workshop on Thirty Five Years of Automath. Edinburgh (2002)

17. The Coq development team : Coq (1989)

18. Wang, F., Hannafin, M.J. : Design-based research and technology-enhanced learning environments. Educational Technology Research and Development 53(4), 5-23 (Dec 2005). https://doi.org/10.1007/BF02504682
<figure><img src="image_2.png" /><figcaption>FIGURE 1 – L’interface de ProofWeb [9], qui affiche l’arbre de preuve (en bas à droite) lors de la construction textuelle de la preuve (à gauche)</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>FIGURE 2 – Exemple de tableau de variation</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>(a) Un exemple d'interaction : émettre une conjecture qu'il faudra montrer en ligne de commande</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>(b) Autre exemple : ajouter des étapes intermédiaires de raisonnement dont la preuve par l'outil est immédiate, ce qui évite de passer par la ligne de commande</figcaption></figure>

<caption>FIGURE 3 – Différentes interactions avec l'interface envisagée</caption>