X-UPS Days 2026: "Formal Verification of Proofs" – Benjamin Werner 2

Merci Pascal. Bonjour tout le monde. Donc en fait, je vais je vais vraiment faire deux exposés. C'est un petit peu une gageur parce que c'est vraiment deux trucs extrêmement différents et les deux m'intéressent beaucoup. Euh mais il y aura clairement une une rupture entre les deux, hein. La partie donc les quatre couleurs, on va reprendre et on va regarder vraiment ce qui se passe dans la preuve. Et le petit commentaire là-dessus, c'est que c'est alors je pense c'est intéressant, en tout cas c'est amusant et ça pose des questions sur la formalisation. C'est une motivation pour la formalisation, mais dans le monde mathématique d'aujourd'hui, c'est quand même un petit peu ça reste une espèce de monstre ce théorème au sens que c'est un quand même un truc très particulier. Et dans la deuxième partie, je vais parler complètement d'autres choses qui est une interface graphique pour faire des preuves. Et donc là, c'est plutôt pour aller vraiment vers les mathématiques qu'on fait tous les jours, qu'on enseigne tous les jours, que vous enseignez tous les jours et comment euh ça pourrait ça pourrait évoluer. Mais donc revenons au aux cas de couleur, hein. Donc on avait vu la la preuve fausse le truc, mais il y avait comme cette idée que on trouvait un point faible dans le graphe, on enlevait ce sommet, on coloriait le reste et puis après il fallait qu'on recolle euh avec le coloriage de l'extérieur et que le coloriage de l'extérieur, il fallait qu'on le change un petit peu ou un peu plus. Et donc la d'un point de vue formel, pas formalisation juste dans la preuve, ce qu'on va faire c'est que au lieu de regarder, j'avais dit le sommet qui a le moins de voisin, on va regarder les sommets qu' ont le moins de voisin à distance 2. Mais alors là, il y a quand même beaucoup de cas, hein. Euh il y a une étude combinatoire alors qui dans la preuve de 76 avait été faite à la main. dans la preuve de 95 déjà, il y a aussi un programme qui vérifie que ça marche, hein, euh pour identifier un certain nombre de configurations. Donc ça, c'est quelques-unes des 633. Euh et euh le truc c'est que d'une part, on va montrer qu'on a une de ces 633 configurations. Donc ça, je vais pas trop en parler. Euh et euh ensuite on va voir donc ça c'est que c'est inévitable. Donc ça je vais pas trop en parler. Et ensuite on va voir que ces configurations dans chacun des cas on va être capable de le traiter et comme j'ai dit c'est dans chacun des cas qu'on aura beaucoup de calcul. C'est ce qu'on appelle la euh la réductibilité hein. C'est ici qu'arrive le calcul. hein. Donc j'ai dit on verra demain mais en fait c'est aujourd'hui. Euh et là en fait fallait que je saute plus loin dans le truc. Ça c'est voilà c'est ça. C'est ici que je voulais commencer. Euh c'est ici que Oui, c'est juste pour pour bien comprendre le qu'est-ce que ça veut dire avoir peu de de voisins à distance 2. C'est on compte tous ceux qui sont à distance 1 ou 2 et on regarde. Non, je crois que c'est la longueur du cercle de rayon mais je en fait pour être tout à fait franc, je suis plus sûr si c'est pas rayon 3. D'accord. Euh mais donc par exemple le tout premier cas là en haut à gauche, c'est c'est alors on va regarder là. Il y en a un peu plus mais c'est les mêmes. Euh donc euh vous voyez qu'il y a une espèce de code là pour dire euh que les sommeils sont soit un petit point un gros point, soit un petit point comme ça ou alors un point comme ça. C'est un code pour dire le nombre de voisins. Donc ça ça veut dire qu'ils ont trois voisins. Non quatre voisins. Quatre voisins comme là il y en a déjà trois. Ça veut dire qu'il y en a un de plus ici, un de plus ici de 2 donc comme ça. Voilà. Pardon, je fais des bêtises. Et un de plus. Tu veux qu' affich? Ouais. Oui, mais ça c'est le même. Voilà, c'est celui-là ou 5. Alors, c'est ça. Je sais plus, je suis perdu. Je je l'ai je l'ai refait tout à l'heure là pour me dire faut pas que je me plante. Euh bref, le résultat, on fait le truc, ça tombe juste. Et ça veut dire que en fait autour de ça, vous avez un truc de rayon euh de 6, d'accord? De rayon 6. Celui d'après, il y en a un de plus là, donc un rayon 7. Et puis là, après, il faut décider, c'est un peu plus compliqué, il y en a plus. Les frontières, elles sont entre 6 et 14 sommets, hein. Donc, ce qu'on va faire, c'est qu'on va découper sur cette frontière. On va colorier l'extérieur et après il faut qu'on recolle avec un coloriage de l'intérieur. Euh il y en a un certain nombre là. C'est ce qu'on appelle des contrats. Euh je vais dire tout à l'heure ce que ça veut dire mais c'est pas pour l'instant c'est pas le truc important hein. Donc l'idée c'est qu'on découpe. Voilà là on a le dessin. C'est ça que j'avais pas réussi à faire. Donc il y en a deux là. Donc en fait c'est cinq. Voilà deux ici puis là. D'accord. Là, vous avez le losange là au milieu et puis là vous avez les trucs et donc vous avez le truc de longueur euh c'est 6 ou non c'est un autre. Bon en tout cas on découpe le long du truc. D'accord. J'ai dupliqué les trucs. On colorie l'extérieur, on colorie l'intérieur et il faut qu'on réussisse à recoller le truc après un certain nombre de réarrangements, après un certain travail. Alors, comment ça marche? C'est là qu'on a la grosse combinatoire. Vous rappelez qu'il y avait une autre preuve fausse en 1880. Et celle-là, elle était due à Tate, à monsieur Tate. Et il avait fait cette remarque que euh quand on quatre coloris les sommets sur un graphe triangulé, c'est la même chose que de trois coloriers les arêtes, hein. Donc là, j'ai fait que l'intérieur, on a deux faces, mais ça veut dire que vous voyez, j'ai trois couleurs, rouge, vert et bleu. Et chaque triangle voit chaque couleur une et une seule fois. Donc la l'idée c'est assez simple, c'est qu'en gros la couleur de l'arrête si vous voulez la différence entre les couleurs des deux sommets, hein. Donc si on connaît la couleur d'une des extrémités et la couleur de l'arrête, on a forcément la couleur du de l'autre sommet. Donc en gros, on fixe une couleur de sommet. Si on a le tr coloriage des arêtes, on a on colorie tous les sommets et on a la propriété que sur un cycle, la somme des couleurs, c'est c'est l'identité. sur un triangle toc toc toc on a les trois couleurs une fois c'est l'idée. Vous pouvez le faire je pense que c'est raisonnablement clair. Alors une fois qu'on a fait ça, quand on a une case triangulation donc là quelque part vous voyez la quasi triangulation le la face pas triangulaire elle est à l'extérieur. En pratique, ça sera plutôt à l'intérieur au sens qu'on aura le gros graphe, on a enlevé la configuration au milieu et qu'on va colorier. Ce qu'on va faire, on va choisir une couleur qu'on va appeler la couleur pivot. Donc, on va dire vert ici, c'est pivot. Et puis je vais dire, bah je vais prendre une arrête ici qui est pas verte et je vais la traverser et je vais ressortir par l'autre arrête non verte. Donc à chaque fois, j'ai pas le choix. Je rentre par un triangle dans un triangle en passant par l'arête rouge ou bleu et puis il faut que je sorte par la bleue ou rouge. Et donc je finis par ressortir parce que je peux pas faire de cycle hein. C'est pas possible que je retombe sur les trucs. Donc je retombe sur une autre arête rouge ici et puis je peux recommencer sur la suivante et euh bah je ressors sur là sur l'autre arête rouge. Alors qu'est-ce que je peux faire là? sur le chemin alter les couleurs. Exactement. Je peux inverser les rouges et bleu sur les trucs. Alors, une autre remarque, c'est que je vais faire ça tout de suite sur les dessins. L'autre remarque, c'est que quelque part donc là on a cette structure qui est assez informatique, syntaxique qui apparaît, ce qu'on appelait George George a appelé un chromogramme, ils appellent ça sign matching dans l'article américain. Donc c'est quoi? un mot bien parenthès où il y a les parenthèses ouvrantes, les parenthèses fermantes sont euh marquées par un plus ou un moins et puis il y a le tiret. Donc le tiret c'est quoi? C'est pour les verts. Euh les parenthèses ouvrantes c'est quand on rentre dans le truc. La parenthèse fermante c'est quand on sort. D'accord? Donc là l'idée c'est quoi? C'est que le mot ici je l'ai fait débuter là en tournant comme ça. J'aurais pu faire autrement. Donc le bleu, vous voyez qu'ensuite on a tout euh on a une deuxième parenthèse ouvrante qui correspond au rouge. Une un rouge ici qui est la parenthèse fermante. Alors plus ça veut dire que c'est de la même couleur donc c'est la parité du chemin. Ensuite on a vert vert vert qui sont des tirets. Ensuite on a la parenthèse fermante qui elle est moins parce que c'est pas la même couleur. Et ensuite on a les deux verts. Et donc on peut assez facilement définir la relation de être compatible avec entre un coloriage, une suite de couleur et un chromogramme. Et comme Guillaume l'a dit, ben sur un chemin comme ça, je peux inverser les couleurs. Et là, j'ai un autre coloriage qui est également compatible avec le chromogramme. Donc en gros, une fois que j'ai choisi le pivot, ça c'est le pivot, ça c'est l'autre la couleur que je veux mais il faut que quand je fais quand je referme, j'ai la couleur correspondante. Alors, ça induit une petite remarque d'ailleurs qui est que la parité du nombre de pivots vert ici, c'est identique à la longueur de la frontière puisque les parenthèses elles se elles se ferment et puis c'est vrai pour les autres couleurs puisqu'on pourrait choisir le pivot qu'on veut. et pardon. Ah non, c'est pas ça. Oui. Là, le chronogramme tu l'as écrit en regarde le tour. Ouais. Mais on n pas censé avoir des triangles partout? Non, c'est la quasi triangulation. C'est une cas Ah oui, quasi et le tout le truc ça va être d'avoir deux quasi triangulations avec la même longueur de frontière qu'on va recoller. C'est ça. D'accord. Et en fait ce comme je disais, la quasi triangulation où on va faire les réarrangements, ça sera plutôt l'extérieur, ça sera le gros graphe, c'est pas la configuration. Donc euh un coloriage induit un chromogramme qui est compatible avec le coloriage de la frontière. Et une fois que j'ai le chromogramme, je peux recolorier sur la frontière et je peux obtenir n'importe quel trois coloriage qui est compatible avec le le chromogramme. Et du coup euh et du coup ben la manière dont on va traiter les configurations essentiellement c'est ça. On va prendre la configuration, donc le petit bout de graphe là, le petit dessin et on va énumérer tous les coloriages possibles et on va regarder l'ensemble des coloriages que ça de frontières que ça donne. Et je vais appeler ça C0. Et ensuite, je vais regarder quels sont les coloriages que je peux atteindre, que je suis sûr de pouvoir atteindre en reconfigurant, hein. Donc si j'ai un coloriage tel que pour un certain pivot, pour tout en fait là les chromogrammes, j'ai appelé ça W pardon, j'ai changé de lettre. Pour tous les chromogrammes compatibles avec le coloriage, il existe un coloriage qui est dans ces zéros que je sais atteindre. Et ben dans ce cas, ce coloriage là, je sais aussi l'atteindre. OK? En gros, ça généralise le raisonnement qu'on a fait sur les quatre la longueur 4. Euh bah du coup ça nous donne un ensemble C1 et puis après on peut recommencer. Alors, je rajoute ces zéos là puisque en gros ça veut dire que je sais traiter ça. Donc là, je sais traiter tout ça. Je sais traiter tout ça et on itère. Puis comme tout est fini, bah il y a un moment ça s'arrête quoi. Pardon? Euh C prim ici. Ouais. Ouais, tout à fait. Merci Alisé. C prim ici. Donc jusqu'à ce qu'on s'arrête. Et euh si on a traité tous les coloriages là, tous les coloriages qui ont la bonne condition de parité puisque on est si a que ceux-là qui peuvent arriver, bah dans ce cas, on sait qu'on peut recoller. Donc ça ça c'est dans ce cas-là, on dit que la configuration est réductible. On sait on est bon. Alors en fait, si on rentre dans les détails, c'est ce qu'on appelle déréductible. La plupart des configurations qu'on a, il y a elles sont seulement c'est réductibles. Euh mais en fait les configur les coloriages qu'on va pas savoir traiter, on peut ramener ça à un contreexemple sur un truc plus petit. Et en gros, on fait la même chose pour le vous avez les les arêtes un peu grasses là, on les contracte, on fait la même manipe et on va montrer que les coloriages qui sont problématiques, donc ils sont pas dans le sé, ils sont aussi problématiques pour le le truc contracté. Donc on aurait un contrexemple plus petit. Euh et alors c'est là qu'on a beaucoup de combinatoires. Je vais donner les chiffres après, mais c'est là que ça devient compliqué. C'est-à-dire que euh bah en gros euh des coloriages euh longueur 14 3^iss 14, c'est là que ça commence à faire beaucoup. Euh alors même avec de la symétrie, on un peu de symétrie, on arrive à 500000 coloriages possibles et des chromogrammes 1500000. Euh alors on va cela dit euh on va regarder comment on fait ça. Donc dans le le programme C qui est fourni dans le papier de 95, on va le regarder, on va enfin on va le faire tourner. Euh il y a un certain traitement mais là nous on veut faire la preuve en rock. Donc il faut écrire le programme qui fait ça euh en langage fonctionnel pur. On va voir qu'on va améliorer un petit peu l'algorithme, hein. Mais ça veut dire qu'en particulier, par exemple, on tombe dans des questions qui sont informatiques. Ça, c'est des trucs qu'on fait en cours d'informatique. Comment on représente un ensemble euh de mots comme ça dans un langage fonctionnel pur? Bah, ce qu'on va faire, c'est qu'on va le représenter par un arbre. Donc là, c'est pour les coloriages, d'accord? Donc c'est c'est des séquences de de mots dans un alphabè trois lettres. Les trois couleurs d'arrête, bah c'est des arbres ternaire. Donc là si la première lettre c'est rouge, on est ici. La deuxième c'est rouge, on est ici. Et la troisième est bleu, on est ici. D'accord? Donc rouge rouge bleu n'y est pas mais rouge rouge vert il est dans l'ensemble hein. Rouge vert vert c'est rouge vert vert. Il est là euh lequel on a ici là par exemple ça c'est bleu rouge bleu qui est effectivement dans l'ensemble. Donc on on construit cette structure puis chaque fois qu'on en rajoute un euh ou qu'on en enlève un suivant qu'on prenne le complémentaire ou pas, ben on va reconstruire l'arbre en euh changeant une une des feuilles. Après il y a un petit peu d'optimisation parce qu'on a la euh pour le coup là on peut faire un truc de symétrie par rapport aux couleurs. Donc on va dire que la première c'est toujours rouge par exemple. La parité, elle va imposer le la dernière couleur. Euh donc ça fait que les les frontières qu'on considère en fait c'est de longueur 12. Euh alors je sais plus s'ils font ça dans le papier de 95. Peut-être que ça fait un peu moins de 500000 mais enfin ça reste quand même gros hein. Alors là j'ai décrit comment on construit les définitions des C. On peut le faire comme ça mais là c'est c'est très naïf. On a intérêt à utiliser un algorithme quand même un petit peu plus malin. Alors ça c'est l'algorithme usuel au sens que c'est celui qui est présenté dans l'article de 95, celui qui tourne en qui qui donne en C. On a donc ça ça serait naïf, d'accord? Ça serait de C'est ça, c'est la définition que j'avais tout à l'heure, ça serait de définir directement C + 1 à partir de C. Euh ce qu'on va faire pour être un petit peu plus efficace déjà, c'est qu'on va avoir en parallèle un ensemble de configuration de pas de configuration de chromogramme, les mots parenthèsés. Euh et donc en gros, c'est les chromogrammes euh qu'on s'est traité. Donc ça veut dire que à partir de ce chromogramme, je peux atteindre un coloriage qui est correct. Euh et du coup euh bah du coup on peut définir C + 1 comme à partir de K au lieu de le définir à partir de C. Euh et euh on fait comme ça. Les chromogrammes, c'est pareil, c'est des mots de quatre lettres. Donc en gros, c'est des arbres caternaires. Alors c'est pareil, il y a les trucs à la fin qu'on peut retrouver parce qu'il faut fermer la parenthèse. On a le signe, en tout cas le signe de la dernière parenthèse est imposé. Je sais plus si on arrive à optimiser ça. Euh donc ça c'est l'algorithme usuel. L'algorithme usuel du coup c'est ça. On calcule C0, on parcourt C0 enfin en l'occurrence C après l'étape d'après pour énumérer les pivots et les chromogrammes compatibles. Et euh pour chaque chromogramme on le rajoute à l'ensemble des chromogrammes qu'on s'est traité. Et puis ensuite, chaque fois qu'on rajoute un chromogramme dans Kai, on va parcourir tous les coloriages. J'ai pas le truc super en tête, hein. On n'est pas euh il y a des gens qui sont très forts qui arrivent à qui arriveraient à me corriger là si je me plante. Mais euh mais en gros, pour chaque euh on va être obligé de reparcourir les coloriages. on prend les C primes compatibles, on repère ceux dont tous les chromogrammes compatibles sont déjà dans le Kai et c'est cela qu'on rajoute dans le dans le C dans l'ensemble CI suivant. Du coup, il y a ce parcours qu'il faut faire et comme George Gontier est un mathématicien extraordinaire mais aussi un informaticien extraordinaire, il a dit bah oui mais en fait on peut être plus malin au lieu d'avoir pour l'ensemble des chromogrammes juste un boulé qui nous dit il est dans l'ensemble ou pas. Non, ce qu'on va faire, pardon, pour les coloriages, il est dans l'ensemble ou pas, on va mettre le nombre de chromogrammes compatibles euh qui sont pas encore dans Kai. Donc, on calcule ça au début et puis chaque fois qu'on rajoute un KI, on prend les chromogrames, les les coloriages compatibles, on diminue de 1 et puis quand on tombe à zéro, paf, on est bon. Alors du coup, il y a un dessin sur le les notes là où ça explique pourquoi on parcourt moins une le des arêtes pas pas les arêtes du graphe mais des des trucs entre des relations entre les chromogrammes et les coloriages et on est à peu près on est à peu près optimal. Et là voilà, ça c'était le truc que j'aurais dû mettre avant. Donc comme ça, ça tourne. Euh, il y aurait pas mal de choses à dire euh mais pour euh pour avoir les ordres de grandeur. Donc ces trucs qui font que là, on a vraiment besoin des machines. Donc pour les grandes configurations, j'ai dit on est on doit considérer 500000 coloriages de frontières, euh 1500000 chromogrammes. Et le truc qui est fou, c'est que pour les configurations les plus compliquées, pour arriver à l'ensemble C limite là, il faut arriver c'est C130 à peu près. C'est qu'il faut faire jusqu'à 130 réarrangement. Et euh alors je vais revenir sur les conclusions. Est-ce que j'arrive Alors, du coup là, on a un truc très bordélique. Attendez, je vais faire comme ça. Donc là, je suis dans une fenêtre Unix et il y a le fichier le programme là. Il faut que j'agrandisse. Voilà, je vais lancer le programme. Donc c'est le programme C, celui des Américains. Il y a tas de trucs qui s'affichent. Qu'est-ce qui s'affiche? Il passe les configurations en revue et puis il dit là, j'en ai une ou là, pardon. Oui. Euh voilà, je vais la récupérer dans un fichier qui qui affiche le truc au fur et à mesure. Donc la première là, c'est la petite. Là, c'est 6. Donc il y a 16 coloriages. Là, on a le nombre de de chromogrammes. Première itération 106 toc toc toc. Et là, on tombe sur zé assez vite. On voit que c'est déductible. Là par exemple, je suis sur un truc. Ah oui, là je suis sur la fin. Là, on voit qu'il y en a une de 13. Il y a déjà pas mal d'itération. Euh alors ce qu'on va faire c'est qu'on va regarder plutôt le l'ensemble de l'output. Donc j'en avais trouvé une un peu grosse par exemple. Voilà ici. Donc là il y en a une 14. D'accord. Donc vous voyez qu'on commence avec euh ça c'est le nombre de coloriages. Alors en fait c'est marrant hein le nombre de coloriages qui marche au départ il y en c'est 20000 sur 500000 he et après les autres il faut vraiment les traiter. Donc ça diminue beaucoup. Vous voyez qu'il y a beaucoup beaucoup de de recoloriag tout ça. Ça c'est des contrexemples qui vont être des contrexemples du contrat. Voyez qu'à la fin on diminue peu 6. Bah ces 6 là sont nécessaires sinon ça marche pas. Donc c'est vraiment c'est ricraque quoi. En tout cas, ça donne l'impression qu'on est quand même très très ricrac. Euh et ça donne un peu cette impression qu'on a quelque chose qui est vrai par hasard. Alors, il y a beaucoup de choses qu'on pourrait dire là-dessus. On peut dire les trucs comme en exagérant un petit peu le théorème d'accomplitude de Godel, il dit bah oui, des fois il y a des théorè qui sont pas très grands et la preuve elle est immense. Donc est-ce que c'est ça? Est-ce que c'est ce genre de truc? Est-ce que ça peut arriver plus souvent? Est-ce qu'avec des de nouveaux outils, on tombera plus souvent sur des théorèmes monstrueux comme ça? Il y a pas mal de trucs. Il y a deux remarques que je veux faire. Enfin trois remarques. Euh il y en a une. Donc là on a un peu l'idée de la preuve he le calcul. Ben il y a vraiment un programme qui est écrit, il y a une preuve de correction et puis après, il faut recoller les trucs avec les un petit peu comme pour les noms de premiers quoi. Mais c'est c'est plus compliqué. Euh c'est que si on veut écrire la preuve du théorème des quatre couleurs dans un langage mathématique, ben on n pas le choix. on est obligé d'avoir un langage avec du calcul, hein. Si on l'écrit en théorie des ensembles comme dans l'article, et ben là, on est obligé de dire un moment et ben là vous regardez le programme C. Donc on change de langage parce que sinon on aura pas la le raisonnement est super simple hein. C'est vraiment dans ce cas-là, je fais ça, dans ce cas-là, je fais ça, dans ce cas-là, je fais ça. Sauf on le fait des milliards de fois. Euh donc là le seul les seuls langages où on peut l'écrire de manière uniforme de de manière uniforme, c'est des langages où il y a du raisonnement et des et des programmes. Donc c'est des trucs comme la théorie des types. Euh le deuxième truc, j'ai oublié. Donc la question, est-ce que il y a une preuve courte, une vraie preuve dirait les beaucoup de mathématiciens? Bah ça on sait pas. Enfin, ça commence à à pas on se dit que ça risque pas d'arriver tout de suite. Et il y a un dernier truc qui est que bien que cette preuve soit euh Ah oui. Non, ce que je voulais dire ce que je voulais dire c'est que quand on a une preuve comme ça, on va vraiment exploiter à fond les caractéristiques précises du formalisme. On va avoir besoin de faire de l'informatique non triviale. On va être dans une situation très très différente de ce qu'on a vu par exemple quand on fait du MAT matlib en ligne, hein, où là on peut utiliser euh des bibliothèques mathématiques, des définitions mathématiques, des outils, des tactiques sans être obligé de regarder tous les détails. Là, on est obligé de se coltiner tous les détails, hein. Donc c'est un c'est un gros boulot. Ça vaut le coup dans certains cas, mais on veut pas que ce soit toujours comme ça, ça c'est clair. Euh le dernier point, c'est que bien que ce soit une preuve monstrueuse euh parce que justement on est obligé de rentrer dans tous les détails, en même temps, c'est important d'être élégant dans dans une preuve comme ça ou dans une preuve formelle en général. Euh quand on a un outil d'automatisation, quelque part, une fois qu'il a répondu, qu'il a fabriqué une preuve, on est content. La preuve est vérifiée. Si elle est pas jolie, euh on s'en fiche un petit peu. Nous, ce qu'on voit, c'est juste "J'ai utilisé tel outil". Quand on fait la preuve plus à la main, c'est plus compliqué. On a beaucoup beaucoup d'hypothèses. Il faut il faut garder le une vision claire de son espace de travail. Et euh là dans ce tru là, il y a un truc que je trouve très très joli. Je l'ai pas mis sur les transparents, mais en fait euh pendant la formalisation, il y a tout un tas de trucs dans une arrête, découper un une quasi triangulation. C'est des trucs qui sont visuellement assez clairs mais c'est pas si facile formellement sur un truc formalisation algébrique si on veut. Et George s'est rendu compte que au fond la bonne manière de parler des graphes planaires, c'est pas d'avoir des arrêtes et des sommets, c'est de prendre on a des brins. Donc les arêtes en fait c'est deux voies d'autoroute. C'est ça c'est des brins. Et donc le graphe ou la la structure du graphe c'est donc c'est quelque chose qui généralise les graphes. Ça s'appelle les hypercartes. savait pas que c'était ça s'appelait des hypercartes que les combinatoriciens ils aimaient ça. Euh donc c'est un ensemble de brins B avec trois euh applications dessus qu'on peut appeler A comme arrête, S comme sommet, F comme face et avec alors peut-être qu'il y a un ordre là, j'ai pas le truc en tête. J'espère que je dis pas de bêtises, mais enfin en tout cas c'est à la composée des trois, c'est l'identité. Ça c'est une hypercarte. Et en gros, l'idée c'est quoi? C'est que les brins, ils partent de sommet. Donc du coup là le truc sommet c'est on prend le brince suivant qui part du même sommet en tournant dans un certain sens. Donc l'orbite de S, c'est les sommets. Euh l'autre ça va être euh je prends le som le brin suivant en tournant. Alors je crois qu'il faut que je tourne dans l'autre sens. Pareil, j'ai pas complètement révisé. Donc ça c'est là je passe sommet. Là, c'est F parce que l'orbite de cette application, ça va être les faces. Et euh la l'application arrête, c'est celle qui qui fait demi-tour, qui revient en arrière. Sauf que là, j'ai pas imposé. Et donc le fait d'avoir cette équation, ça impose que c'est des applications, c'est des permutations, des bijections. Là, j'ai pas imposé que les orbite de A, c'est des de cardinal 2. Ça c'est le cas particulier des graphes, mais les hypercartes, il y a des hyperarêtes et donc des fois on est dans un truc plus général et euh ça permet de euh moi je trouve ça assez fascinant et en tout cas ça simplifie réellement les tout un tas de de preuves. J'ai je sais plus non, je l'ai pas écrit dans les notes de cours. Il y a par exemple une jolie formulation épreuve d'une version combinatoire du théum de Jordan he qu'on peut découper le plan en deux sur ces trucs là. Un truc purement combinatoire, on parle pas de de nombre réel. Euh voilà. Donc là, je vais arrêter un peu brutalement ici sur les quatre couleurs. Euh est-ce qu'il y a des questions là-dessus ou est-ce qu'on veut les garder pour plus tard? S'il y a pas de questions tout de suite euh bah je vais passer à la suite complètement différent. Donc ça c'est plus récent pour moi. Euh alors euh je vais C'est un titre de transparent. Euh non je vais essayer de Ouais non je vais garder le partage. Je vais essayer de Faut que je mette ce truc là. Alors, c'est en fait sur les trois petits points, il y a une dans le menu, il y a masquer les commandes flottantes. Génial. Euh voilà et puis un certain nombre de gens qui ont travaillé là-dessus. Donc euh là c'est euh donc j'ai appelé ça comment faire des preuves à la main ou avec la main plutôt. Euh donc je vais monter un montrer un programme, un truc mais c'est vraiment un prototype, il est assez buggé. Euh d'ailleurs, j'ai j'ai là là j'ai j'ai pas la version la que je préfère. Euh les motivations de ça, c'est de faire des preuves formelles, hein. Donc il y a le début du truc, on va pas le refaire mais c'est tout le truc, Socrate et cetera, c'est de faire des preuves en on peut faire des preuves en rock, mais on pourrait brancher ça, j'imagine, sur quelque chose comme Lin. Et il y a deux il y a deux motivations d'une parc soit plus intuitif, plus facile à apprendre donc que la barrière pour fabriquer des preuvre formell soit plus soit abaissé mais aussi de faire l'épreuve de manière plus efficace hein. Donc en général quand je le montre on me dit toujours bah oui c'est plutôt c'est c'est vraiment pour le premier truc donc c'est pour l'enseignement en fait. Moi, je pense que euh si on en fait quelque chose de robuste, ça pourrait être utile pour des pour des gens qui ont l'habitude d'épreuv formell. Donc la remarque, une des remarques derrière ce travail, j'avais déjà dit, il y a plusieurs niveaux dans les la formalisation, hein, et il y a deux niveaux de de langage formel. Il y a celui des propositions et ça ça on a l'habitude, on est quasiment on a l'habitude de d'avoir un truc préformalisé déjà hein, euh une proposition mathématique et puis après tout ce qui décrit la preuve, faire une induction sûre, appliquer la tactique machin et cetera. Et euh dans les preuves formelles en particulier, autant euh le langage des propositions, il est bien structuré, euh le langage des preuves, il est assez bordélique, quoi. Au mieux, il y a des euh il y a des tirets qui sont regroupés, quoi. Euh et donc la question, c'est est-ce qu'on peut se passer de ce niveau-là? Est-ce qu'on peut faire les preuves euh juste en bougeant, en agissant sur les propositions? Et le fait est que sur le tableau mathématique euh la plus grande partie du texte c'est des propositions. C'est peu de choses sur les sur les preuves. Euh par contre, il y a un truc qu'on fait, c'est que on peut montrer au tableau, hein, on a le doigt. On peut dire ici, il y a des occurrences, on peut indiquer des occurrences dans le texte. En ayant ça en tête, on va essayer de faire quelque chose. Pourquoi est-ce qu'on écrit une proposition? Bah, il y a quand même deux cas. Il y a deux statutes pour la proposition. Soit c'est pour dire je vais prouver ça, soit c'est ce que je sais. Ce que je sais c'est je réénonce le lem ou c'est une hypothèse. Et puis après, il y a montrer que ça, je dois le montrer. Ce qu'on va faire c'est qu'on va utiliser un code couleur. On va dire que en bleu, on va écrire ce qu'on sait et en rouge, ce qu'on veut prouver. Alors euh on va essayer. Donc ça c'est l'exemple Socrate. Alors là c'est un transparent. Donc là je suis en rock. Là c'est aujourd'hui je suis en en rock en VS code. Donc j'ai énoncé en gros le truc de Socrate et puis là j'ai fait j'ai appelé ACEMA. Donc la commande de preuve c'est j'appelle l'interface Aktema et du coup maintenant en fait ça donne la main à l'interface. C'est assez grand là les caractères. Vous voulez que j'agrandisse? C'est bon. Est-ce que je peux cacher ça? Ouais. Bon bah là, on est dans la même situation que que Aristote. On a quand même un avantage sur Aristote, c'est qu'on a la souris et là je peux les bouger. Et donc ce que je vais faire, c'est que je vais par exemple essayer d'amener ici mon hypothèse tous les humains sont mortels sur Socrate est mortel. Donc là, j'ai juste amené pour l'instant je tiens la souris. Donc il se passe rien, mais il voit quand même que il y a une interaction possible. Donc qu'est-ce qu'il est en train de dire? Il est en train de dire "Oui, on peut essayer de prouver. On peut agir sur le but en utilisant cette hypothèse en gros en superposant mortel de X avec mortel de Socrate. Donc qu'est-ce que je fais là? J'utilise ça. Donc le système il dit bah ça veut dire quoi? Ça veut dire là, c'est moi qui commente X dans ce cas c'est Socrate. Et donc quand je vais lâcher, il va dire bah oui, tu peux montrer que Socrate est mortel à condition maintenant que tu montres que Socrate est humain. Alors donc le Socrate est humain, il vient évidemment ici du euh X est humain ici. Et ensuite bah ça c'est bon parce que là le je l'ai en hypothèse hein. Donc en gros là, on a l'idée que alors en anglais ça se dit bien parce que alors je sais pas dans l'hypothèse où ce un tel outil est est généralisé, utilisé, comment les gens en parleront plus tard, mais il y a un peu l'idée que euh en anglais, on dit evidence, c'est pas l'évidence euh en français, c'est euh le matériel de preuve. hein, c'est comme au tribunal. Bah là, evidence, c'est en bleu et on l'amène là où on en a besoin en rouge. Pardon? La pièce à conviction. Voilà, la pièce à conviction. Exactement. Et alors là, je vais le refaire dans l'autre sens parce qu'il y a un truc pourquoi est-ce qu'on a tendance à faire les preuves à l'envers là en top down dans les systèmes de preuve? Je sais pas pour diverses raisons, mais il y en a peut-être une, c'est que alors ici, il y a toujours un seul truc rouge, c'est un peu idiot, vous pouvez en avoir plusieurs mais bon euh c'était un choix de design qu'on a fait au début. Mais en tout cas, quand on a des hypothèses ici, vous voyez que là, j'ai pas comme je les montre, comme je les bouge, j'ai pas besoin de leur donner des noms comme dans le système de preuve dans la version textuelle. Et du coup, je peux facilement faire interagir des choses. Et là, par exemple, vous voyez le fait que Socrate est humain, je peux le faire interagir avec le human de X ici, hein. Et donc quand je fais interagir deux objets bleus, qu'est-ce que je vais faire? Bah, je vais Oh, il y a un petit bug là que ça reste rouge, hein, ça veut rien dire. Bah là, j'ai créé une nouvelle preuve, cette fois que Socrate est mortel. Et là, bah là, c'est bon. En fait, j'ai aussi un truc que je peux double cliquer sur dans si j'ai le bon truc, mais vous voyez là le là dans ce cas-là, est-ce que j'amène le bleu sur le rouge? Le rouge sur le bleu, c'est pareil, ça marche. Donc j'ai fait ma preuve. Donc là, je l'ai faite cette fois en mode forward. Et donc ça crée la preuve en rock après. Ouais, ça crée la preuve en rock. Alors là, c'est des exemples un petit peu bêtes euh mais qui montrent des choses. Euh donc quelque part euh il y a au départ l'idée de d'être intuitif euh et de pas avoir besoin de se rappeler des noms des commandes. Mais il y a quand même un avantage qu'on a, c'est que on montre les objets et c'est pas juste que je monte tel objet. À la limite, je pourrais dire c'est l'objet numéro 1, numéro 2, mais je monte des endroits dans l'objet. je le dépose à tel endroit ou à tel endroit. Et ça c'est un truc qui coûte cher en mode textuel. Euh et ça c'est intuitif et c'est pour ça que je dis au tableau, je peux montrer ça. C'est quand même un truc dans quand j'explique, c'est pas mal. Et donc là, qu'est-ce que j'ai? J'ai je veux montrer A alors que je sais A et B. Bon, c'est évidemment vrai. Euh mais les choses dont j'ai pris conscience en utilisant ça après euh les outils habituels. Donc évidemment c'est automatisable, d'accord? Mais quand on le fait à la main, euh bah les règles elles parlent du connecteur à la racine. Donc ici, elle voit que le E. Elle voit pas le A, elle voit le E. Donc il faut commencer. Donc ça ça serait la manière habituelle de casser le E. Donc là, je peux le faire hein en double cliquant et ensuite j'amène le A sur le A. Mais alors quand je fais des backtracks, ça tire un peu. Voilà. Mais là, je peux dire bah oui, j'ai une preuve de A et B, donc ça ça peut me servir à prouver. Donc je peux le faire directement comme ça. Euh làà, il est pas content parce que euh parce qu'il y a eu le backtrack. Donc, ça c'est dans cette version là. C'est mal implémenté. C'est pas grave. De toute façon, on se fiche de la preuve. Euh là, par exemple, qu'est-ce qui se passe? Euh j'ai B et je dois montrer C et A ou B. Donc là, qu'est-ce qui va se passer? Bah, c'est assez intuitif, hein. B, je le prouve. Donc A ou B, il est prouvé. Donc, le A ou B, il disparaît. Par contre, le C il reste. On se ramène à C. Voilà. Après là, si j'ai pas plus d'informations, je peux pas continuer. Mais euh voilà, donc il y a différents trucs. Euh alors, il y a d'histoires avec les quantificateurs qui sont un peu euh marrants, mais là, on va peut-être faire euh autre chose. Je vais montrer un peu des trucs avec l'égalité. Donc là, c'est trivial, hein. C'est juste pour montrer déjà comment ça marche. Euh, j'ai X et Y et je veux montrer la symétrie. X = Y implique Y = X. Euh donc, la manière don en rock, c'est on utilise l'égalité pour remplacer Y par X ou X par Y dans le truc rouge et puis après on se ramène à la réflexivité. Euh donc là, ce que je peux faire quand j'ai quand j'ai un une preuve d'égalité, ben je peux m'en servir pour remplacer l'un par l'autre. Donc j'amène le Y sur le Y ou le le X sur le X. Euh et là quand c'est de la réflexivité, en gros la la preuve canonique euh c'est double clic. Donc je double clic et voilà. Euh donc là, j'ai fait la preuve. Transitivité. Transitivité, c'est pareil. Du coup, on la garde. Euh alors, je voulais faire un truc. Alors, ça c'est marrant parce que c'est vraiment un truc de mon cours de sup. Je ça m'avait frappé de ma sup donc il y a longtemps et c'était joli. Puis là, je m'en suis je dis bah voilà. Alors pourquoi je le fais? Parce que bon, c'est pas très dur mais parce que c'est on n pas besoin de de beaucoup d'hypothèses. Donc c'est sur n mais en fait ça pourrait être sur n'importe quoi F et ça pourrait être d'un ensemble vers un ensemble. Donc on a deux applications, enfin de Oui, deux applications F et G. Et euh ici pour tout et F c'est l'inverse à gauche de G, c'est ça? F de G de Y, c'est Y. Donc F est l'inverse à gauche, un inverse à gauche de G et G est surjectif. Et on va montrer que du coup G est l'inverse à gauche de F. Alors comment on fait? Comment on fait? Bah on dit OK soit X. Donc soit X, ça veut dire je casse le pourt- clique et là il me dit OK, soit X ici. Et euh si puisque j'ai X, j'ai un antécédent de X. Alors là, le truc c'est que quand j'ai un pour tout bleu, je peux dire ben instancil X par ça, instancil le X par X. Donc du coup voilà, j'ai là et puis quand j'ai un il un y un il existe bleu, ben je peux le casser en double cliquant dessus. Donc là, j'ai le Y et j'ai le Y = X. Et comment on finit? Ben on dit enfin on finit, on fait bah là X c'est G de Y. Pourquoi on a fait ça? Bah c'est pour avoir f de g de Y. Donc là, vous voyez qu'il est quand même rusé parce que il comprend que le Y bleu, c'est le Y rouge, hein. Il fait les bonnes instanciations sinon il refuserait. Et donc il va remplacer f de Y par y. Et là bah c'est exactement l'hypothèse que j'avais. Donc là j'ai trois manières de le finir. Comment je peux faire? D'une part c'est la même chose. Là le rouge et le bleu, c'est la même chose. Donc je peux amener toute la proposition dessus. Mais je peux aussi euh remplacer GY par X et puis faire la réflexivité ou X par Gy. Yy. Alors, juste pour montrer, si je double clique là sur l'un des deux, il va remplacer tous les Gy par des X. Il y en a qu'un seul, mais euh voilà. Et là, j'ai fini. Je pose une petite question. Ah, il revoit que c'est le Y. Euh, il y a un renommage. Si vous les avez appelé Z, vous avez qualifié sur Z ou Ouais. Ouais. On peut Qu'est-ce qu'on peut faire? On va on va mettre un Z ici peut-être comme ça. Alors avec les noms, il y a il y a sûrement des cas où où ça fait des trucs. Alors là, qu'est-ce qui se passe là? C'est bon. Euh donc qu'est-ce qu'on veut faire? On veut remplacer Z par GY. Ouais, je sais pas si ça répond à ta ton truc, mais a priori ça marche, hein. Euh mais il peut y avoir des cas où il y a des trucs qui se qui se qui se collide. Alors, je peux faire ce truc-là qui est un exemple un peu il est un peu extrême. Je dis pas que c'est le truc le plus intuitif, mais c'est un peu rigolo pour donc quelque part derrière, on essaie d'avoir des trucs intuitifs et quelque part, je suis content que vous disiez vous m'ayiez pas trop interrogé sur quel comment ça fonctionne, comment il choisit de faire les choses mais c'était pas évident de trouver la bonne manière de faire. Et en fait, on a eu du j'ai enfin eu du bol parce que moi j'avais cette idée d'interface et en fait je me suis rendu compte que au bout du couloir en fait c'est maintenant l'équipe à laquelle j'appartiens. Il y a des gens qui avaient exactement les bons outils logiques pour décrire la manière dont ces ces trucs rouge et bleu ou bleu et bleu interagissent pour pour aboutir à une nouvelle une nouvelle conclusion ou un nouveau but. Là ici j'ai un truc. Donc qu'est-ce que j'ai? Je sais que il existe x qui est l'antécédent de tous les y. et je dois montrer un truc plus faible qui est pour tout a il a un antécédent. Donc là du coup bah ça marche direct en fait les les règles vont faire que donc le but c'est pas d'automatiser en général ici tout ça c'est vraiment de contrôler de contrôler ce qu'on fait mais de le faire de manière confortable mais là ici ça va les les quantificateurs il s'instancil les uns les autres et ça résout le truc directement et par contre si j'inversais les les deux Là, bah là, il refuserait de de superposer les deux R sans rentrer trop dans les détails. Euh ouais. Donc, c'est capable après de sortir la preuve en rock. Ouais. Mais en fait, est-ce que c'est il est-ce que la preuve en rock c'est vraiment ça suit ce qu'on a fait la souris? Par exemple, si on fait des trucs pas pas du tout optimal, on passe au temps à faire des substitutions un peu cycliques, un peu est-ce que finalement la preuve sortie à la fin, elle suit exactement ce là. Là, quand je dis c'est un prototype, c'est vraiment un prototype. Donc les c'est pas c'est pas si facile de simuler euh de fabriquer la preuve en rock. Il y a il y a un certain travail, il y a des trucs qu'on peut faire. Alors ça marche pas toujours, mais par exemple, on peut euh pour ceux qui ont l'habitude des des trucs comme rock euh quand on utilise une égalité, un rewrite, mais pour réécrire en dessous d'un quantificateur euh c'est pas c'est pas possible, il faut utiliser des outils plus compliqués. Là, naturellement, ça passe en dessous avec les règles. Je je vais en dire je peux en dire deux mots tout à l'heure. Euh donc là, pour l'instant, les preuves, si on les regarde, on a juste le terme preuve, c'est très très moche. Euh donc clairement, il faut euh donc là, on rajoute des trucs, il faut essayer de garder une trace de la preuve telle qu'on la fabrique avec les actions. Et après, il y a tout un tas de trucs qu'on peut vouloir faire. On peut vouloir fabriquer des vidéos où on peut refaire le truc. Euh, on peut avoir, on a envie d'un texte qui est lisible. euh qui peut être rejouable de manière simple pour le système mais aussi éventuellement je sais pas une sortie en langue naturelle ou des trucs comme ça. Donc il y a tout un tas de trucs parce que effectivement il reste plus rien. C'est c'est c'est pratique même pour à la limite pour faire on peut imaginer pendant un exposé mais après il reste plus la trace de la trace des actions. Donc et là il y a un boulot à il y a un boulot à faire. Euh j'ai montré, je vais peut-être pas le faire en entier mais il est il est il est marrant parce que je manque donc ce dont on manque. Oui. Je disais juste chacune des actions que que vous faites avec la souris correspond pas à une tactique de coque de Alors en gros c'est une c'est c'est pas une tactique existante. Il a fallu écrire des tactiques spéciales et ces tactiques, elles prennent en argument euh les occurrences en disant "C'est à tel endroit, c'est à tel endroit." Mais mais on peut pas imaginer pour pour une action avoir une suite de de tactique correspondant euh dans un certain nombre pour un certain nombre d'action, c'est pas si facile. Ouais, mais évidemment, on va pas enfin tout ce qu'on prouve est prouvable en rock avec des tactiques habituelles, mais le passage de l'un à l'autre est pas est pas si évident. Euh et là là je peux en montrer un où il y a des des implications un peu rigolotes. Donc c'est un exemple euh c'est un exemple un petit peu idiot mais ça vient d'un truc qui s'appelle Educera qui avait fait un truc une espèce de version un truc au-dessus de rock pour l'éducation. c'était avec certaines bonnes idées mais ils ont pas l'éducation nationale elle elle finance pas des logiciels et donc ils ont pas ils ont pas réussi à vendre donc on est dans une dans un monde où il y a des des gens qui ont chaque personne a une mère et les personnes peuvent être riches ou pas euh les personnes sont de type entier naturel là ils sont de type entier naturel parce qu'il fallait choisir un type mais ça ça aurait pu être autre chose. Et en fait ça ça peut pas ces deux hypothèses sont pas compatibles. Donc on va montrer faux que quand une personne est pauvre la mère est riche et puis que pour toute personne soit la personne est pauvre soit la grand-mère est pauvre. Donc ces deux trucs sont incompatibles. S'il y a aucune intuition c'est juste que ça marche pas. Mais par contre dans la preuve, le fait de faire la preuve avec ça, je trouve que ça ça c'est assez rigolo. Et puis il faut qu' pour que soit pour que ça marche pas, faut qu'il y ait quand même au moins une personne parce que sinon s'il y a personne, il y a pas de problème. Donc ce qu'on va faire, c'est qu'on va dire bah la personne on va regarder, elle est soit elle est pauvre, soit la grand-mère est pauvre. Euh donc là, j'ai ça et puis maintenant je double clique sur le ou et là j'ai deux en fait j'ai deux trucs. J'ai voyez j'ai deux onglets. J'ai le cas où c'est la grand-mère qui est pauvre et le cas où c'est John qui est pauvre. Alors quand la grand-mère est pauvre, ben l'arrière- grand-mère est riche. Et c'est là que c'est rigolo. Et c'est là que c'est quand même plus pratique que dans le truc avant. Donc là, je vais amener le fait que cette arrière-gr-mère est riche ici. Ce truc dit pour tout X, soit la grand-mère de X est pauvre, soit X est pauvre. Donc qu'est-ce qui se passe ici? X c'est quoi? C'est la mère de John. Donc je contredis la branche là, l'arrière-gmère de John est riche. Et du coup, qu'est-ce qui va me rester? Et pauvre. Et là, bah je dis bah oui, mais si la mère est pauvre, la grand-mère est riche et là j'ai la contradiction sur le statut, le truc. D'accord. Vous avez compris ce qui se passe quand il y a une contradiction, bah ça disparaît. Donc là, il me reste que l'autre. Alors, il pourrait y avoir un truc qui disent on a résolu l'onglet, maintenant l'autre onglet. Alors, l'autre, c'est la même chose. C'est juste un tout petit peu plus long parce que au début on a le fait que la mer est pauvre. Alors là, du coup, je peux pas. Voyez, en fait, le truc c'est maintenant, on a compris ce truc là. Cette disjonction, elle permet d'enlever niveaux de mover mais ici, ça marche pas. Donc, on est obligé d'aller là. Et du coup, on va remonter de tr niveaux. Du coup, c'est l'arrière arrière grand-mère qui est riche cette fois. Mais si l'arrière arrière-gr-mère est riche, on va enlever deux mother. Donc c'est la grand-mère qui va être pauvre. Si la grand-mère est pauvre, qu'est-ce qui va se passer? La l'arrière grand-mère va être riche. Donc ça va contredire ça. Alors, je peux essayer de faire un truc rigolo là. Si vous avez suivi sinon, c'est pas grave. Mais je peux dire euh donc là je vais contre le truc le but pédagogique que tout est confortable mais on peut c'est pour dire que donc c'est très très piégeux ça d'accord parce que ça ça on a envie de jouer avec le truc et c'est moi qui joue et vous regardez et je sais bien que que c'est mais là qu'est-ce qui se passe? Je dis que le fait que l'arrièreg l'arrière-g-mère est pauvre, ça va contredire le fait que mother de X est riche. Donc ça va me demander de montrer que la grand-mère, elle est pas pauvre. Non. Non. Et ça euh et ça et ça et ça. Ben non, c'est pas ça que je voulais. Celui qui Ah bah si, voilà, il est là. Oui, c'est exactement ça que je voulais dire. Oui, c'est ça. Il est là. Voilà, il est là. Donc, on a bien la contradiction. Donc là, je le fais dans un ordre différent, mais c'est la même chose. Et j'ai euh et j'ai fini la preuve. Alors, j'ai montré deux trois trucs euh qui sont moins euh qui sont moins rigolos. Alors, je pense que j'aurais pu trouver des exemples plus mat classique, mais là à un moment, j'étais euh je vais montrer un truc qui est très très rock dans l'esprit, d'accord? Mais juste on va refaire un tout petit peu des tout petits trucs de calcul. Ah oui, pardon. Al, du coup, faut que je montre euh qu'est-ce que j'ai fait là? J'ai défini ici euh comment je fais là ici là. J'ai défini une fonction qui prend deux entiers une R là zéro successeur et qui rend un boulé 1 en gros qui teste l'égalité. D'accord? 0 c'est c'est vrai. Successeur successeur ben je m'appelle récursivement en enlevant les successeurs et tous les autres cas qui sont zéro successeurs et successeur zéro. C'est faux. Et je vais montrer que ce trucl est réflexif. Donc du coup bah là il faut le faire par récurrence. Donc je peux sélectionner une proposition, un bout de proposition. Là toute la proposition, je vais faire une récurrence. Donc là comme c'est un truc qui commence par un pour tout, ça veut dire que la récurrence, elle est sur le n. Donc j'ai de kn = 0 et puis l'autre ça va être successeur. Alors là ce que je peux faire, vous vous rappelez le simple là, le truc qui dit calcule, calcule tout ce que tu peux. Bah là, je peux dire calcule tout ce que tu peux ici. Bon, je pourrais le faire partout mais en fait ce qui est important, c'est juste là sur ce truc-là parce que c'est quoi ça? C'est ça. Ça se calcule vers vrai 00. Donc je fais simple vrai vrai. Vous voyez que c'est pas beaucoup automatisé. Je double clic et c'est bon. Et dans le cas successeur ici, bah ça va faire quoi? Ça va se réduire vers l'appel récursif. Donc c'est la même chose et là c'est comme tout à l'heure, j'ai soit je dis c'est la même proposition, soit je réécris. Bon voilà donc là c'est bon. Donc là je l'ai montré. Alors je vais faire une autre qui est un tout petit peu plus compliqué mais après j'arrêterai l'épreuve. Euh bah là en gros, c'est le contraire. Je montre que quand le test est vrai, alors ils sont égaux. Donc c'est pareil, c'est par récurrence. Alors il y en a deux du coup. Alors c'est par récurrence sur le premier. et je montre par récurrence sur le premier que pour tout m qui et cetera. Alors du coup ici je peux je suis pas obligé de refaire une récurrence mais faut quand même que je regarde c'est que zéro au successeur. Donc je fais juste un cases euh 0. Bah oui 0 = 0 c'est bon. Donc là je je casse l'implication et je fais ça. On pourrait imaginer qu'on puisse le faire directement. Voilà. Alors ici qu'est-ce qui se passe? On est dans le cas zéro successeur. Bah oui, zéro successeur, ça se calcule vers quoi? Ça se calcule vers le boulet info. Donc l'égalité, ça va se calculer vers tr égal false. Alors là, il y a un minimum d'automatisation, c'estd que quand on a des trous égal false qui apparaissent, le but va disparaître. Donc là, je dis juste de calculer et le but disparaît, hein. Et là, on est dans le cas successeur. Il faut à nouveau faire un cas sur M. Ici, c'est pareil. C'est trivial parce qu'on a cette hypothèse qui est qui est absurde. Et dans le cas ici là, il y a juste un calcul qui se fait ici, les successeurs disparaissent. Et ce tru là, bah je peux utiliser l'hypothèse de récurrence sur n cette fois, hein. Donc là, je dis bah oui, voilà, c'est bon. Là, j'ai ça, hein. Alors, encore une fois, il y a quand même un truc qui se passe, c'est que ça instancie le le pourt m par m par le m du contexte. Et du coup, j'ai n é= m. Et là, pour le coup, je dois me servir de l'égalité, hein. C'est pas juste un truc, je dois remplacer l'un par l'autre et je finis. Donc cette preuve, elle est extrêmement routinière mais en même temps, c'est typiquement le genre de preuve qu'on fait beaucoup beaucoup en rock. Alors soit sur des trucs au début quand on leur apprend le système hein. Euh mais ensuite le schéma de preuve récurrence un peu de calcul des raisonnements par cas, c'est un truc qu'on fait beaucoup. Donc là on pourrait faire par exemple prouver la correction d'un programme de tri assez assez facilement. Donc en gros, ouais, on arrive à faire un un début de cours avec ça. Euh je vais euh revenir au transparent. Oui. Alors là, on s'en fiche un peu. Ça, je l'ai dit. Donc ça c'est ce que je voulais dire mais je vais pas je vais pas le détailler. C'est que on a de manière abstraite identifié on avait déjà ça dans le le calcul dans le le travail d'un collègue là Costum Chodury qui explique le comportement du drag and drop. Donc en gros si j'amène le B ici là sur ce B là comment ça marche? Il y a des règles qui décrivent comment les deux items là interagissent, se déstructurent et on arrive à la conclusion. En gros, le B là, il est remplacé par un trou et puis après il y a une simplification, on arrive au résultat. Donc il y a des bases logiques. Les quantificateurs, je vais pas en parler, on a un peu intuité le truc. Je voulais juste dire un un certain nombre de trucs. Euh donc en gros quand on montre ça, en général tout le monde trouve ça chouette puis après les gens il ils retournent à leur travail quotidien. Euh je pense personnellement que donc il y a le un un bottle un un goulot d'étranglement, c'est le travail de développement. C'estàd que ça demande, on veut un truc qui qui soit robuste, qui soit euh qui soit bien fichu et ça demande quand même de s'interfacer avec des trucs assez divers entre une interface graphique d'un côté qui rentre dans les termes et ces termes c'est des termes rock même s'ils sont ils ont été traduits un petit peu. C'est pas c'est pas si c'est pas si facile et il faut le faire bien. Moi je pense que un tel système il serait utile même à des experts de preuv formelles. Mais bon, les experts ou les gens qui font ça d'habitude, ben ils ont leurs habitudes et puis sont ttuus. Donc on verra. Euh j'aimerais bien l'avoir pour enseigner rock. Moi aussi j'enseigne rock à des étudiants de 2e année, hein. Michel en a parlé. Effectivement, ça marche bien. Je pense que ça leur fait du bien. Et est-ce qu'est-ce que ça ferait aux étudiants? Je je suis curieux. Euh et clairement pour les mathématiciens, des mathématiciens euh euh professionnels, bon avec un produit mieux fini, je pense que ça pourrait être intéressant et ça me permet de rebondir sur un truc que je voulais dire en en voyant le l'exposé Line euh le ce qu'on voit là dans le les bibliothèques liges et les tactiques qui qui vont avec c'est que il y a un moment on arrive à avoir suffisamment alors est-ce que c'est de l'automatisation mais c'est aussi du carrossage des théories et cetera pour que on arrive à faire ce qu'on veut de manière raisonnablement simple sans sans rentrer dans trop d'arcane hein. Et donc je pense que clairement là il faudrait aussi ce genre de chos en particulier. Il faut des bibliothèques parce que on veut afficher les trucs, on veut que les les notions de sous-terme elle elle elles fassent ce qu'on veut pour des des écritures non non trivial. Donc il y a il y a beaucoup de choses à faire. Et pour l'enseignement, c'est peut-être le truc qu'on pourrait faire le le plus vite, y compris un niveau secondaire. Euh mais il y a aussi beaucoup de travail à la fois de de rendre le truc robuste. Mais je pense il faut identifier des avant les corpus. Il faut identifier à la fois des corpus d'exercices qui font sens. mais qui chacun fonctionne avec un certain comportement du système. par exemple euh c'est sans doute pas le le je suis pas sûr que ce soit la meilleure idée mais dans un premier temps, on travaille, on explique la commutativité et une fois qu'ils ont compris que la commutativité, on peut faire tel ou tel truc, mais à ce moment-là, on on autorise un machin qui fait que quand on a une expression algébrique avec un truc commutatif, on peut bouger le on peut bouger un des termes et le le remettre à l'endroit qu'on veut. chose qu'on peut pas faire pour l'instantin. Euh donc voilà, il y a des euh il y a il y a des euh moi je sais pas, je trouve qu'il y a il y a beaucoup de choses à faire. Euh après, le truc c'est de trouver un cadre qui permet de développer un produit parce que là on est dans un truc où il y a de la recherche mais il y a pas que de la recherche. Et voilà. Bah j'ai écoutez, j'arrête là. Si vous êtes intéressé, vous avez des questions là-dessus, moi je suis même d'en discuter plus tard, je serai évidemment preneur. Voilà. Merci. Il y a-t-il des questions? Oui. Oui. En fait, c'est presque ça paraît presque trop ludique et donc le le risque pour les étudiants, c'est de voir des étudiants qui joueraient un petit peu avec ça en essayant de pas faire matcher des choses avec d'autres sans rien comprendre euh sans avoir une structure logique derrière et en se disant en faisant des choses comme ça, finalement il y a peut-être des choses qui vont apparaître et et je vais obtenir quelque chose qui va fonctionner. Et est-ce que tu as vu ce genre de chos des défilants? Al c'est c'est peut-être aussi quelque chose qui se passe avec Rock parce que il parfois il teste peut-être plein de tactiques un peu n'importe comment en espérant que quelque chose va produire. Excusez-moi, je pense j'ai tendance à penser que ça risque d'être un peu comme avec Rock. Effectivement, c'est qu'au bout d'un certain temps, on se rend compte que pour des trucs compliqués, il faut réfléchir. Euh après, il y a il y a une question euh là, j'ai j'ai pas de réponse euh au-delà des étudiants. C'est que pour des dès qu'on rentre dans des trucs un petit peu compliqués, quand on fait une preuve formelle, même si le le l'approche top down donne l'impression que le système va aider à faire la preuve, au fond, il faut avoir compris la preuve, à part certains cas particuliers. Si on si on cherche la preuve en formalisant, en général ça se passe mal. Est-ce que là un jour on aura un truc, on a une espèce de si on fait de la science-fiction, une espèce de tableau noir intelligent où on cherche et en même temps il il vérifie que ce qu'on est en train d'écrire c'est c'est possible. Or, il dit ça, je suis pas sûr. Des choses comme ça. Donc où on a à la fois de la vérification en même temps qu'on cherche, ça me paraît pas impossible mais on en est pas encore là. Et après pour les étudiants, je pense que c'est ce que je disais, je pense que de toute façon on voudra contrôler à chaque fois leur donner des outil pour qu'il y ait le bon niveau disons de de ludicité. Hm. Mais euh ouais, c'est difficile de prévoir. Moi, j'arrive pas à visualiser tout ce qui peut se passer. C'est juste de c'est qu'effectivement le fait d'avoir gardé la trace va être important d'avoir une sorte d'onglet ou ça ça c'était une bonne idée ce que tu as fait là et puis là là tu as fait deux fois tu as fait un meilleur tour là. Ouais donc c'est des trucs très simples faire des choses comme ça parce que Oui ça c'est une bonne idée aussi le fait de d'envoyer du feedback indépendamment de l'ordre. Oui oui. Ouais. Moi je crois c'est ce que j'aimerais pour mes élèves ça serait que les choses restent affichées. J'ai un pour tout je clique et là il écrit soit en toute lettre il me fait comme moi je fais moi au tableau je je parler debout et je leur écris ah et là et on doit montrer un et que ça reste affiché. Alors ça fait un peu grand mais on peut scroller et que la étapes restent restent là. ou seisse sur un anglais différent. Si on sait faire le si on fait un truc qui fait un output en langue naturelle, déjà quand c'est fini, c'est une chose mais après effectivement on pourrait l'afficher petit à petit en disant ici faut montrer ça quoi. Ouais. Oui, c'est pas mal. Et euh ça a été essayé sur des preuves un peu plus grosses parce que là il y a quatre trucs à bouger mais c'est à 25000 quand on prend des trucs il y a il y a déjà il a du mal à au début il allait pas à la ligne donc déjà on était coincé euh quand il y a des gros trucs si on fait le programme de tri par exemple déjà à un moment c'est c'est affiché de manière un peu gross Donc il y a il y a tout un tas de questions autour de ça qui se posent. Ouais. Euh et après je pense que sur certaines preuves plus réelles, c'est plus dans des preuves informatiques, enfin comment dire sur des objets plus informatiques. Souvent il y a des trucs on a beaucoup de cas. C'est qu'au lieu d'avoir juste zéro successeur, il y a il y a toutes les constructions d'un langage de programmation, les instructions d'une machine. Euh et alors par exemple, d'ailleurs, j'ai pas dit ça mais pour les cas de couleurs, George Gontier, il a développé tout un ensemble de tactiques, un langage qui est utilisé dans Matom qui s'appelle SS Reflect. Euh et justement l'une des motivations de SS Reflex, c'est dans ces cas-là euh de on peut rajouter un petit truc derrière à la fin de la ligne qui va traiter tous les quatre riviaux et du coup on arrive au lieu d'avoir 25 K et qu'on traite à la main, bah on on tâonne un peu et puis après on a une instruction, il y a les 25 cas qui vont partir d'un coup et on on reste sur le cas important. Euh bah ça il je va pas rentrer dans les détails techniques mais comment on ferait ça avec un truc comme ça? C'est c'est pas si clair. Faut faut faut réfléchir. Euh et donc là si on a 25 onglets, c'est c'est pas c'est pas joli. C'est pas on va être textuel. La fin. Merci. J'ai juste une dernière question, c'est on a parlé plusieurs fois du tiers exclus depuis et euh donc là, j'ai l'impression quand tu utilises, c'est par exemple parce que le fait qu'une grand-mère soit riche ou pauvre, c'est décidable. Non, euh le euh en fait, on se sert pas du fait que c'est riche ou pauvre, mais on sait que le ou c'est juste Non, on a pas besoin du tir exclu là. Le où c'est juste euh c'est juste sur que soit X et riche ou pauvre, je sais plus et ou la grand-mère est pauvre. Ah donc la tactique case elle décompose juste le alors le le case c'était le case c'était sur des objets qui sont soit zéro soit successeur et ça c'est décidable ou euh et sinon sur un ou d'accord. Par contre, il y a un truc, ça c'est dommage. Alors ça je regrette parce que en fait quand on présente la logique classique, on le fait avec des séqu avec ce ce signet un peu bizarre mais il y a plusieurs il suit qu'on est plusieurs conclusions. Et la manière dont on montre le tir exclu dans ce cas-là, je veux montrer A ou non A, il y a une règle qui dit ben ça, je peux le déduire de ce trucl de montrer soit A, soit non. Et euh et là donc noir c'est a implique faux. Et quand on a une implication qu'on veut montrer dans un truc comme Aktema B, on double clique dessus. Et le truc qui rend la logique classique classique, c'est que quand on fait ça, bah le a il devient une hypothèse là. Donc, faudrait qu'il soit bleu. Et en logique classique, on a plusieurs conclusions et du coup le ce qu'on a sorti de ça, bah on peut l'utiliser pour prouver ça. D'accord? Donc, il suffira d'autoriser deux trucs rouges et là, on aurait la logique classique. Et euh alors je savais qu'avec plusieurs conclusions, on avait la logique classique, mais je l'avais jamais visualisé comme ça euh depuis que que quand il y a il y avait ce truc. Ça avec deux trucs rouges mais il suffit d'en prouver l'un. Deux trucs rouges. On en prouve un seul. Ouais. Oui, on en prouve un seul. Le la logique classique, c'est que la présentation logique classique en calcul des séquences, c'est que on a une liste d'hypothèse, une liste de conclusion et c'est ça. Ça veut dire que tous ces trucs là, ça implique un de ces trucs là. Ouais. Bon après je sais pas je sais pas et après je sais pas pourquoi les est-ce que les systèmes de preuve ils sont naturellement avec une conclusion parce que ils ont été faits par des gens qui aiment la logique intuitionniste ou parce que quand on a plusieurs conclusions ça va c'est plus c'est plus fatiguant parce qu'il faut à chaque fois qu'on fait un truc faut dire je je travaille sur la conclusion 1, la conclusion 2, la conclusion 3 ou la conclusion A B ou Cici puisqu'on la montre onindique Voilà, je pense qu'on peut remercier.