"Preuve par Geogebra"

Lorsqu'on constate un alignement sur geogebra sur une figure dépendant, disons, de $n$ points en faisant varier ces points, on considère presque ça comme une preuve. Appelons $F(a_1,...a_n)$ la figure. Supposons que les courbes algébriques qui s'illustrent sont de degrés au plus $d$. Alors il existe un entier $g$ telle que pour tout ensemble de plus de $g$ point vérifiant certaines conditions de "généricité", la garantie qu'on a un alignement dans les situations où on applique $F$ à chacun de ces "plus de $g$" $n$-upplé fournit une preuve (par Bézout) que ces points sont bien alignés. Le problème est qu'on a pas de telle garantie, à part nos yeux, mais on a un nombre potentiellement infini d'encadrements (en l'occurrence extrêmement précis) et on doit pouvoir utiliser les encadrements d'interpolations pour pouvoir établir que les points sont réellement alignés.

Question : existe-t-il des logiciels qui utilise ces techniques pour démontrer des alignements ?
Et je dis bien démontrer (à partir du moment où on considère preuve par informatique comme preuve)

Il pourrait y avoir un logiciel à l'intérieur de geogebra qui utilise des techniques mettant en scène des inégalités d'interpolation et disons la souris de l'utilisateur pour lui signaler qu'il s'est suffisamment baladé avec la souris pour qu'on soit sur que tel ou tel groupe de points sont alignés. (le logiciel pourrait le faire sans la souris de l'utilisateur mais ça donne une info importante à l'utilisateur si il se met à clignoter à tel ou tel moment)

J'imagine que cette question a dû être traitée mais en tout cas, personne ne dit sur le forum "geogebra confirme" de façon formelle je pense, c'est une sorte de boutade de dire "confirme" alors qu'on a déjà démontré. Vu que personne ne dit "c'est vrai, car geogebra le démontre" je me dis que la question n'est peut-être pas encore clairement traitée. Pouvez-vous me renseigner là-dessus?

Merci

LMPC

Réponses

  • Bonjour, LMPC,
    Mais il n'y a pas besoin "d'encadrements de plus en plus précis" pour vérifier avec Geogebra que trois points sont alignés !
    Tu peux tout simplement tracer la droite passant par deux de ces points et demander à Geogebra quelle est la distance du troisième point à cette droite (avec suffisamment de chiffres significatifs), et s'il te répond "0", cela veut bien dire que les trois points en question sont alignés ...
    La distance d'un point $P(xp, yp)$ à une droite d'équation $ax + by + c = 0$ dans le repère orthonormé de Geogebra est immédiatement calculable, n'est-ce pas ? Je ne pense donc pas qu'on ait éprouvé le besoin d'élaborer des logiciels a priori plus compliqués ... Mais à vrai dire, je n'en sais rien !
    Par ailleurs, quand quelqu'un écrit "Geogebra confirme", je comprends, pour ma part, "Geogebra m'a permis de vérifier telle ou telle hypothèse, ou tel ou tel résultat de calcul", et non pas "Geogebra démontre ...".
    Bien amicalement, Jean-Louis B.
       
  • jelobreuil a dit :
    Bonjour, LMPC,
    Mais il n'y a pas besoin "d'encadrements de plus en plus précis" pour vérifier avec Geogebra que trois points sont alignés !
    Tu peux tout simplement tracer la droite passant par deux de ces points et demander à Geogebra quelle est la distance du troisième point à cette droite (avec suffisamment de chiffres significatifs), et s'il te répond "0", cela veut bien dire que les trois points en question sont alignés ...

       
    Non pas forcément, en tout cas pas aussi clairement. 

    Par ailleurs, quand quelqu'un écrit "Geogebra confirme", je comprends, pour ma part, "Geogebra m'a permis de vérifier telle ou telle hypothèse, ou tel ou tel résultat de calcul", et non pas "Geogebra démontre ...".
    Bien amicalement, Jean-Louis B.
       
    Je ne comprends pas ce "par ailleurs", personne ne dit autre chose, justement... je me demande si on pourrait en toute rigueur.

    Par ailleurs😂😂 les deux parties que j'ai citées sont en légère contradiction (du point de vu de l'argumentatif) car s'il est vrai qu'un alignement certifié par Geogebra en est toujours un, il suffit, dans les cas où les courbes sont algébriques, de le vérifier pour un nombre fini de configurations, et on peut facilement trouver une borne supérieure $M$ même très très large, de configuration à tester, et conclure que c'est une vraie preuve. donc en gros si ce que tu dis est vrai dans la première citation, alors quelqu'un qui invoque Geogebra (et qui justifie qu'il a fait  $M$ vérifications) peut légitimement dire "Geogebra démontre .."(sic)

    Amicalement

    JC
  • Geogebra Discovery permet de faire des preuves certifiées.

  • @lesmathspointclaires,  j'écris "Par ailleurs" pour signifier que je change de sujet, ce n'est qu'un artifice de rédaction ... au même titre qu'un "D'autre part", par exemple ...
    Bien amicalement, JLB


  • @lesmathspointclaires : il n'y a pas de preuve possible avec l'utilisation dont tu parles de la version standard de GeoGebra. On peut d'ailleurs fabriquer des contre-exemples où le logiciel se trompe tout le temps, et cela montre que tu ne peux pas conclure que trois points sont alignés simplement parce qu'il le dit.
    J'ai fabriqué de tels contre-exemples : ici GGB affirme que les points $C$ et $M''$ sont confondus pour une bonne partie de l'arc où se déplace $A$, alors qu'on peut démontrer que c'est toujours faux.
    Une autre version de cette figure ici.
  • lesmathspointclaires
    Modifié (30 Oct)
    @parisse Merci, je vais examiner plus en détail tout à l'heure ! J'ai déjà jeté un très rapide coup d'œil et j'ai l'impression que cela répond à la question.
    @jelobreuil j'entends bien mais les artifices de rédactions sont parfois de nature à subtilement désorienter un propos, et ce n'est pas la première fois que je remarque cela dans ton discours (je me permets ce petit tacle amical en te rappelant que  tu m'as taquiné sur mon pseudo (jeu de mot avec "point net") , certainement à juste titre, mais si je ne semble parfois pas clair, c'est peut-être justement parce que j'essaie d'être précis, peut-être que je devrais l'être encore davantage, pour dissiper toute ambiguïté, mais je ne serais lu que par de rares courageux, donc je pense qu'il s'agit d'optimiser le ratio précision/lisibilité, en attendant que je me perfectionne, je me permets de faire remarquer à ceux qui me répondent à la va-vite, qu'il serait préférable qu'ils lisent bien ce que j'écris en ayant à l'esprit que sauf maladresse de ma part, si j'évoque quelque chose qui leur parait simple d'une façon qui leur parait compliquée ou peu claire, c'est que peut-être je ne dis pas le quelque chose qu'ils croient que je dis.....) 

    Ceci m'offre une parfaite transition pour m'adresser @Ludwig qui n'a sans doute pas compris ce que je disais... Peut-être d'ailleurs parce qu'il a été parasité dans sa lecture par la "confusion simplificatrice" de jelobreuil consistant à jeter quelques truismes mal articulés ayant un vague rapport avec le sujet (j'insiste non pas (que^^) pour être taquin, mais parce que je pense que cette attitude nuit au propos, mais ça n'enlève rien à la sympathie que je te porte !).

    @Ludwig : je ne prétends justement pas qu'observer quelques semblants d'égalités soit une preuve, et même pas qu'observer un semblant d'égalité dans toutes les configurations soit une preuve (observe "par ailleurs"** dans ton exemple l'égalité affirmée par GGB n'a lieu que sur une portion connexe limitée du cercle qui paramétrise la figure), mais qu'il y a des cas où un nombre fini d'encadrements (fonction du contexte, et des diverses interpolations de courbes algébriques, encadrements même pas nécessairement aussi fins qu'un œil ne les distingue!!!) suffit à conclure, et que dans ces cas uniquement, il serait pertinent d'avoir un outil qui l'utilise pour donner une preuve (acceptable par tous ceux qui acceptent une preuve par ordinateur), rien n'interdisant d'utiliser d'autres techniques de démonstration que celle très spécifique dont je parle, merci encore @parisse : je poserai sans doute des questions aux concepteurs qui apparemment en donne l'opportunité et je rapporterai d'éventuelles précisions dans le thread.

    @Ludwig à nouveau : par ailleurs** (et là, c'est un vrai "par ailleurs"), je ne peux pas encore dire "waou" à ton exemple, car la construction est cachée : les courbes sont-elles toutes algébriques ? Si c'est le cas, c'est très joli ! Peux-tu en dire plus sur cette construction, comme par exemple l'expliciter (peut-être qu'il y a un moyen de le faire depuis les deux liens que tu as donné mais je ne l'ai pas trouvé^^)
    Merci en tout cas pour ce lien qui permet (s'il n'y a pas une espèce d'arnaque dessous) d'illustrer le fait que ce n'est pas aussi simple que ce que @jelobreuil le semble prétendre, merci à tous pour ces interventions toutes utiles pour des raisons diverses!!
     




  • Ludwig
    Modifié (30 Oct)
    J'ai détaillé la construction de ces deux figures ici.
    Je vois mal comment on pourrait déterminer les cas pour lesquels un nombre fini d'encadrements permette de conclure. Au contraire, je pense qu'il doit être assez facile de produire un contre exemple à partir d'une configuration de base donnée. Rien qu'avec deux cercles et quelques droites (voir ma figure "Dans les choux") on fait déjà échouer GGB.
  • Cher Ludwig, je suis pris par la conversation intéressante du fil que tu as initié, je ne suis donc pas encore arrivé à la conclusion et la construction en question, mais je suis rassuré quant au fait qu'elle ne "triche pas", et que tu n'es pas un farfelu lol. Dès lors, puisque cette fonction respecte les règles que tu annonces dans le fil : chapeau !

    On se pose la même question toi et moi, et il est possible que toi comme moi soyons victime de biais, dans des directions contraires, pour les dissiper il faudra juste résoudre le problème, si on le peut, en tout cas au moins partiellement.

    Ce qui me fait dire que tu es sans doute victime d'un certain biais, c'est tout simplement que tu confonds quel que soit et il existe, ce qui pour quelqu'un de ton niveau n'est possible que si tu t'es fabriqué une histoire, d'ailleurs d'où peux-tu tenir que c'est impossible dans certain cas, juste parce que tu as prouvé que ça l'était dans d'autres ?? et dans des situations ad hoc, donc identifiables.

    C'est vrai que ça n'est pas forcément évident quand on lit mon premier post que je parle de situations précises où justement il y a un moyen de conclure. De dire qu'il n'y en a pas en revanche, c'est s'avancer un peu trop en tout cas sans preuve. Je serai par exemple plus qu'étonné que le démon contre ma thèse puisse juste avec des constructions à la règle arriver à créer des points faussement alignés ou faussement confondus en ce sens bien précis que si on laisse l'ange bouger les paramètres de constructions, il ne puisse démasquer le faux alignement (si le démon gèle certains paramètres c'est autre chose, mais qui a parlé de ça?)  

    Tu es d'accord au moins avec le fait que dans cette configuration, un nombre fini de vérifications dépendant du nombre de droites tracées suffit? 

    Si oui, c'est qu'il y a des situations où le fait de pouvoir conclure sur plusieurs encadrements s'applique.
    Après peut-être que ces situations sont moins courantes que ce que je pronostique, mais j'ai conscience que ce n'est qu'un pronostic. Et je le répète, il me semble quasi indéniable qu'il y a des situations non triviales où un nombre fini (même grand) d'encadrement permet de conclure, je ne comprends pas qu'on puisse soutenir le contraire (et j'ai du mal à concevoir qu'on puisse non pas soutenir, mais simplement croire le contraire, mais ça, ça reste une sorte d'évaluation opinion vs opinion) 

  • En complément de mon message précédent, je précise que Geogebra Discovery ne fournit pas une preuve "classique" (de géométrie synthétique), il traduit le problème en un calcul d'élimination polynomiale. 
    Le certificat renvoyé correspond à l'écriture (de 1 ou de 0 en général) comme combinaison linéaire des générateurs polynomiaux d'un idéal, à la différence d'un calcul usuel de base de Groebner qui va renvoyer une base de l'idéal sans déterminer les combinaisons linéaires des générateurs permettant de retrouver la base. On peut ensuite aisément vérifier le certificat, éventuellement avec un autre logiciel de calcul formel. Le calcul est relativement long alors que les algorithmes efficaces de calcul de bases de Groebner sont en général beaucoup plus rapides, mais non certifiés (ce sont des algorithmes multi-modulaires qui en gros s'arrêtent lorsque la reconstruction se stabilise, ce qui assure une très grande probabilité d'exactitude mais pas une certitude).
    C'est tout-à-fait analogue à un certificat de primalité vs un calcul (de type Miller-Rabin) donnant une quasi-certitude qu'un entier est premier.
Connectez-vous ou Inscrivez-vous pour répondre.