Le concept de preuve dans les mathématiques d’aujourd’hui

Démontrer, prouver, vérifier, établir, ça veut dire quoi pour nos élèves ?
vendredi 8 juin 2012
par  Alain BUSSER

Ce qui a toujours été considéré comme l’essence des mathématiques, c’est la démonstration telle qu’Euclide la pratiquait, qui consistait à ramener la vérité indubitable de certains axiomes à celle des théorèmes qui en résultaient. Or, de plus en plus, ce genre d’exercices (qui se faisaient surtout en géométrie) tend à disparaître de l’enseignement des mathématiques, basé sur « problématique ». En fait, il est vrai que cette évolution accompagne celle de la recherche mathématique, les preuves obtenues par des démarches non déductives abondant au sein même de celle-ci et même depuis assez longtemps finalement.

Dans cet article, on va prouver que le pantographe ci-dessous construit bel et bien le symétrique de P par rapport à Q. Et on va le prouver de plusieurs manières.

Le pantographe en question (on peut manipuler P sous CaRMetal après téléchargement), et la trace de Q s’affiche tant qu’on ne zoome pas avec la molette de la souris) :

CarMetal - 3.4 ko
le pantographe au format CaRMetal

On va distinguer trois manières de prouver que O est le milieu de [PQ] :

  1. Par raisonnement déductif (la démonstration à la Euclide)
  2. Par le calcul (à la mode, avec la géométrie repérée et les logiciels de calcul formel)
  3. Preuve probabiliste (les interrogations qu’elle suscite, proches de celles entraînées par les CAS, restent d’actualité)

Preuve par déduction

Principe

La preuve par induction (logique), souvent pratiquée dans les sciences expérimentales, utilise comme point de départ, des faits qui sont perçus ou induits : Elle va du connu vers le moins connu, et se trouve souvent entachée d’erreurs ou de risque.

Un exemple connu :

l’erreur de Fermat :

2^{2^0}+1=3 est premier ;

2^{2^1}+1=5 est premier ;

2^{2^2}+1=17 est premier ;

2^{2^3}+1=257 est premier ;

2^{2^4}+1=65537 est premier ;

Donc 2^{2^5}+1=4294967297 est premier

En fait, Fermat avait, fidèle à son style, présenté ce résultat comme une conjecture. Son « erreur » est juste de ne pas avoir pensé à vérifier la non-divisibilité par des nombres congrus à 1 modulo 128, dont Euler a prouvé un siècle après que ce sont les seuls diviseurs possibles d’un nombre de Fermat, et la preuve d’Euler utilisait des outils mathématiques que Fermat avait à sa disposition.

Au contraire, la déduction logique part d’axiomes (qui ne sont pas perçus mais conçus) pour aller vers des théorèmes, par une construction allant vers une vérité croissante (techniquement, par une relation d’ordre dans une algèbre de Lindenbaum). Les hypothèses ne viennent donc pas de l’expérimentation mais sont des constructions logiques faites une fois pour toutes en préambule de la déduction : Sous réserve que ces axiomes soient vrais, la théorie qui en résulte l’est aussi.

Mais sont-ils vrais ?

L’histoire des géométries non euclidiennes montre que même une construction solide peut être fondée sur des bases fragiles. Les travaux de Kurt Gödel ont confirmé cette impression, notamment avec d’autres exemples comme l’axiome du choix et l’hypothèse du continu : Le point faible des mathématiques, ce sont les axiomes...

Or le travail de déduction des théorèmes à partir d’axiomes ou de lemmes, est largement mécanisable. Le projet, lancé par Leibniz vers 1700, a abouti à la création d’un langage de programmation (Prolog) puis de logiciels de démonstration automatique comme Coq (logiciel) ou Isabelle (logiciel). Parmi ces outils permettant de démontrer, voire découvrir, des théorèmes de géométrie, on ne considèrera ici que ceux qui sont interfacés avec des logiciels de géométrie dynamique (dans les onglets suivants).

L’un des premiers de ces logiciels était GeoProof, au demeurant l’un des premiers logiciels reconnaissant les formats Kig et C.a.R., mais il est « discontinué » et loin d’être multiplateforme...

Géometrix

Géometrix semble le plus ancien des logiciels de ce genre (développé en Pascal (langage) avec un moteur de déduction en Prolog), à en juger par la date de 1990 affichée sur le site. Le logiciel a été magnifiquement décrit par son auteur sur MathemaTICE dès 2006. Dans sa version de 2013 (en cours d’élaboration à l’heure où j’écris ces lignes, et hélas seulement sous Windows pour l’instant), le moteur d’inférence de Géométrix tourne en tâche de fond, ce qui lui permet d’afficher des faits déduits en temps presque réel : Au cours de la construction de la figure, les théorèmes sont produits automatiquement. Géométrix s’éloigne donc un peu de la géométrie dynamique, les conjectures n’étant pas seulement visuelles mais également suggérées par le logiciel. Pour utiliser Géométrix, on a le choix entre la version élève (qui ne fait que conjecturer) et la version professeur (qui, en plus, affiche sur demande la démonstration en Prolog de la propriété conjecturée). En effet, ce logiciel a pour but essentiel de permettre la conception d’exerciciels de démonstration en géométrie.

Donc, le plus dur pour démontrer que E est le milieu de [AF] (les noms des points ont changé par rapport à la figure ci-dessus) c’est de commencer la construction. En effet, le menu de construction des points n’a pas de point libre dans le plan :

Conseil préliminaire : Bien regarder les vidéos de tutoriels sur le site avant de commencer une activité avec Géométrix. En effet, son comportement est parfois si différent des logiciels de géométrie dynamique classiques, qu’on ne sait pas toujours comment faire, ni même ce qu’on peut faire.

Dans le cas présent, quelques tentatives ont mené à la découverte du célèbre double-clic sur la figure, qui se charge de construire un point libre, avec une suggestion de nom pour celui-ci (A puis B etc.). Pour avoir un losange, on peut placer C sur le cercle de centre A passant par B, pour garantir que AB=AC. Pour compléter le losange, on peut construire des parallèles [1] puis leur intersection :

Dès que E (milieu de [CD]) et F (symétrique de B par rapport à D) sont construits, Géométrix affiche (en bas à droite) que E est le milieu de [AF] :

(incidemment, une piste de démonstration apparaît juste au-dessus...). Pour avoir une démonstration automatique, on doit cliquer sur l’icône représentant un professeur et paramétrer le moteur d’inférence. La première entrée du menu permet de définir des restrictions (choisir des axiomes pour démontrer au niveau voulu, avec les outils connus des élèves de ce niveau) :

L’onglet « base de théorèmes » permet de choisir les théorèmes utilisables dans la démonstration à venir :

(hélas, il n’est pour l’instant pas possible de désactiver les axiomes d’Euclide et de Desargues pour explorer les géométries non euclidienne et non arguésienne ; qui a dit « tant mieux » ?). L’onglet « but » permet de choisir parmi les centaines de propositions trouvées par Géométrix, celle qu’on veut démontrer. En cliquant dessus (par exemple en l’activant), on voit la démonstration à droite de l’écran :

Plus précisément, il ramène la preuve de la conjecture à des preuves d’autres conjectures (ou « tactiques » dans le langage de Coq). Dans le cas présent, on peut traduire par « si seulement je pouvais prouver que ACFD est un parallélogramme alors comme E est déjà le milieu de la diagonale [CD], on aurait prouvé que E est aussi le milieu de l’autre diagonale ». La démonstration est alors ramenée à celle d’une autre conjecture, qu’on peut explorer en cliquant dessus dans la liste des buts possibles. Ce qui permet récursivement d’arriver à devoir démontrer des hypothèses, ce qui achève l’exercice.

JGex

JGex est un logiciel similaire à Géométrix, mais développé en Java, donc multiplateforme. L’histoire remonte apparemment à Wu Wenjun qui a découvert un algorithme pour démontrer des théorèmes analytiquement (voir ci-dessous la démonstration par le calcul) qui ressemble beaucoup à l’algorithme d’Euclide. Des étudiants, sans doute sous son impulsion, ont travaillé sur un logiciel mettant en pratique l’algorithme de Wu, et dont le nom anglais est Geometry Expert. Lors d’un séjour au Canada, ils ont réalisé JGex qui est la version Java de Gex. Puis apparemment ils sont retournés en Chine où ils ont recommencé leur travail avec le nouveau logiciel MMP, entièrement en Mandarin, et non libre. D’ailleurs JGex non plus n’est pas libre. Il n’empêche que c’est un beau logiciel (mais ses auteurs ont une orthographe anglaise très hésitante...).

Le losange n’existant pas dans le vocabulaire de JGex, on est obligé de construire un cercle. Chaque étape de la construction est ponctuée par une mise à jour de la liste des faits à gauche de la figure. Quand celle-ci est construite, on peut choisir dans le menu « to prove » le fait à prouver (ici « midpoint », en sélectionnant dans un menu déroulant les noms des points F, A et E) ; immédiatement, JGex répond que la proposition est vraie :

Ci-dessus, l’algorithme de Wu est sélectionné pour la démonstration (voir ci-dessous le résultat surprenant qu’il donne) ; en sélectionnant la déduction « GDD », on obtient automatiquement la démonstration suivante :

Comme là encore, on a une arborescence de tactiques, on lit mieux la démonstration de bas en haut :

  • point10 : BD=DE par hypothèse sur E ;
  • point 9 : F est équidistant de C et D par construction
  • point8 : le parallélisme entre (AC) et (BD) entraîne une égalité d’angles alternes-internes ;
  • point 7 : Les longueurs AC et BD, toutes deux égales à DE, sont égales entre elles ;
  • point 5 : D’après les points 7, 8 et 9, les triangles CFA et DFE sont isométriques (en fait l’isométrie en question est une symétrie centrale ce qui évite d’avoir à utiliser ce vocabulaire d’« égalité des triangles »).
  • Donc (point 6), on a deux angles (opposés par le sommet) égaux entre eux ;
  • Point 4 : donc les droites (FA) et (EF) sont parallèles (les angles pouvant être considérés comme alternes-internes) ;
  • Point 3 : D’après le point 5, FA=FE (la symétrie centrale conserve les longueurs).
  • Point 2 : Deux droites parallèles entre elles ayant un point commun sont confondues : F, A et E sont alignés
  • Enfin, point 1 : Les points 2 et 3 se résument à la propriété de milieu conjecturée.

La démonstration est plus compliquée que celle de Géométrix (plus longue, et utilise les triangles isométriques, ce qui n’était pas nécessaire). Mais il suffit de cliquer sur une proposition pour la voir codée sur la figure, avec une animation, et un lien vers la règle utilisée pour démontrer la propriété :

En cliquant sur « lemmas », on peut voir la liste des règles des axiomes utilisables pour la démonstration, parmi lesquels on retrouve l’axiome d’Euclide :

Las ! Malgré ce que laisse penser la présence d’une case à cocher, il est impossible de désélectionner un axiome, donc là aussi, les géométries non euclidiennes et non arguésienne sont exclues de JGex [2]...

DrGeoII

Le logiciel DrGeoII est écrit en Smalltalk, un langage objet d’âge similaire à celui de Prolog, et depuis des années, des tentatives pour l’interfacer avec Prolog ont été menées, y compris avec un Prolog écrit en Smalltalk. En ce moment, l’idée la plus aboutie est celle d’un système expert écrit directement en Smalltalk. Ce système expert a déjà été interfacé avec DrGeoII, mais pour démontrer autre chose que le théorème de Varignon montré dans l’exemple, il reste encore à enrichir ce système avec une collection d’axiomes plus impressionante, ce qui risque d’être long et de nécessiter de l’aide, pour l’instant encore attendue...

Mais cette possibilité d’extraire des données logiques d’une figure géométrique est déjà impressionnante, d’autant que contrairement aux logiciels précédents, la manière de faire est accessible à la lecture (dans le langage Smalltalk), les logiciels Pharo et DrGeoII étant libres.

Et puis, comme la base d’axiomes est éditable avec un fichier texte, on peut y mettre les axiomes qu’on veut, et donc explorer les géométries non arguésienne et non euclidiennes de manière purement axiomatique...

Savoir ou croire ?

En fait, le mode de fonctionnement de ces logiciels ressemble à celui de l’apprentissage : On part d’une base de connaissance (les axiomes) et on l’enrichit par déduction ; la base de connaissance grandit alors jusqu’à ce qu’on arrive à y trouver la proposition à prouver. Or il existe une théorie de la connaissance, c’est la logique épistémique. Son axiome de la connaissance Kp \Rightarrow p empêche le droit à l’erreur (il se traduit par « si je sais que p est vraie, alors p ne peut pas être fausse ») ; c’est lui qui est responsable du fait qu’au cours du temps, la quantité de connaissance ne peut que croître.

Comparaison

Modus ponens Apprentissage
Axiomes Savoir inné
Théorèmes Savoir acquis
Règles de déduction Méthodologie
Déduction Apprentissage
Asymétrie de l’implication Impossibilité de réviser les connaissances
Raisonnement inductif Croyance

Or l’intelligence ne se réduit pas à la connaissance, et se caractérise plutôt par la possibilité de remettre en question les fondements même de la connaissance (comme dit l’expression « détruire pour mieux reconstruire ») ; on a donc cherché à remplacer la logique épistémique par la logique doxastique, ou logique des croyances. La logique doxastique est une logique non monotone, qui permet la révision de croyances (on peut supprimer un fait lorsqu’on s’aperçoit que finalement on n’y croit plus, comme les coups de gomme du Sudoku quand on dit « ah ben non ça ne peut pas être un 6 finalement »).

Le cours de psychologie cognitive expérimentale de Stanislas Dehaene laisse penser que le cerveau humain (même celui du nourrisson) est structuré de manière à pratiquer l’inférence bayésienne (avec ses révisions de connaissances) plutôt que le raisonnement déductif.

Le problème P = NP quant à lui, suggère que l’intervention de l’intuition [3] (ou « trait de génie » ou « haha » comme l’appelait Martin Gardner) peut être nécessaire, par manque de temps pour l’exhaustivité du raisonnement, bien plus souvent qu’on le voudrait. En d’autres termes, certains problèmes sont peut-être tout simplement trop difficiles pour se prêter à des démonstrations par syllogismes. On peut donc s’attendre à une recrudescence des preuves probabilistes ou constructivistes dans l’avenir.

Preuve par le calcul

Intuitionnisme

La logique intuitionniste privilégie la démonstration constructive dont un aspect important est la preuve par le calcul : Quand on demande de « démontrer que f’(x)=(2x+1)(5-x) », on attend bien un calcul et pas un syllogisme.

La logique intuitionniste refuse

  1. le tiers exclu
  2. la démonstration par l’absurde
  3. l’utilisation de l’infini potentiel

La logique intuitionniste, un délire ?

Le refus du tiers exclu a mené à la création de la logique trivalente (vrai-faux-indéfini) par Jan Łukasiewicz [4] ; ainsi qu’à la disparition de la double négation. Elle rappelle donc les problèmes d’indécidabilité étudiés par Kurt Gödel : Puisqu’on sait qu’on ne peut pas tout démontrer, on fait avec, en acceptant (ou non) des axiomes indécidables comme l’axiome du choix ou l’hypothèse du continu. Et dans la lancée, on fait souvent pareil avec l’hypothèse de Riemann généralisée [5]...

Ceci dit, pour démontrer que 32 est pair, il suffit d’effectuer la division de 32 par 2 et de constater que le quotient est entier. Il y a donc quelque chose de très concret dans la logique intuitionniste.

Wu

Le logiciel JGex décrit ci-dessus permet de démontrer des théorèmes, non seulement à l’aide de moteurs d’inférence, mais aussi par le calcul formel. L’idée est de représenter chaque hypothèse par une condition algébrique, ce qui définit l’espace des propositions comme l’intersection de variétés algébriques, et enfin, démontrer que la condition algébrique qui exprime la conclusion à prouver, se ramène à un calcul algébrique. C’est l’algorithme de résolution algébrique qui diffère selon la méthode employée : Bases de Grobner, ou algorithme de Wu. JGex permet de choisir entre les deux, et ses auteurs affirment que le nombre de propositions démontrées par JGex avec l’algorithme de Wu dépasse largement celui des propositions démontrées par les bases de Grobner, et encore plus celui des propositions démontrées déductivement. En général...

Un exemple

Pour démontrer le théorème de Varignon, on peut choisir son repère de telle manière que l’espace soit de dimension deux (s’il y avait un cercle dans la construction, on aurait besoin d’un repère orthonormé ce qui amènerait à un espace de dimension 4 ou plus).

Pour montrer que IJKL ci-dessus est un parallélogramme, on peut choisir le repère affine que l’on souhaite puisque toutes les propriétés de la figure sont elles-mêmes affines, et en choisissant pour repère (B,A,C), on a les coordonnées suivantes : A(0,1), B(0,0), C(1,0), I(0,1/2) et J(1/2,0). Alors, en appelant (a,b) les coordonnées de D,

  • L’hypothèse « K(c,d) est le milieu de [CD] » se traduit par les équations 2c=1+a et 2d=b ;
  • L’hypothèse « L(e,f) est le milieu de [DA] » se traduit par les équations 2 e=a et 2f=b+1 ;

En résumé, dans l’espace de dimension 6 engendré par a, b, c, d, e et f, chaque équation (qui est linéaire dans le cas présent) restreint l’espace des configurations possibles à un hyperplan (de dimension 5), et l’intersection de deux hyperplans étant en général de dimension moindre (4), on se demande si les conditions affirmant que IJKL est un parallélogramme sont systématiquement dans cet espace. Dans le cas présent, comme le vecteur allant de I à J est de coordonnées (1/2,-1/2), et celles du vecteur allant de L à K sont (c-e,d-f), les conditions qui expriment que IJKL est un parallélogramme sont

  1. 2(c-e)=1 ;
  2. 2(d-f)=-1.

Alors la démonstration du théorème de Varignon revient à montrer que l’espace engendré par ces deux conditions (de dimension 4) est inclus dans l’espace de dimension 4 précédent. Ce qui se fait algébriquement (et facilement dans le cas présent, il suffit de calculer les coordonnées des vecteurs en fonction de a et b). Et même pour des propositions euclidiennes (concernant des angles et des cercles) le système, non nécessairement linéaire, reste soluble par le calcul formel, comme le montrent les deux onglets suivants.

Bien que JGex sache prouver que E est le milieu de [AF] avec la méthode déductive, la méthode de Wu échoue dans ce cas :

Par exemple, le point 4 donne deux équations exprimant que F est le milieu de [CD] (visiblement, les variables x11 et x12 sont les coordonnées de F) ; les équations h0 à h6 viennent d’une triangulation du système ; la suite des restes des divisions de l’algorithme d’Euclide apparaît en bas de la figure, et le dernier de ces restes n’étant pas nul, la proposition n’est pas considérée comme démontrée. En affichant le message selon lequel la proposition est fausse (alors que JGex l’affichait comme vraie), le logiciel permet de cliquer sur un bouton pour afficher le reste non nul en question.

Bien entendu, c’est vraisemblablement un bogue (une erreur de calcul formel) qui est responsable de cette affirmation erronée. Le calcul formel permet bel et bien de démontrer la proposition.

Xcas

Xcas permet de faire la figure pour conjecturer la propriété (en géométrie dynamique) mais alors, on est dans un monde numérique où les calculs sont approchés, et non dans le monde formel qui permet de prouver réellement la propriété conjecturée. Pour cela, on peut choisir un point de coordonnées (x,y) pour A et deux points B et C sur le cercle de centre A et de rayon 5 (pour avoir moins d’inconnues à l’affichage). Pour éviter d’allonger à l’excès les équations, on peut fixer, sans perte de généralité, C à la verticale de B (lignes 1 à 3 ci-dessous) :

La ligne 4 montre la syntaxe pour compléter un parallélogramme ; la ligne 5, celle du milieu, et la ligne 6, celle du symétrique. Pour terminer la démonstration que O est le milieu de [AP], on peut créer le milieu en question (Q à la ligne 7) et vérifier que ses coordonnées (formelles) sont les mêmes que celles de O, par exemple en demandant à Xcas (ligne 8) de calculer les coordonnées du vecteur allant de O à Q.

GeoGebra

En fait, dans tout cet exercice, le fait que ABDC est un losange est un distracteur. La proposition à démontrer est affine, et seul le parallélogramme est utile à la démonstration. On peut donc « démontrer par le calcul » en choisissant pour repère (A,B,C). Alors A(0,0), B(1,0) et C(0,1). L’hypothèse « ABDC est un parallélogramme » donne les coordonnées de D(1,1). Et l’hypothèse « E est le milieu de [CD] » donne les coordonnées de E(1/2,1). Enfin, l’hypothèse « B’ est le symétrique de B par rapport à D » donne les coordonnées de B’(1,2). Ces coordonnées permettent de calculer dans le repère (A,B,C) les coordonnées du milieu de [AB’] et de vérifier que c’est bien E.

Alternativement, on peut utiliser le repère orthonormé de GeoGebra (en arguant du fait que la proposition est affine) et laisser ce dernier calculer les coordonnées des points de la figure :

Ensuite, il suffit de rajouter le symétrique de A par rapport à E (que GeoGebra nomme A’) et de constater qu’il a les mêmes coordonnées que B’. En cas de doute, on peut utiliser l’outil « relation entre objets » de GeoGebra qui confirme l’égalité des deux points :

CAS, y croire ?

Fermat

Pour prouver que 2^{2^5}+1=4294967297 est composé, Euler a juste effectué la division par 641. La démonstration est constructiviste : On peut effectuer la division, on trouve 6700417 qui est entier, on a un diviseur, on a prouvé que 4294967297 n’est pas premier et que Fermat avait tort. Oui mais comment prouver que 2^{2^{20}}+1 est composé ?. Déjà, pour 4294967297, qui a refait comme Euler les calculs à la main, et qui a préféré les faire avec une calculatrice ? Doit-on faire confiance à Euler ou à la calculatrice ?

Mersenne

À l’heure où j’écris ces lignes, le plus grand nombre premier connu est 2^{43112609}-1, un nombre de Mersenne de plus de douze millions de chiffres. Pour prouver qu’il est premier, un algorithme basé sur le petit théorème de Fermat a été utilisé, et il a occupé plusieurs jours de temps de calcul sur un superordinateur cis à Grenoble. Et en plus, ce nombre est « probablement premier », le test de Lucas-Lehmer étant probabiliste. Même pour vérifier que son exposant 43112609 est premier, je n’ai personnellement pas le courage de faire les calculs à la main, et je préfère laisser un logiciel de calcul formel (ou Java) faire le travail, pas vous ?

Les mathématiques constructives sont mises à mal par ces constatations, la notion de « prouver, c’est construire » devenant progressivement celle de « prouver, c’est dire qu’on pourrait construire », et la construction elle-même se défosse sur l’ordinateur. Depuis la démonstration du théorème des quatre couleurs par ordinateur, les exemples se multiplient, où l’étape la plus longue de la démonstration se fait avec un ordinateur, parce que sa longueur la rend inaccessible à l’être humain (conjecture de Kepler, de Seifert ...). Peu de gens ont pris la peine de lire les centaines de pages qui démontrent que la classification des groupes simples sporadiques est terminée, mais tout le monde fait confiance à ceux qui ont rédigé ces pages (même si certains passages sont peut-être plus évoqués que démontrés [6]) ainsi qu’à Andrew Wiles et Grigory Perelman, qui sont plus faillibles qu’un ordinateur, mais on est de plus en plus amené à faire confiance à l’ordinateur parce qu’on ne peut pas faire autrement. Ce qui pose des problèmes nouveaux et parfois très terre-à-terre :

  • L’importance épistémologique des logiciels libres (on a encore moins confiance en l’ordinateur si on est privé de la possibilité théorique de vérifier son travail)
  • la nécessité d’accepter l’utilisation quotidienne de résultats non constructifs : Bien qu’on ne sache pas s’il existe un algorithme factorisant rapidement des nombres entiers, on utilise RSA pour les échanges bancaires, et on n’a pas la certitude que RSA est sûr, ni qu’on aura cette certitude un jour
  • Le manque de temps laisse la part belle à l’émission de conjectures et le cours de maths ressemble de plus en plus à une liste d’algorithmes (ce qu’il était d’ailleurs à ses débuts avec les ouvrages d’Âryabhata et al Khawarizmi)

Preuve probabiliste

CaRMetal

Pour montrer que le point rouge ci-dessous est bien le symétrique de A par rapport au point marron, CaRMetal utilise une méthode fréquentielle (déjà existante chez Cinderella) consistant à secouer la figure dans tous les sens pour estimer la proportion de cas où la proposition est fausse, à l’aide de l’outil de validation de conjecture appelé Monkey et déjà utilisé au premier cycle. La construction de la figure est assez rapide avec l’outil « translation » :

Pour valider l’hypothèse, on peut construire le symétrique de A par rapport au point marron et le comparer avec le point rouge, en actionnant le Monkey pour vérifier que le résultat du test ne change pas.

Mais une alternative est de créer un exercice pour automatiser ce test : Il suffit de demander la construction du point rouge comme énoncé de l’exercice, et de laisser l’outil « symétrique » disponible pour faire l’exercice « en trichant » [7].

Après ça, en cliquant sur « vérifier la construction », une barre de progression s’affiche et au bout de quelque temps, le pourcentage de cas de figure où la proposition est vraie apparaît (ou plutôt, n’apparaît pas puisqu’il est égal à 100%) :

Confiance ?

CaRMetal effectue 1000 essais, donc un intervalle de confiance à 95% a pour borne supérieure 1 (puisque une fréquence ne peut dépasser 1) et pour borne inférieure 1-\frac{1}{\sqrt{1000}}\approx 0,968 : On peut affirmer que O est effectivement le milieu de [PQ] avec une probabilité supérieure à 0,968. Autrement dit, la probabilité que O ne soit pas le milieu de [PQ] est évaluée à 0,032.

Et si l’activité est faite en réseau par un groupe de 16 élèves, en admettant l’indépendance entre les simulations des 16 élèves, la probabilité que O ne soit pas le milieu de [PQ] devient 0,032^{16}\simeq1,2\times10^{-24}.

Fermat dirait « j’ai exclu une si grande quantité de cas de non-alignement que j’aurais peine à me déduire » !

Arithmétique

Lorsqu’on demande à l’ordinateur si 12345678901234567891 est premier, il répond « probablement oui ». Le principe est de vérifier le petit théorème de Fermat sur des exemples. Par exemple, avec DrGeoII, le test de primalité de Miller-Rabin est utilisé :

Comme on estime la proportion de résultats faussement positifs inférieure à 0,25, et qu’on fait le test sur 25 valeurs indépendantes (enfin théoriquement) entre elles, on estime la probabilité que 12345678901234567891 soit composé à 0,25^{25}\simeq 8,9 \times10^{-16} qui est négligeable. En Java par exemple, le test de primalité est nommé isProbablePrime et ne donne la primalité qu’à une probabilité donnée près, laquelle est aussi proche de 1 qu’on le souhaite, mais au prix d’un temps accru à passer dessus...

Si on accepte de faire ainsi (est-ce encore des maths ?) c’est encore une fois parce qu’on n’a pas vraiment d’autre choix, mais aussi parce qu’on estime que la probabilité d’apparition d’un bogue est largement supérieure à 10^{-15}.

Polynôme d’Euler

Avec un tableur connaissant le calcul formel (en fait, le tableur, puisque seul Calc peut être muni de CMathOOoCAS) on compte que parmi les entiers n entre 1 et 100, il y en a 86 pour lesquels n²-n+41 est premier. Donc en choisissant un entier entre 1 et 100 au hasard, la conjecture « n²-n+41 est premier » est vérifiée avec une probabilité de 0,86 [8]. Et la probabilité de ne jamais avoir de nombre composé en répétant le tirage au hasard 16 fois, est environ 0,09 qui est peu : En d’autres termes, si chaque élève d’un groupe de 16 choisit un nombre au hasard n entre 1 et 100 et teste la primalité de n²-n+41, il a 91 chances sur 100 qu’au moins l’un d’entre eux infirme la conjecture.

Confiance ou méfiance ?

Lorsqu’Xcas prétend que 12345678901234567891 est premier, il ne paraît pas raisonnable de mettre en doute cette affirmation ; d’autant que ce logiciel étant libre, on peut voir comment il trouve que 12345678901234567891 est premier, en consultant la partie du code source qui se charge des tests de primalité. Mais lorsque Fermat affirmait que 4294967297 était premier, même si Fermat lui-même présentait ce résultat comme une conjecture qu’il restait à vérifier, on voit bien (depuis Euler) qu’il fallait émettre un doute sur cette conjecture.

Avant même de lire une démonstration abordable du théorème de Morley, j’avais personnellement confiance en ce résultat : C’est un théorème qui a été démontré par quelqu’un qui a l’air digne de confiance et « on voit bien » avec un logiciel de géométrie dynamique que c’est vrai. Or c’est bien par l’émission de conjectures qu’on fait découvrir les théorèmes de géométrie plane, et ceux-ci sont de plus en plus souvent admis (et présentés comme tels). Une situation analogue s’est récemment présentée avec le théorème d’Ayme dont une courte démonstration par le calcul formel a été donnée sur wikipedia anglais (en utilisant une de ces fameuses « propriétés bien connues » que je ne connaissais pas...).

Admettre un résultat sans démonstration, juste parce qu’il a l’air vrai (et l’ordinateur semble le confirmer) est pratique en cours de maths (pour aller plus vite, au risque de frustrer les meilleurs élèves). De toute manière, il est difficile de rédiger une démonstration vraiment exhaustive (quels sont les axiomes, faut-il démontrer tous les résultats intermédiaires, même ceux qui paraissent évidents ?). Les « ROC » du bac S sont des démonstrations courtes dont les hypothèses sont clairement rappelées, et portent le plus souvent sur d’autres domaines que la géométrie (typiquement, analyse ou arithmétique).

Et au bac ?

Extraits de sujets :

S Liban 2012 : « Justifier qu’il existe un unique réel α tel que g (α) = 0 ». Quel est l’attendu ? Ou bien l’élève utilise le théorème des valeurs intermédiaires et la justification prend une ligne, ou bien il ne pense pas au théorème des valeurs intermédiaires et n’arrive sans doute pas du tout à justifier l’existence de α, du moins de façon satisfaisante pour le correcteur.

ES Liban 2012 : « Montrer que la probabilité de l’évènement M est égale à 0,42 » : S’agit-il vraiment d’une démonstration ? Ne doit-on pas plutôt comprendre « Calculer la probabilité de M » ? En effet, il est clair que la réponse est donnée uniquement pour ne pas léser ceux qui n’ont pas réussi le calcul, pour la suite de l’exercice où la valeur de 0,42 est nécessaire. D’ailleurs que « démontrer » ici ? À moins d’admettre que « montrer » veut dire « montrer par le calcul »...

STG Amérique du Nord 2012 : « En déduire le sens de variation de la fonction f sur cet intervalle », alors que la question précédente portait sur le signe de f’ : Quelle « déduction » peut-elle être faite ? Que doit rédiger un élève en guise de raisonnement ? Ne suffit-il pas qu’il donne le tableau de variations en guise de « déduction » ?

Cette année, en Terminale STG, je disais à mes élèves que les verbes « démontrer », « montrer », « vérifier », « déduire », « justifier » veulent tous dire « expliquer pourquoi » ; l’explication devant évidemment être rédigée sur la copie, même si elle ne fait qu’une phrase. Le texte « tout trace de recherche etc » précisant juste un besoin de rédaction supplémentaire. Donc

  • Une « ROC » (quelle « connaissance » restitue donc l’élève ?) est une démonstration par la déduction, à la Géométrix (mais en moins exhaustif)
  • Les autres « montrer » etc. seraient plutôt des preuves par le calcul (éventuellement formel, éventuellement à la calculatrice, en témoignent les questions sur la droite de régression par la méthode des moindres carrés, qu’il est délirant d’exiger par un autre moyen que la calculatrice ; c’est bien la capacité de l’élève à utiliser la calculatrice qui est évaluée, pas son talent pour les maths).
  • La preuve probabiliste n’est pour l’instant pas encore demandée au bac, mais les inévitables questions sur la statistique inférentielle iront dans ce sens.

[1ou depuis peu, utiliser l’outil de construction de parallélogrammes

[2à moins de « dézipper le jar » pour modifier le fichier texte contenant les règles mais cette manip s’apparente à de l’ingéniérie inverse, dont l’absence de licence libre laisse douter de la légalité.

[3le « N » de « NP » veut dire « non-déterministe »

[4Cette logique trivalente est à l’origine de la logique floue.

[5Une des dernières en date : La démonstration par Terence Tao que tout nombre impair supérieur à un est la somme de 5 nombres premiers (au plus).

[6Un auteur définit un « résultat bien connu » comme « une conjecture qu’on n’a pas le temps de démontrer » et qui paraît suffisamment évidente pour que personne ne prenne le risque d’avouer qu’il ne la connaît pas. Il peut très bien arriver que le « résultat bien connu » ne soit en réalité connu de personne !

[7ou l’inverse : Proposer comme exercice la construction du pantographe, en donnant le symétrique de A par rapport au point marron, comme but de l’exercice ; dans ce cas au contraire on désactive l’outil « symétrie centrale » dans la palette restreinte.

[8Donc un intervalle de confiance à 95% pour la proportion de n pour lesquels cette conjecture est vraie, est [0,76 ;0,96]


Commentaires

Annonces

Prochains rendez-vous de l’IREM

Séminaire EDIM-IREM

- Mercredi 22 novembre 2017, 14h-18h, campus du Tampon, amphi 120 D
- Mercredi 7 février 2018, PTU, Saint-Denis, salle S23.6
- Mercredi 7 mars 2018, 14h-18h, campus du Tampon
- Mercredi 4 avril 2018, PTU, Saint-Denis, salle S23.6
- Mercredi 2 mai, 14h-18h, campus du Tampon
- Mardi 5 juin 2018, PTU, Saint-Denis, salle S23.6
- Mercredi 6 juin, 14h-18h, campus du Tampon

Fête de la science

Campus du Moufia, 16 et 17 novembre 2017.
Thème : « La recherche à l’heure du numérique »

Semaine des mathématiques

Du 26 au 31 mars 2018.
Thème : « Mathématiques et mouvement »


Brèves

Décès de Raymond Smullyan

mercredi 15 mars

Le logicien Raymon Smullyan est décédé en février 2017, à l’âge respectable de 97 ans : Il avait eu Alonzo Church comme professeur ! Pour en savoir plus, voir cet article

Travailler à plusieurs

lundi 19 décembre 2016

Les enseignements d’exploration au lycée imposent aux enseignants de travailler ensemble. Chantal Tuffery-Rochdi a analysé dans sa thèse les pratiques des enseignants de MPS (méthodes et pratiques scientifiques). Elle répond aux questions des Cahiers pédagogiques.

Un document sur Eduscol

mardi 19 mai 2015

Un document clarifiant bien la façon dont les mêmes concepts vivent en mathématiques et dans les sciences « exactes » les utilisant, publié par Eduscol en octobre 2014. Citons-les :
« Le document proposé ci-dessous s’adresse aux professeurs de mathématiques, physique-chimie et sciences de l’ingénieur intervenant dans le segment [Bac-3 ; Bac+3]. Il vise à les informer des différences de présentation et d’interprétation qui sont faites de certains concepts mathématiques dans les autres disciplines. Ces éclaircissements peuvent contribuer à harmoniser et à clarifier l’utilisation de ces notions auprès des élèves. »

Histoire de la comptabilité

vendredi 28 décembre 2012

Sur ce site (en anglais) dédié à la comptabilité, on trouve des informations intéressantes sur l’histoire et les pratiques de ce domaine, qui peuvent être utiles aux professeurs enseignant des mathématiques financières (et aussi aux autres...).

La CGE et la réforme des lycées

lundi 16 janvier 2012

La Conférence des Grandes Écoles publie 19 préconisations pour la réforme du lycée.

Sur le Web : Les 19 préconisations

Pratique des mathématiques en série STD2A

lundi 16 janvier 2012

Le site de l’IGEN offre des recommandations et des ressources pour enseigner les mathématiques en série STD2A. Les thèmes abordés (couleurs et nuances de gris, arcs et architecture, jeux vidéos, photo et tableur, perspectives parallèles...) sont de nature à donner aussi des idées d’activités aux enseignants des autres séries !

En cheminant avec Kakeya

lundi 16 janvier 2012

Un livre (à télécharger) de Vincent Borelli et Jean-Luc Rullière qui présente le calcul intégral et la dérivation en s’appuyant sur la question de Kakeya. Pour les lycéens, les étudiants et tous les esprits curieux qui souhaitent voir les mathématiques sous un jour différent.

Sur le Web : Livre à télécharger

Bicentenaire Galois

lundi 12 septembre 2011

À l’occasion du bicentenaire de la naissance d’Évariste Galois (1811-2011), l’Institut Henri Poincaré et la Société mathématique de France organisent un ensemble de manifestations et proposent un site contenant diverses ressources documentaires susceptibles d’intéresser les enseignants.

Statistiques

Dernière mise à jour

dimanche 12 novembre 2017

Publication

773 Articles
Aucun album photo
133 Brèves
11 Sites Web
132 Auteurs

Visites

906 aujourd'hui
1252 hier
2163217 depuis le début
24 visiteurs actuellement connectés