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

Voilà. Merci beaucoup Pascal, merci beaucoup euh Guillaume je suis vraiment très content de de pouvoir vous vous parler. J'espère que je vous apporterai quelque quelque chose. Euh donc oui, je suis euh prof à l'école polytechnique mais j'ai fait longtemps ma carrière à l'INRIA et je suis à nouveau dans une équipe Inriia. Le titre, la la part du calcul, je l'ai emprunté à à notre collègue Gilow qui est décédé cet été euh qui sur la fin était un peu fâché avec moi, mais ça ne retient rien à ses ses grandes qualités scientifiques et surtout c'était un pédagogue et un communicateur hors paire et c'est lui qui avait trouvé cette formule, je crois c'était pour son habilitation à diriger des des recherches euh sur euh cette question du calcul dans les dans l'épreuve. Alors, de quoi je vais essayer de vous parler aujourd'hui et demain? Euh donc deux preuves dans lesquelles il y a du calcul, des preuves qui sont formelles, qui sont formalisées essentiellement en rock. Donc je vais essayer d'expliquer les principes mais là on a déjà parlé ce matin. Puis je veux prendre deux exemples euh qui sont des exemples assez concrets et euh où le premier vous serez certainement beaucoup plus à l'aise que moi sur des preuves de de primalité et puis le théorème des quatre couleurs. C'est Alain qui m'a dit que ça serait bien d'en parler et ça me ça me fait plaisir. C'est toujours quelque chose de d'attant. On le carré vert là sur le ça veut dire qu'on rate quelque chose sur le zoom ou le carré vert normalement représente ce que vous partagez. Ouais, je sais pas pourquoi j'arrive pas à partager plus. Bon, on va il vous dérange pas trop hein? On va faire avec euh le théorème des quatre couleurs. Donc là, je vais essayer de voir pourquoi on a besoin de calcul dans cette preuve. C'est quelque chose qui est toujours assez amusant. Je pense que je m'arrêterai aujourd'hui euh au milieu des quatre couleurs et on reprendra demain pour la partie la partie calculatoire. Et dans une dernière partie, je voudrais parler de quelque chose d'assez différent euh qui est une nouvelle interface, quelque chose sur lequel je travaille, des idées pour une nouvelle interface pour construire des preuves en rock euh de manière qui est peut-être plus intuitive ou plus amusante. Et là, de ce point de vue-là, je suis curieux de voir ce que de voir ce que vous allez en penser euh puisque vous êtes en au contact vraiment de l'enseignement et des mathématiques. Alors, néanmoins avant, je vais faire un petit peu de contexte sur les sur les preuves formelles. Je vais essayer de d'être rapide, hein. En plus, on vous a déjà parlé de de logique. Mais euh sur le rapport entre la logique, la déduction, le raisonnement mathématique et le calcul, il y a des choses qui remontent assez loin. Je trouve que c'est amusant de le regarder. Oui. Est-ce que tu pourrais juste faire en sorte que les deux cases en haut soient OK pour ces conditions qui ont été enregistrées et augmenter le volume? Si elles peuvent disparaître, ce sera mieux pour la vidéo enregistré après. Voilà. Et puis voilà, c'est c'est mieux. Voilà. Merci. Super. Merci. Oui, je j'y pensais pas. Merci beaucoup Guillaume. Alors avant ça, je voulais faire un petit euh c'est que j'ai que le mot anglais là qui me vient disclaimer. Euh on est dans un contexte où il y a on parle beaucoup d'informatique et il y a un petit peu deux deux informatiques. Ah, je sais ce qui se passe que je reclique ici. Voilà, j'espère que là ça va marcher. Euh, il y a une informatique précise et là c'est plutôt celle dans laquelle on ancre le la question d'épreuv formelles. Euh l'ordinateur, c'est d'abord une machine qui exécute des algorithmes et qui les exécute précisément. Si l'algorithme, si le programme est bon, l'ordinateur va le faire, hein. Euh c'est tout ce qui est euh relève de quand on enseigne la programmation, l'algorithmique. Et dans ce cette partie-là, en gros, on essaie de comprendre ce qu'on veut faire. On écrit le programme et ensuite l'ordinateur donne le résultat et on le croit. On croit en tout cas que ce que nous affiche l'ordinateur, c'est le résultat de l'algorithme tel qu'on lui a euh qu'on lui a donné. Et puis on a une autre informatique qui est moins précise, hein. Donc en gros, je mets là-dedans le big data, l'IA et ces choses-là. Je suis pas du tout en train de faire un jugement de valeur entre les deux, hein. Mais disons qu'on est dans euh c'est un petit peu dans l'autre sens, on fait tourner des algorithmes aussi, mais souvent sur des données qui sont tellement complexes qu'on sait pas exactement ce qui va se passer et puis après on arrange les choses jusqu'à ce que ça marche, qu'on soit raisonnablement satisfait du résultat, hein. Ça peut être que le chat GTP ou autre va nous parler de manière intelligible ou ça veut être que on va vendre les produits qu'on veut vendre parce que la la publicité ciblée fonctionne, hein. Donc typiquement, c'est pas tellement que l'algorithme est pas compris, mais la plupart du temps, c'est parce qu'on est sur des données qui sont très très grandes et que qu'on comprend pas, hein. Ça peut être le big data, ça peut être les connexions entre les neurones artificiels dans des pour de pour de lire. Donc les deux informatiques se complètent, hein, les deux sont intéressantes pour ce qui nous intéresse. Mais quelque part le truc principal, nous ici, on va utiliser l'ordinateur de manière précise comme une machine, un bureaucrate sans âme un petit peu. Et pourquoi on fait ça? On fait ça pour les mathématiques. Donc ça c'est le petit transparent que j'utilise en général quand j'ai je veux expliquer ce que je fais hein. Comme l'a dit Mikaela, c'est vraiment un exemple qui remonte à Aristote. Tous les hommes sont mortels. Socrate est un homme donc Socrate est mortel. On sait tous qu'il est mort depuis longtemps. Qu'est-ce qui est intéressant dans cette phrase? He c'est le petit bout de déduction. C'est le donc ça n'a rien à voir avec qui est Socrate, qu'est-ce que c'est qu'un homme? C'est juste la syntaxe des hypothèses, on comprend bien, qui nous permet d'arriver à cette déduction. hein. Donc, on a utilisé une règle syntaxique euh parfaitement euh parfaitement précise. Le point de vue de la logique mathématique, l'idée de la logique mathématique, c'est qu'en fait c'est quelque chose qui caractérise les mathématiques, voir qui définit les mathématiques. C'est qu'une preuve mathématique correcte, elle peut être détaillée jusqu'à devenir un enchaînement comme ça de règles de règles syntaxiques. on a ces règles qui sont les briques du raisonnement euh du raisonnement mathématique. Donc cette idée, elle remonte à loin, hein. Euh on en garde ce truc, cette sensation qu'on a en cours de math que le en math la vérité, elle est mieux définie qu'ailleurs, si on veut, plus objectivement qu'ailleurs. Mais bon, c'était quelque chose qui était un petit peu là, mais sans plus. également comme la Micaela, ça a commencé à changer au 19e siècle où là il y a eu la tentative de fabriquer vraiment des formalistes, des ensembles de ces règles syntaxiques, de ces règles du jeu mathématique et de manière complète quelque chose qui permet de fonder pas juste la géométriecléienne ou l'algèbre mais vraiment toutes les les mathématiques. Donc l'un parmi les grands penseurs Russell, Cantor, Zermelo, Frankel et cetera, Fregux. Euh donc je le mentionne donc il y aurait pas mal de choses à dire là-dessus. Le le l'introduction du livre de Freegel à Begr Schrift, c'est assez étonnant à lire. c'est il y a des bouts qui sont très très modernes avec des des standards de vérification formelle qui ressemblent presque à ce qu'on fait dans l'industrie aujourd'hui. Et puis d'autres idées qui nous apparaissent beaucoup plus naïves, assez idéaliste, c'est le fait que la vérité existe, que une proposition mathématique, ça veut dire quelque chose. Donc quelque part, forcément, elle est vraie ou pas hein. Aujourd'hui, on on est revenu de ça, mais il n'empêche qu'il nous donne les outils pour euh pour ce qui nous intéresse ensuite. Alors, à l'époque, les la logique, c'est une branche des mathématiques qui a pas vraiment d'application. Les mathématiciens sont contents de savoir que leur leur raisonnement sont formalisables en principe, hein, mais personne le fait parce que détailler une preuve non triviale complètement, ça devient vite inintelligible et donc on risque de se tromper. Donc ça c'est un vrai scan du livre de Frégueux de son écriture mathématique. Alors je je le mets d'une part parce qu'on voit que bon c'est pas super intuitif mais plus que ça il y a quand même un truc c'est que cette structure arborescente. Alors pour un informaticien ça parle. Bah oui, parce que les arbres, on en a dans les ordinateurs, hein. Et de fait, les choses changent euh bah quand l'ordinateur arrive, hein. Donc ça va assez vite, hein. Les premiers ordinateurs, c'est à la fin de la 2e guerre mondiale. Euh dans les années 60, il y en a dans les dans les universités. Et donc Nick de Bry moi aussi j'ai eu la chance de le rencontrer, a été le premier à fabriquer ce qu'on appelle un système de preuve, donc un logiciel où les preuves formelles sont euh effectivement construites, hein. Ces arbres syntaxis qu'ils existent dans la machine et ils sont vérifiés. Euh donc on fabrique vraiment les les preuves formelles. Euh le système automate, il y a beaucoup de choses intéressantes à dire là-dessus, mais une chose qui est remarquable, c'est que l'architecture de ce système, elle reste toujours intéressante. Les idées sont en en grande partie encore relevantes pour les systèmes modernes. en particulier parce que il a bien identifié le fait que alors peut-être qu'il le formalisait pas si il le disait vraiment comme ça que la partie du logiciel qui vérifie la preuve donc quelque part qui est réexécuté au moment du QED bah c'est ça la partie critique c'est ça dont on a qui qui est qui apporte vraiment quelque chose parce que au début je pense que les motivations c'était bah parce que de voir si on pouvait le faire quoi he c'est comme celui qui veut monter sur la montagne parce qu'elle est là euh mais assez vite, on a vu qu'il y avait quand même un intérêt pratique, hein, puisque euh le fait de demander à l'ordinateur de vérifier une preuve formelle de manière bureaucratique, sans âme, sans sans se laisser discuter sur des questions de rédaction, ces choses-là, bah ça fait que là, on est vraiment sûr que la preuve est correcte et la certitude. Il y a des cas où c'est pratiquement important, essentiellement pour prouver la correction de logiciel euh soit du logiciel qui tourne, soit les protocole, les versions plus abstraites du logiciel. Euh donc c'est quelque chose qui est euh qui qui est important euh à partir du moment où euh là le la le bas du transparent et je vais je voulais l'afficher plus tard à partir du le une remarque c'est qu'un système de preuve il va implémenter ben un certain ensemble de règles logique. Et avant ça même un langage. Donc c'est ce qu'on appelle un formalisme, le langage et les règles. Et dans le langage, ben il y a il y a un petit peu trois niveaux. Il y a le langage des objets mathématiques, de quoi on parle. En théorie des ensembles, tout est ensemble. En théorie des types, bah il y a des lambes à termes typé. Euh ensuite, on a le langage des propositions mathématiques, hein. Quelque chose qu'on a déjà l'habitude de formaliser. C'est déjà préformalisé, hein, dans ce que vous faites. Vous écrivez des choses. Là, on est dans un langage formel et cetera. Et puis ensuite, on a le langage des des règles et des preuves euh mathématiques. Donc tout ça, c'est des choses qui sont définies dans le langage, dans le formalisme. Et quelque part, un système de prof, ça implémentalisme donné, un petit peu comme un environnement de programmation implément un langage. Javaam, Python, c'est des langages qui sont décrits sur le papier puis après il y a des implémentations pratiques et l'analogie, elle va plus loin parce que à partir du moment où on fabrique réellement les preuves formelles, on va demander des nouvelles qualités au formalisme, hein. le la théorie des ensembles, c'est quelque chose qui est qui est pas mal parce que ça permet de tout faire et on peut tout formaliser en théorie des ensembles. C'est pour ça que c'est un petit peu le langage universel des mathématiques informelles. Euh mais quand on construit vraiment la preuve, ben on voudrait que les preuves formelles elles-mêmes soient relativement concises, qu'elles soient relativement lisible, euh relativement intuitive. Enfin, qu'on qu'on arrive à traduire assez vite nos idées dans ce langage formel. On veut aussi que ça puisse servir de base pour des algorithmes qui vont nous aider à automatiser des preuves, hein. Donc là, on passe dans l'informatique imprécise. Éventuellement, les IA peuvent nous aider à faire des preuves, mais euh on les fait vérifier par le bureaucrate. Donc la recherche dans les formalismes logiques, c'est quelque chose qui ressemble pas mal à la recherche dans les langages de programmation. Ça se ça se recoupe, ça se recoupe pas mal. Alors, ça va être intéressant pour la suite. Alors, je vais faire une petite digression sur les justement dans ces questions de formalisme, les liens entre calcul informatique et fondement des mathématiques. Euh et ce qui est marrant, c'est qu'on peut remonter avant l'ordinateur, hein. Donc on a alors Turing, on le connaît, on sait que c'est quelque part le père de l'informatique, même si il a commencé à travailler avant que les les premiers ordinateurs existent. beaucoup de choses à raconter sur Turing. Mais en en 1936, il euh il définit ce dont on a entendu parler les machines de Turing, hein, qui est une ce qui sont une manière de définir ce que c'est qu'un algorithme. En 36, donc c'est à Cambridge chez lui et mais il a pas encore fini sa thèse. En 1937, il part faire sa thèse aux États-Unis à Princeton et son directeur de thèse, c'est Alonso Church. qui est un logicien et Alonzo Church, il vient de définir pour formaliser les mathématiques, pour aller vers un form une formalisation des mathématiques, un nouveau formalisme, le lambda calcul. Alors du coup, je reparle du lambda calcul. Alors je sais que quand on parle de lambda calcul à des gens qui sont pas habitués, c'est très facile de les perdre. Moi, je me souviens il y a longtemps, j'étais en étudiant ici. Un jour, il y a Jean-Louis Krivin qui nous a fait un exposé sur l'emble à calcul. Moi, j'étais enchanté mais j'avais des camarades qui étaient qui sont sortis en disant lambda lambda lambda. Euh ça va pas être très long en tout cas. Euh néanmoins, au départ, on peut dire ben le lambda à calcul, c'est quelque chose qui est très très C'est juste pour formaliser euh ce genre de choses, hein. On a un langage, on va prendre juste les trucs dont on a besoin des termes, les variables. Dès qu'on a une variable, on peut le voir comme un terme. Si j'ai deux termes, bah je peux faire l'application de fonction. Alors, en lambde à calcul, on met souvent les parenthèses comme ça. Euh donc, si t et u sont des termes, alors t appliqué à u est un terme. Et puis donc on peut construire la fonction qui a x associé, hein. Donc ce qu'on note comme ça en de manière informelle et qu'on écrit donc lambda x point t. Alors, j'ai regardé, on n'est pas sûr de l'origine du lambda, visiblement. Il y a des différentes hypothèses. Euh j'ai j'ai regardé depuis tout à l'heure hein. Euh euh donc c'est la fonction qui a x associé mais on peut voir ça aussi comme l'expression t où il y a qui est paramétrée par x. Et donc on a cette opération qui paraît extrêmement intuitive et anodine qui est la donc la betta réduction. Si j'applique u à la fonction qui est x associé, ben on peut réécrire ça en t où je remplace x par u. Le remplacement là, je l'écris différemment de Mikael parce qu'on sait pas concerté mais j'espère que ça sera pas trop grave. Et donc l'idée et ça c'est important même pour les le reste de l'exposé, c'est qu'en gros quand on a deux termes qui sont identifiés par betta réduction, donc là c'est la clôture réflexive symétrique transitive. Enfin, quand je peux passer de l'un à l'autre en faisant des betas réduction, des betta expansion, bah c'est la même chose. C'est c'est plus que égal, hein. Ça ça va être important. Ils sont vraiment identiques. Il y a pas de différence. Euh voilà. Et donc le truc qui est marrant, c'est que arrive là-dessus, donc je suis pas sûr de l'enchaînement exact entre Church, Turing. N'empêche que Turing arrive, il vient quelque part de d'inventer ou de coinventer ou de définir ce que c'est que le calcul, qu'est-ce qu'on peut calculer. Donc on a la betta réduction et donc là à un moment assez vite, ils se rendent compte d'un truc. Si je prends ce lambda à terme là, donc là c'est la partie un petit peu olé olé. On va prendre quelques minutes mais c'est rigolo. Donc la fonction qui a x associe x appliqué à x. Alors qui le connaît ça? Juste pour voir, vous êtes peu nombreux à l'avoir vu. Euh bon ok, je vais l'appeler delta. Et là maintenant je fais euh delta appliqué à delta. Donc c'est ce trucl lambda x x appliqué à x. Là j'ai changé le nom de la variable liée mais c'est la même chose. He lambda y y appliqué à y. Je peux faire une betta réduction. Il y en a qu'une seule, hein. C'est ici. Ça c'est la fonction et là c'est l'argument. Donc c'est quoi? C'est le corps de la fonction x appliqué à x où je remplace x par delta. C'est quoi ça? C'est ça. Donc c'est delta delta. C'est la même chose ça. Ce betta réduit vers lui-même. Donc on tourne en rond. Dire qu'on tourne en rond à chaque étape, on retombe sur nos pattes. Bon. Euh le truc qu'on peut faire, c'est si maintenant on change un tout petit peu le truc, on dit bah j'ai une fonction, une certaine fonction, une fonctionnelle grand f et puis au lieu de dire lambda x x appliqué à x et x appliqué à x le tout appliqué à f. Qu'est-ce qui se passe quand je fais delta del delta prime appliqué à delta prime? Il va se passer en gros la même chose, sauf que j'ai un grand f qui a été rajouté devant. Alors, qu'est-ce qu'on peut faire avec ce truc? Bah, on peut faire beaucoup. Donc là, on a pas le temps de rentrer là-dedans, mais en gros, on va on va être capable de tout faire parce qu'on peut faire on peut écrire un programme récursif. Il suffit que grand f soit une fonctionnelle qui définit une fonction à partir d'elle-même. Euh, on peut définir en gros le lettre de de ML avec ça. Et à partir du moment où on a ce trucl, excusez-moi, on va un tout petit peu. Est-ce que c'est possible d'avoir enregistré tout le tout l'écran pas vu que si la ligne verte c'est ce qui est enregistré dans la vidéo, ça serait possible de régler juste ça. Bah ça dépend après de combien d'informations c'est pris en bas mais là sur les deux dernières. Je suis pas sûr, je sais pas exactement euh c'est la question. Non, c'est une question. Qu'est-ce qu'on voit sur les slides? Ça c'est tout enfin de mon de mon côté c'est tout bon. Je contrôle on va espérer sinon voilà. Alors en gros, il y a on a ce truc là. Après ils se sont rendus compte assez vite que juste avec les lambdes à terme on peut coder des entiers. Donc en gros l'entier n c'est la fonction qui prend x et f en argument et qui itère f n fois. Donc ici 0 fois une fois de fois trois fois et cetera. Ça s'appelle les entiers de church. Et en gros euh avec le point fixe et ça bah on arrive à euh écrire tous les algorithmes, écrire toutes les fonctions récursivement définissable ou toutes les fonctions calculables. En gros, on peut coder toute machine de Turing par un lambda à terme et euh avec les euh donc toute fonction calculable, tout algorithme est codable dans ce lambda à calcul pur. Alors bon, on peut dire c'est pas mal mais en fait ça va poser des problèmes de cohérence logique. Donc là je c'est la dernière partie de cette ce volume logique. Et il y a une remarque qui que je trouve quand même frappante, c'est souvent les formalistes, les grandes familles de formalisme logiques, les premières versions, bah elles étaient mauvaises, hein. Ça montre bien que quand il y a une erreur, ça veut pas dire que l'idée est mauvaise. Au contraire, au contraire. Donc la théorie des ensembles, on connaît le l'histoire de Cantor du paradoxe de de Russell. Euh comme Michael l'a dit, la première version de la théorie des types de Martin Love qu'on va utiliser ensuite était euh était euh aussi paradoxal. Et pour Church, le premier formalisme de Church était paradoxal parce qu'il utilisait des et c'est lié au fait qu'on utilisait des lambes d'erme non typé. En gros, ce qui s'est dit c'est que ces lampes d'erme, c'est quand même génial. Je peux tout faire avec ça. Je peux définir les je peux l'utiliser pour les objets mais pour représenter les propositions et aussi les ensembles. Après tous les les ensembles, les propositions, c'est un peu la même chose hein. Donc en gros l'idée c'est quoi? TU. Donc vous pensez que c'est lambda terme mais t appartient à U. C'est la même chose que T euh je me suis trompé. C'est T vérifie la propriété U hein. Donc c'est U appliqué à T. J'aurais dû le mettre dans l'autre sens. Euh et du coup Benjamin Oui. Et euh dans les Principiades de Russell et White, est-ce qu'on sait si c'était si on veut le prendre au pied de la lettre? Est-ce que est-ce qu'on sait si c'est consistant ou pas? Euh je pense pas qu'il y a de paradoxe dans les principi euh qui s'appelle aussi théorie des types mais qui sont une version euh théorie des types plus euh plus ancienne. En tout cas, ça m'étonnerait queil y ait le paradoxe de Russell parce que c'est Russell mais encore que on sait jamais un gros paradoxe. Non, pas que je pas que je sache, pas que je sache. Et en gros, par contre dans ce truc là, on peut faire le paradoxe de REL parce que l'ensemble des X qui n'appartiennent pas à eux-mêmes, c'est quoi? C'est la propriété ne pas s'appenir à soi-même. Donc c'est lambda x ne s'appartient pas à lui-même. Ça ressemble à quelque chose hein. Du coup cet ensemble R appel R pour seul R appartient à R c'est quoi? Bah c'est R appliqué à R. Et là c'est le même lme que tout à l'heure. Ça se réduit vers quoi? Ça se rédu vers non R appartient à R. Donc ça veut dire que cette proposition R appartient à R, elle est beta équivalente. Elle est vraiment identique avec non R appartient à R. Et à partir du moment où il a une proposition qui est identique à sa sa négation, bah là on a un paradoxe. Donc c'était paradoxal. Euh donc il a fallu revenir changer quelque chose et la réaction de Church, bah ça a été de passer au l calcul typé. Donc là, je peux aller plus vite parce qu'on en a parlé mais en gros quand on abstrait une variable, il faut donner un type. Donc c'est une espèce de de notion d'ensemble assez structuré hein. Donc c'est type A flèche B. B c'est le type de du résultat. Donc ça ça va assurer un certain nombre de choses. La terminaison du calcul. Donc on n'est plus Turing complet. Quand on a un lambda calcul typé, on n'est plus Turing complet, sauf si on rajoute le lettre rec comme dans un langage de programmation. Euh et le formalisme de Church avec toute petite modification qui qui s'appelle la théorie des types simples mais aussi higher order logic HOL. C'est toujours utilisé dans des systèmes de preuve effectivement utilisés hein, les tous les systèmes qui s'appellent d'ailleurs HOL, HOL Lite, les choses comme ça. Euh donc euh Benjamin, du coup en fait le problème original dans le premier calcul c'était que on pouvait appliquer tout à n'importe quoi. Enfin, c'est le fait ça empêche d'appliquer X à à XO. Oui oui oui. Euh le j'ai j'ai pas moi-même bien regardé dans les archives exactement qu'est-ce qu'on sait du paradoxe. Est-ce qu'on a des brouillons? Est-ce qu'il y a eu un une première version publication de church qui a été qui était paradoxale? Ça je sais pas mais mais c'est lié à c'est lié à ça. Alors les types il ils ils reviennent sur le le devant de la scène. Alors là aussi un truc assez frappant. C'est Père Martin Love. Euh là, il est plus âgé qu'au moment où il a inventé cette théorie des types modernes. Euh c'est pas un informaticien, hein. Et il va faire quelque chose, il va inventer un formaliste qui est très très informatique euh mais pour des motivations assez différentes, hein. Donc l'idée de la théorie des types modernes, on a parlé un petit peu ce matin déjà, c'est que les propositions sont des types et les preuves, bah c'est des objets de ce type. Donc T de type A, ça veut dire T est une preuve de A. Mais il y a aussi des types qui correspondent pas tellement à des propositions qui sont plus des types de données comme les entiers naturels. Donc les preuves sont des objets comme les autres. Donc c'est un des trucs assez rigolos, hein. Et donc il y a cette vision fonctionnelle des preuves. C'estd qu'une une preuve de A implique B. En fait c'est une fonction de A vers B. Ça prend une preuve de A, ça la transforme en preuve de B. On n pas trop besoin de ça pour la suite mais c'est quand même marrant à voir. Une preuve de A et B. Ben en fait A et B c'est le produit cartésien parce que les éléments du produit cartésien bah c'est fabriqué par une preuve de une paire avec une preuve de A et une preuve de B. Si vous me prenez une preuve de A et une preuve de B ensemble une preuve de A et B. Et pour le pour tout c'est aussi une fonction on va l'utiliser un petit peu. Une preuve de pour tout x de type A B c'est une fonction qui prend une preuve de A en un objet de type A en argument et qui rend une preuve que cet objet vérifie B. Donc ça ressemble, ça généralise en fait la flèche, sauf que le l'objet X ici peut apparaître dans le le coproduit. Et le dernier truc, c'est ça, on l'avait dit déjà, le A ou B, bah il y a deux preuves canoniques de de forme pour les preuves canoniques de A ou B. Soit une preuve de A avec un petit drapeau qui s'appelle I ici qui dit je suis une preuve de de la gauche de de A ou une preuve de A ou B. Et euh une remarque, c'est que un formaliste comme ça, il est naturellement constructif, hein. Donc ça se voit bien ici parce que quand j'ai une preuve de A ou B, ben si je la en fait si je la betta réduit, si je fais les calculs, ça va terminer puis à la fin, j'aurai soit ça, soit ça et donc je saurais si je suis dans le KA A ou le KB et donc je serai en donc c'està dire qu'on est dans une logique qui est qui est intuitionniste où le tiers exclu n'est pas prouvable. Alors, on peut le rajouter comme axiome, mais dans ce cas, on perd la propriété de constructivité. Et aussi une preuve de euh pour tout x il existe y tel que ça, ben on peut voir ça comme un programme qui prend X en argument, qui rend Y avec en plus une preuve que X et Y sont en en relation. Mais ça, on en a pas trop besoin. Ce qui nous intéresse et ce qui est assez remarquable, c'est que le langage des objet dans ce formalisme, bah c'est des lambes à terme typé. Et des lambes d'M typé, c'est des programmes fonctionnels typés. Et en plus, on a un système pour créer des nouveaux types. Alors, chez Martinlov, au début, c'était pas aussi généralisé, hein. Donc là, c'est pareil, on en a parlé. Euh, on peut définir les entiers naturels de manière très simple. Alors, c'est pas la manière la plus efficace d'un point de vue calculatoire en disant bah c'est le plus petit type qui est qui contient zéro et le constructeur successeur. Donc, j'ai zéro puis j'ai successeur de zéro puis successeur de successeur de zéro. Et comme c'est le plus petit, bah il y en a pas d'autres que qu'on a vraiment les entiers naturels. Et on peut là-dessus calculer, hein, en faisant une analyse de cas. Donc là, c'est voilà, on l'a déjà vu aussi l'addition euh on regarde si le premier argument donc il faut faire un choix est-ce qu'on regarde le premier ou le deuxè? Si le premier là on fait le choix du premier, si le premier c'est zéro, le résultat c'est le deuxè et sinon on met un successeur et on a un appel récursif. Donc il y a une condition de terminaison qui fait qu'on sur les fonctions récursifes qui fait qu'on va toujours avoir des fonctions qui qui terminent. Et donc au fond les programmes de cette théorie des objets dans cette théorie des types hein, donc dans Rock mais aussi dans Line quelque part c'est une espèce de fragment de ML purement fonctionnel avec une condition syntaxique pour garantir la la terminaison. Oui. Juste pourquoi tu avais appelé ça fix point? C'est la déf parce que c'est une fonction récursive. C'est pour dire c'est c'est pas moi, c'est le euh fix point parce que j'ai pour avoir le droit ici d'appeler récursivement la fonction. D'accord. Et fix point parce que une définition récursive, c'est un truc de logiciel. On peut voir ça comme le point fixe d'une d'une définition. Euh c'est relié à cette histoire du delta delta là qui permet de crocoder les fonctions de euh les fonctions récursives. Et donc le truc qui va nous intéresser, c'est la règle de conversion. Donc ça c'est pareil Michael l'a dit dans théorie des types euh on s'en fiche un petit peu mais en gros c'est défini, il y a tout un tas de règles qui définissent euh dans quelles conditions un tel jugement est valide. Donc dans gamma, on a les axiomes. En fait, les axiomes, c'est des variables, hein. Si je suppose fais une hypothèse, ben je une hypothèse H, ben j'ai une variable qui est de type H, hein. Donc là-dedans, il y a des variables qui sont des axiomes ou des des variables de d'objets. Et donc euh ça c'est T de type grand P. Et quand quand on peut voir P comme une proposition, c'est T est une preuve de P. Et le truc qui est important, c'est ça. Alors, qu'est-ce que ça dit? Ça dit bon ici il faut que je garantisse que P B est une proposition qui veut dire quelque chose et en gros si j'ai une preuve de A même T c'est aussi une preuve de B à partir du moment où A et B sont convertibles par calcul. Donc c'est ce que j'ai dit au début. Les propositions A et B, elles sont identifiées. C'est les mêmes. C'est les mêmes les mêmes objets qui sont les preuves de l'un et de l'autre. Et c'est ça qui va être qui va être crucial. Euh parce que cette betta réduction, ça capture le calcul. Et rien qu'avec l'exemple du transparent précédent, ben 2 + 2, c'est quelque chose que j'ai le droit de former mais en plus j'ai le droit de calculer avec. et 2 + 2, bah ça se calcule vers 4. Donc 2 + 2, c'est pas est égal à 4, il est convertible à 4. Et à partir du moment où 2 + 2 est convertible à 4, euh donc c'est ce que j'ai déjà dit, à partir du moment où 2 + 2 est convertible à 4, la proposition 2 + 2 = 4. Donc là, c'est le proposition he c'est le égal propositionnel. Ce trucl par congruence c'est convertible à 4 = 4. C'est la même que la proposition 4 = 4. Alors le fait qu'on ait plusieurs niveaux d'égalité, c'est à la fois une force mais aussi des fois c'est un petit peu ça complique les la vie dans les théories des types hein. Il y a des avantages et des défauts mais là on va pas aller trop loin hein. Donc là juste on va utiliser cette remarque là hein. Alors là on écrit un tout petit peu de preuve. la on a la propriété de réflexivité sur l'égalité. Je dis pas comment elle est définie mais peu importe mais ça veut dire que pour tout type A euh X de type A bah j'ai X = X. Alors vous rappelez les le pour tout c'est un truc qui prend un argument. Ça veut dire que si je lui applique NAT pour le type A 4 pour le X, ben j'ai une preuve de 4 = 4. C'est rassurant. Mais comme on l'a dit, 4 = 4, c'est la même chose que 2 + 2 = 4. Donc là, j'ai prouvé 2 + 2 = 4 aussi, hein. Euh puis j'ai pas prouvé que ça, j'ai prouvé aussi euh 200 + 200 = 400, hein, de la même manière. Donc euh c'est pas super impressionnant, mais on voit qu'on peut avoir des trucs assez compliqués qui utilisent pas mal de calcul. Et ça c'est ce qu'on va faire. Alors là, c'est un calcul un peu gros. Les petits calculs qu'on fait dans des preuves. Je vite, je vais néanmoins faire une démo. Euh les petits calculs qu'on fait dans l'épreuve. Je voulais quand même faire un petit exemple tout simple. Voilà. Alors, j'espère que vous avez pas trop peur quand vous voyez une fenêtre coque rock. Donc là, c'est les entiers. Voyez, j'ai défini le prédécesseur là. D'accord? C'est quand c'est zéro, ben faut que je choisisse quelque chose. Prédesseur de zéro, je prends zéro. Mais sinon, j'enlève le successeur. Donc si je fais, je peux vérifier le calcul là, je prouve rien. Je dis juste compute près de 5. Donc 5 en fait, c'est successeur successeur 5 x 0 in. Il me dit bien 4. Ça marche. Ah non, faut pas que je fasse trop. Bon zut, peu importe. Euh un truc qui est marrant là, ce que je vais pouvoir montrer en utilisant ça, c'est ce lem là qui dit pour tout x et y. Si successeur de x é= successeur de Y, donc en gros le successeur est injectif, alors x = Y. Donc tout ce que j'ai sur les entiers, c'est le schéma de récurrence et le calcul. Mais là, j'ai du calcul avec le prédécesseur. Donc qu'est-ce que je vais faire? Donc je vais bouger les trucs là. Les détails, on s'en fiche un petit peu. Je mets ça au-dessus du contexte. Donc vous voyez que là ce que je dois montrer, c'est x = Y. dans le contexte où X et Y sont des entiers et je sais que successeur de Xeur de Y. Je suis embêté parce que j'ai une égalité sur successeur de X mais dans la proposition j'ai X. Ce qu'on va faire? Ben on va faire le un calcul à l'envers. Je vais dire remplace X par c'est quoi X? C'est le prédécesseur du successeur de X. Alors, il va me demander de prouver l'égalité ensuite, hein. Mais cette égalité là, ça sera juste du calcul, hein. Et là, comment je fais maintenant? Là, je dois faire un petit raisonnement. Ben, je dis puisque successeur de x égal à successeur de Y, on peut faire ce rewrite. Donc, ça va remplacer successeur de X par successeur de Y. Prédécesseur du successeur de Y, ça se calcule vers Y. Donc là, si je fais le simple, pardon, si je fais le simple, ben j'ai y = y, c'est réflexif. Et l'autre, c'est aussi de la réflexivité, hein, simple. Et là, j'ai fini. Donc le fait de de pouvoir calculer, ça me permet de prouver des choses et très souvent les calculs, alors c'est encore plus vrai comme on l'a vu dans l'épreuve où il y a du de la récurrence, on fait un peu de raisonnement, un peu de calcul et puis on reprend. Alors ce dont je veux parler c'est quoi? Des preuves calculatoires. Des preuves où il y a beaucoup de calcul. Euh c'est moche là. Je vais refaire le Mais quand tu dis faire du calcul, c'est appliquer une fonction. C'est ça? Euh on va voir. Euh bah ça dépend hein, ça marche pas toujours. Mais là on va on va essayer d'appliquer des fonctions. Donc là un exemple de je ça va apparaître je pense j'espère. Sinon faut reposer la question. Euh le fait que 7 et premier, c'est un peu un archétype de proposition mathématique. Donc les premers après si on regarde des grands nombres premiers en 51, alors 1951 c'était le dernier qui était montré à la main, c'était celui-là. Donc il y avait 44 chiffres, on a montré qu'il était premier. Euh la dernière fois que j'avais fait le transparent, c'était le record c'était en 2018, on avait un nombre avec 24 millions de chiffres. Puis l'année dernière, il y en a un qui a été trouvé avec 40 ou il y a 2 ans avec 40 millions de chiffres. Donc euh il y a un progrès d'un nombre impressionnant d'ordre de grandeur entre ces dates. Euh même si les gens des années 50 étaient sûrement beaucoup moins intelligents que nous. Euh non, évidemment non. Euh la cause du progrès, c'est clairement l'ordinateur, hein. C'est parce qu'on est capable de faire des calculs euh des calculs rapides. Néanmoins, si on avait donné des ordinateurs aux mathématiciens des années 50, ils auraient sûrement pu euh trouver vite des nombres premiers plus grands que ça, mais ils seraiit pas arrivés à ce niveau-là tout de suite, hein, parce que parce qu'on avait l'outil, du coup, on a développé des mathématiques qui permettent de mieux l'exploiter, les courbes elliptiques, des choses comme ça. et euh et du coup ben on on arrive à trouver des grands nombres comme ça. Donc la question après, c'est un petit peu quel est le statut des preuves que de propositions comme celle-là qui repose sur du calcul informatique, hein. Comment est-ce qu'on peut le croire quand on est logicien et un peu borné? Bon, OK, là on avait vu les trucs. Alors, un nombre premier. Alors, pourquoi un nombre est premier? Si je veux montrer que 5 est premier, bah on peut raisonner. On peut dire bah c'est pas divisible par 2, pas par 3, pas par 4, pas par 0. Euh, remarquez d'ailleurs même ça déjà il faut faire en général, on fait un calcul là pour dire que 3 divise pas à 5. Euh, c'est pas tellement un raisonnement. Euh ensuite, les nombres plus grands, enfin ça c'est comment on le fait euh à l'école. Comment est-ce qu'on peut formaliser ça en rock? Ça serait assez pénible. Ça serait assez pénible. La manière simple de prouver qu'un nombre est premier en rock, c'est ça. C'est dire bah oui, mais en rock, je peux écrire des programmes. Donc je vais écrire un programme, c'est un programme fonctionnel, quelque chose qui est type N flashbou puis qui va tester si le nombre premier. Je peux faire très naïvement. Je peux essayer de diviser par tous les nombres là entre 2 et n - 1. Puis je rends vrai si je trouve pas de diviseur. Hm. C'est trop long à faire. B. On va voir. Euh après, je peux prouver là, ça devrait pas être trop dur parce que c'est presque une définition d'être premier mais que si ce programme rend vrai à ce moment-là, le nombre est premier. Alors du coup, c'est quoi la preuve que 5 est premier une fois que j'ai fait ça? Bah test correction, ça me dit permet de prouver que n est premier. Si je prends n = 5, que 5 est premier à condition que test de 5 soit égal à vrai. Et moi ce que je dis, ben ça c'est une preuve. RFL de trou vous rappelez c'est le truc qui dit pour tout x est ég à x. Bah oui, parce que rèfle de trou c'est une preuve que trou égale trou mais par calcul test de 5 ça va calculer vers trou. Donc c'est bon. Donc la preuve est très petite. La preuve est très petite mais on voit que le système de vérification de preuve pour dire c'est correct il doit quand même faire le calcul à un moment. On a rien pour rien. Mais dans la vérification des preuves en théorie des types, il y a un moteur de calcul. Alors euh donc on doit calculer ça. Alors je suis en retard. Donc je vais mais j'ai quand même juste montrer que ça marche euh parce que je l'ai fait j'ai fait ça enfin je l'ai refait pour vous. Euh donc là, je l'ai fait vraiment en amateur, hein. Je je suis parti de rien. J'ai défini être premier comme ça. Donc j'ai que l'addition et la division et la soustraction au début et la multiplication qui sont prédéfinis. J'ai même pas la division. Euh il y a 200 lignes à peu près. J'ai écrit donc là je montre des trucs. Là vous voyez, j'ai j'ai écrit la division pareil super naïve hein qui essaie de de faire la soustraction par tous les nombres. Donc il itère la soustraction. Euh il y a deux trois trucs là. Il y a le truc le programme de test qui teste qui fait un test f sur tous les nombres entre 2 et n- 1. Après le programme il est où le test? Voilà le test. Ça c'est le truc le test qui m'intéresse. C'est cet itérateur là sur le test qui regarde si n est divisible par d enf si n n'est pas divisible par d. Là, j'ai fait des essais. Donc là, pardon, là, j'essaie de diviser 11 par tous les nombres entre 2 et 10. Et puis il me dit, ouais, c'est vrai. Euh 1783 1784, c'est false. Bah oui, c'est pas c'est pas premier 1784. Donc ça a l'air de marcher. Vous voyez que ça va alors bien que le l'algorithme est super naïf, que la représentation des nombres est pourri. Les nombres, ils prennent une taille proportionnelle à n hein. C'est très très mauvais tout. Bah finalement ça va assez vite parce qu'on a un ordinateur moderne et il y a ce VM compute dont je parlerai plus tard mais voilà. Et donc en gros après je fais le reste de la preuve qui me dit voilà c'est ça qu'on voulait là. Donc si euh test de S de N donc j'essaie si quand j'essaie de diviser successeur de n par n tous les nombres entre 2 enfin 3 et non 2 et n si ça me rend vrai alors je sais que successeur de n est premier et donc là je vais montrer que 1783 est premier donc j'utilise ce lem ça veut dire qu'en gros ce truclà ça va être utilisé pour prouver ça donc il il va comprendre que n c'est 1782 et donc il va me rester à montrer ça. Voilà. Et là je dis bah essaie de faire les calculs qu'il y a là-dedans. Donc c'est comme simple, c'est un simple un peu plus rapide ce même compute. Effectivement ça serait écrit vers tr égal tr et donc par réflexivité c'est bon. Et j'ai montré que 1783 était premier et de 1999 ça marcherait aussi. Donc on arrive à faire des preuves qui utilisent euh du calcul. Mais comme je le disais, on veut aller plus loin, on veut faire plus hein, on veut peut-être pas réussir les nombres à 40 millions de chiffres, mais enfin essayer de faire un peu mieux, hein. On veut prouver des trucs dans ce genre-là. Donc là, évidemment, on va pas le faire avec des nombres lunaires et avec un algorithme de division aussi naïf, mais il n'empêche qu'on a les armes pour importer dans notre système de preuve la technologie qui a été développée, soit d'un point de vue algorithmique, de représentation des nombres et aussi mathématiques euh pour prouver des des nombres la primalité de nombre plus grands. Donc là, c'est pas des courbes elliptiques, c'est un truc qui remonte à c'est ce qu'on avait utilisé avec des collègues, ça date, ça remonte aux années 2000, le théorème de Pok Clinton, mais c'est un théorème qui permet de donc j'ai certains transparents qui sont en anglais qui qui donnent une condition suffisante pour la primalité, hein. Donc on on sait que un nombre n est premier quand on a ça, c'est quoi? C'est une décomposition partielle en facteur premier de n - 1. Hein, il faut qu'on arrive jusqu'à √ n avec ce truc. Et puis on a ces conditions-là euh là et là sur ces trucs-là. Euh donc ça ça a été prouvé et euh on dit en général que euh ici donc les différents nombres qui interviennent, les a, les facteurs pi alpha I, c'est ce qu'on appelle un certificat de Pokon pour N. Pourquoi ça? essentiellement parce que vérifier ces conditions-là, c'est pas complètement trivial, mais c'est beaucoup plus facile que euh que de les trouver. Il m' il a un mot d'excuse, ne vous inquiétez pas. Euh que de que de que de les construire, que de les trouver. Donc euh bah du coup on a un plan hein, on veut utiliser le théorème de Clinton donc il faut le prouver en rock. Donc ça ça avait déjà été fait en 2001 à l'époque ça s'appelait COP mais par Martin Risd et Olga Caprotti. Et ensuite, il faut définir ce que c'est que ces certificats. Le test qu'on avait tout à l'heure, bah cette fois, il va être plus malin et plus complexe. Il va prendre en argument le certificat N et le certificat, mais il va quand même dire "Oui, oui, c'est un certificat correct." Il va vérifier les conditions du transférent précédent. Faut montrer qu'il est correct, montrer queil vérifie bien les conditions du théâ de Pokon et après c'est bon hein. On est quasiment dans la même situation qu'avant. Euh bah si, il nous faut quand même des des construire les certificats, mais les certificats pour le coup, on va les vérifier en rock. Donc on peut les construire tous les coûts sans permis. On peut le faire en C en utilisant une bibliothèque numérique, les trouver sur le web et cetera. Et une fois qu'on a fait ça, ben normalement on appuie sur le bouton et tout marche. Euh alors, il y a des trucs un peu rigolos, mais là je vais passer assez vite là-dessus sur comment on définit les certificats. Mais en gros, on va vraiment construire le programme fonctionnel. Il y a des anuplay comme ça. Après, il y a un truc assez amusant qui sont que les pays là, les facteurs premiers, bah il faut eux-mêmes montrer qu'ils sont premiers pour que ça marche. Bah du coup, on va rajouter des certificats pour ces nombres. Puis après, on s'est rendu compte que si ça branchait, on avait des certificats qui qui arrivaient en double, en triple et cetera. Donc en fait, on a tout aplati. Donc en gros, on a une espèce de de liste comme ça de nupla. Euh et là 127 par exemple, il apparaît et voilà les nombres qui apparaissent ici, faut qu'ils aient tous un certificat ensuite. Donc ça c'est un petit certificat, c'est une espèce de de mini base de données de certificat et ça marche. Euh donc ça c'est les définitions rock. Euh il y a un truc, si vous regardez les conditions, vous voyez qu'il y a des gros nombres, il y a des puissance n-1 ou les choses comme ça, mais c'est toujours module ON. Donc en fait, il faut rajouter des des trucs qui calculent module on pour que ça marche assez vite. Et euh les certificats, ben là c'est utilisé, c'est Benjamin Grégoire qui avait fait ça, qui que des programmes C, des bibliothèques numériques. Euh donc ils sont fabriqués, ça fabrique des fichiers qui sont qui sont importés dans Rock. Et du coup ce truclà, bah ça a été vraiment prouvé. On est sûr de ça. Ça a été prouvé. Ça a été prouvé en rock qui s'appelait coque avant quand j'avais mis ce petit gag là. Alors, depuis comme je disais hein, c'est c'est ça date des années 2000, donc quelque part c'est obsolè mais le principe reste valide hein. On a une possibilité de calculer dans le système, de prouver des choses sur les programmes puis d'utiliser la combinaison du calcul et de cette preuve de correction et d'importer des choses comme les mathématiques. Donc pour que ça marche bien, il faut avoir une représentation efficace des entiers dans rock. Donc le les bonnes représentations de nombres al les flottants ou les mais là c'est des entiers mais les flottants c'est c'est la spécialité de de Mikael justement hein. On a intégré donc là je vais pas avoir le temps de mentionner ça je pour peut-être en parler mentionner ça plus demain. La compilation d'un rock c'estàd que pour exécuter les programmes plus rapidement on a les les les termes rock ils sont gardés sous forme source là comme on les écrit mais ils sont aussi compilés vers une machine qui les exécute efficacement et puis par ailleurs, on peut importer des résultats mathématiques plus modernes hein comme la sur la primalité comme les courbes elliptiques. Donc Laurent Théri, Guillaume en ils ont fait des choses et donc on arrive à à aller plus loin. Alors, il me reste un petit peu de temps pour parler d'autres choses que les nombres. Donc quelque part, on est content de ça, mais finalement, on peut dire oui, les nombres premiers, l'énoncé, il est il y a tellement il est tellement calculatoire que c'est pas super étonnant. Et après, si on veut embêter les mathématiciens, on peut dire bah oui, mais il y a des fois, il y a des résultats qui ont pas l'air calculatoire et ben si vous avez pas d'ordinateur, vous allez être embêté. Et il y a deux exemples pour ça, le théorème des cas couleurs et la conjecture de de Kepler. Et dans ces deux cas-là, c'est intéressant parce qu'il y a des mathématiques et des programmes qui sont un peu adoc, qui peuvent être assez complexes dans les deux cas. Et il y a un problème à la l'interface des deux pour vérifier, pour s'assurer bah oui, est-ce que est-ce qu'on est vraiment sûr du truc? Et il y a vraiment une question de vérif de standard de vérification. Alors ce qui est assez amusant, c'est que les quatre couleurs, ça avait pas été trop contesté à l'époque. Par contre, la formalisation la preuve de la conjecture de Kepler, Thomas Hales a eu des problèmes. Alors, la conjecture de Kepler, c'est quoi? Donc, ça a été énoncé en 1611. Alors Kepler l'avait pas vraiment énoncé comme une conjecture mais en gros ça dit si vous avez des sphères de de même diamètre là comme les oranges, vous les rangez de la manière la plus compacte possible, bah les manières intuitives c'est les bonnes. Donc la manière les manières intuitives, ça donne cette ça c'est facile à calculer enfin pas trop dur que c'est cette densité de pi sur √2 et qu'on peut pas faire mieux en tout cas qu'on a une infinité d'orange. Euh donc ça ça a résisté très longtemps aux efforts des mathématiciens. Et donc en 1998 quand Thomas Hayes, professeur à à l'université de Pittsburg a annoncé sa preuve, il a présenté 200 pages de mathématiques. Donc triviale hein, c'est de la géométrie. Là, je serais absolument incapable de le de l'expliquer. Euh, évidemment, ça a été un gros truc. qu'on s'est mis à vérifier tout de suite et euh il a eu du mal à faire reconnaître sa preuve par la communauté mathématique. Les relecteurs après un an, ils ont dit on est à 99 % sûr que c'est bon mais il y a ces programmes informatiques et là on sait pas trop ce qu'ils font et plusieurs années après, c'est ils en étaient au même point. Alors, il a fini par faire réussir à publier son truc, mais ça l'avait quand même échaudé. Comme il avait entendu parler de la formalisation des quatre couleurs, il a entamé un grand effort de formalisation de sa preuve, Flypec, Formalizing Kepler, avec toute une équipe. Il a passé 10 ans à peu près et ça a été terminé en 2014. Il y a une preuve formelle donc en HOL, Hol light euh du euh de son de son théorème alors qui est donc le théorème de Ha maintenant. Euh alors juste pour donner une idée parce que je trouve c'est amusant. Euh ça c'est un des exemples de trucs qui sont vérifiés par ordinateur. Donc vous voyez que c'est des trucs qui sont il y a plusieurs milliers de lemes comme ça. Il y en a pas autant que ça. Euh donc il y a six variables parce que ça correspond à des volumes mais à chaque fois ça beaucoup de variables ce qui complique un peu le truc mais on voit c'est des trucs qui sont ça ressemble à des matap hein, c'est pas des maths fondamentales. On va utiliser un bon algorithme d'optimisation assez rusé qui va réussir à montrer que ce trucl c'est toujours en dessous de ça. Pas de beaucoup hein, il y a des fois c'est assez serré mais ça passe. Donc qu'est-ce que ça veut dire? Ça veut dire que si on veut formaliser la preuve, bah on est obligé de prouver la correction d'algorithme d'optimisation d'algorithmes de mathématique appliqué. Donc là, il y a un truc un peu une espèce de renversement tout ce qu'on utilise des mathématiques appliquées pour montrer des choses de mathématiques qu'on perçoit comme très très fondamental. Alors l'autre exemple euh Oui. Avec on pourrait faciliter la construction euh je connais trop mal la preuve pour pour répondre là-dessus. Euh mais en principe, j'imagine que j'imagine que oui. Euh enfin au moins pour des choses ça pourrait pour pour d'autres choses du même ordre. Après pour autant qu'il y a des choses qui mémorent, mais euh ouais euh globalement le l'idée de de faire discuter ou interagir une IA imprécise avec un un système de preuve précis mais de manière plus complexe que où il y a un vrai aller-retour, je pense que c'est quelque chose qui se fait encore assez peu aujourd'hui mais qui risque d'être assez euh important dans le futur. Alors, je vais donc parler un petit peu du théorème des quatre couleurs. Donc là, on va pas parler de formalisation pour l'instant, c'est juste on va faire des maths un peu rigolotes. Donc le terme des quatre couleurs, vous le connaissez. Quand on a une carte planiaire, il y a toujours moyen de la colorier de manière à ce que deux régions qui ont une frontière commune, pas juste un point, est une une couleur différente. Euh donc ça a été remarqué puis conjecturé en 1852 par un géographe qui connaissait des mathématiciens comme de Morgan, des celui des lois de Morgan. Et puis ça a fait son chemin, ça a été publié. Euh et puis en gros euh n'importe qui. Moi, je me rappelle dans comment s'appelait jeu et stratégie. J'avais vu ça la première fois quand j'étais gamin. On a tout de suite envie d'essayer de le montrer. Euh donc plein de gens essayent. Il y a toujours des gens qui trouvent des preuves qui sont fausses. Euh ou peut-être pas, peut-être qu'il y en a une qui est vraie mais OK. Bref. Et puis en fait en 1879 ça a été prouvé et puis en 1880 il y a une autre preuve sauf que 10 ans après, on s'est rendu compte que l'une puis l'autre était fausse. Donc du coup c'est resté ouvert assez longtemps. Il y a tout un tas de un certain nombre de de constructions qui ont été développées, d'idées dont on va parler un petit peu. Euh et en particulier Wolf Ganghich a été important pour l'histoire d'inévitabilité. Et le gros truc c'est en 1976 euh Can Apple et euh je crois il s'appelle Wolf Kenharkan ont dit bah voilà on l'a prouvé et à l'époque c'était quand même choquant. Il ils utilisaient l'ordinateur 1200 heures de calcul sur un ordinateur de l'époque. Ça coûtait cher évidemment. C'est aujourd'hui, il faudrait beaucoup moins de 1200, il faut beaucoup moins de 1200. Euh la preuve a été raccourci et nettoyée, rendu plus propre en 1995. Alors ce qui est assez marrant c'est que Robertson, Sanders Seimore, ils ont pu faire une preuve plus courte parce qu'ils avaient des ordinateurs plus puissants. Donc ils ont pu réussir à à trouver un truc dont la vérification, ils ont trouvé un meilleur certificat si on veut hein, pour parler un petit peu dans le en terminologie euh Flinton. Et donc ça a été formalisé en 2004, en été terminé en 2004 par George Gontier que j'ai aidé en en coque. Alors ce que je propose de faire c'est parler un petit peu de la preuve aujourd'hui. En fait je vais montrer la preuve fausse de Campe et puis demain, on regardera les principes de la preuve vraie et là on verra le calcul qui arrive. Donc pourquoi le calcul dans cette preuve? Alors en fait, on aura la réponse demain seulement, mais euh c'est quand même amusant. Donc à la base, on a assez vite compris que c'est un problème de coloriage de graphe, hein. Donc chaque région met une capitale. Quand il y a une frontière commune entre les deux régions, on a une arête. Et donc on veut colorier les sommets avec quatre couleurs de manière à ce que deux sommets qui sont voisins ne sont pas de la même couleur. Alors la première remarque c'est de dire que ben on va s'intéresser tout de suite au cas le plus difficile. On a mis le maximum d'arête. Et un maximum d'arrête ça veut dire quoi? Ça veut dire que toutes les faces, donc les faces c'est les régions là sont triangulaires. Donc là, j'ai rajouté il suffit de rajouter des arêtes. Dès qu'il y a une face qui est pas triangulaire, on rajoute une arrête ou deux dedans. Donc là, je rajoute des arêtes partout. Alors là, il y a plus que des triangles. La face à sauf la face extérieure. Donc ça, c'est une quasi triangulation, ça va être important. Et du coup l'extérieur, je rajoute aussi des trucs jusqu'à ce que il y ait plus que trois. Encore une. Voilà. Là l'extérieur, c'est un triangle. Enfin, c'est un truc qui a trois trois arêtes. Donc, on peut considérer uniquement les graphes triangulés. Alors, pourquoi on fait ça? parce que une fois qu'on a la le graphe triangulé, ça va nous donner un point d'attaque pour le coloriage. Et ça ça va l'idée va rester vraie. La preuve de de Campo, elle est quand même donc on est dans des graphes qui sont pleines. Donc on a la formule de l'air qui relie le nombre de sommets, le nombre d'arrêtes et le nombre de faces. Là, c'est quand il est connexe puisque c'est ça qui va nous intéresser. Et quand le graphe est triangulé, ben on a un rapport entre le nombre de phases et le nombre d'arrêtes. He chaque phase voit trois arrêtes, tr demiarrêtes. Et un petit calcul nous montre que le nombre d'arêes, c'est euh 3s - 6. Et du coup, on arrive à la conclusion que comme chaque sommet voit enfin chaque arrêt est vu par deux sommets, euh on a strictement moins de six voisins en moyenne. Donc il y en a au moins un qui a moins de strictement moins de six voisins. Et c'est là qu'on va attaquer le truc. Donc qu'est-ce qu'on va faire? C'est que on va prendre le graphe, on trouve le sommet qui a le moins de de voisins, on l'enlève. On colorie le reste du graphe par hypothèse de récurrence. Éventuellement, on retriangule mais et puis ensuite on regarde est-ce qu'on arrive à colorier le sommet qu'on a rajouté qu'on avait enlevé. Alors si ce sommet il a 1 de ou tr voisins, c'est bon parce que il voit trois voisins. Donc il voit trois couleurs. Là il y en a au moins une 4è qu'on peut mettre. Alors, il reste 4 et c voisins. Donc, on va regarder les quatre voisins. Donc, on enlève le sommet, on colorie le reste. Qu'est-ce qui nous pose problème? C'est quand il voit les quatre couleurs. Dans tous les autres cas, on s'est coloré. Alors, qu'est-ce qu'on fait là? On va regarder les composantes bicolore connex. Pas très compliqué. Là, vous voyez que ici c'est jaune, que en face on a rouge. On va prendre tous les points ici qu'on arrive à atteindre à partir du jaune par un chemin qui est jaune rouge. Et pareil ici. Alors, deux possibilités. Soit ces deux oreilles sont connectées, soit elles le sont pas. À l'intérieur de la composante, bah, on peut inverser jaune et rouge. Ça reste bien coloré. Donc si elles sont pas reliées, on inverse jaune et rouge dans l'un des deux parce que sinon on a perdu. Donc comme ça et du coup bah on peut mettre pardon. Ah catastrophe. Du coup faut pas trop bouger quand on parle. Voilà du coup je peux mettre jaune au milieu. Donc là ça va. Par contre, si elles sont reliées, ben là, si j'inverse jaune et rouge, je vais avoir rouge ici, mais jaune ici, ça marchera pas. Mais qu'est-ce qui se passe? On est plaire. On est plani sur quand on est sur un tort, il faut plus de couleurs. Al, il y a un truc très drôle, c'est que les théorèmes, c'est pas quatre couleurs, mais sur des surfaces de genre supérieur, il faut plus de couleurs. Mais alors là, les les preuves sont elles marchent. On sait le prouver sur le papier. C'est vraiment pour le plan que que c'est compliqué. Donc on va on dire oui mais du coup j'ai pas de chemin jaune bleu entre ça et ça parce que il faudrait que je je coupe là. Donc du coup je prends la composante bleu verte ici ou là j'inverse les deux et du coup j'ai libéré le verre et c'est bon. Donc ça ça marche que si c'est connecté les autres couleurs elles le sont pas c'est ça que donc ça c'est bon. C'est pas c'est bon. Et le fait est que la preuve fausse de Campe, on peut la sauver en la la dégradant en preuve du théorum des cinq couleurs. Alors, l'erreur de Campeu, elle est marrante. Euh donc, on a cinq voisins et on a les quatre couleurs. Donc, c'est un truc de ce genre-là. Par symétrie, on peut se ramener à ce cas-là. Alors, que dit Kempu? Il dit premier truc, on regarde si un chemin jaune vert le vert entre ça et ça. Si on a pas on inverse l'un des deux et c'est bon. S'il y en a un, bah on va regarder s'il y a un autre chemin bleu jaune cette fois entre le bah le bleu et le jaune. S'il y en a pas, on inverse et c'est bon. On va inverser le jaune pour éviter de casser le vert là. Euh et là si on est dans ce cas-là, il dit pardon c'était quoi les hypothèses pour choisir bleu et vert au début? Il fallait qu'elle soit pas consécutive. Ouais, c'est les deux couleurs. On prend leisse une fois. Le bleu, tu vois que tu as chaque couleur euh tu as quatre couleurs. D'accord. Donc il y en a deux qui sont de la même couleur. Donc tu regardes le bleu qui est celui qui est entre les deux. OK. Celui qui est entre les deux autres. C'est ça la symétrie. Euh OK. Et alors là, qu'est-ce qu'il dit? Bah oui, mais là mes oreilles là, bah je peux regarder la composante rouge jaune. Elle va être enfermée dans cette oreille bleue verte. Ici, je peux regarder la composante rouge verte qui est enfermée dans cette oreille bleue et jaune. Je peux inverser là et là. Et puis du coup, j'ai récupéré le rouge. Très joli. Donc ça c'est c'est la preuve fausse. Où est-ce qu'elle est fausse? C'est vache. C'est que il avait pas pensé que les oreilles là elles pouvaient se recouper. D'accord. Là vous voyez que le bleu jaune il passe au lieu de passer comme on pense naturellement de ce côté-là, bah il passe là. L'autre il passe de l'autre côté. Ici un bleu. Et après, j'ai du mal, mais de toute façon, c'est pas grave parce que de toute façon, j'aurais pas le temps à bien expliquer les erreurs. Mais en gros, les inversions qu'on a faites là sur les rouges, il y a un moment ça va rater, ça va ça va ça va euh ça va se ça va foirer. Donc ça marche pas. Donc on arrive si on se ramène à si on dit cinq couleurs, ça suffit. On a droit à cinq couleurs, on s'en tire. Euh mais ça rate et donc il y avait un contreexemple de Hewood qui montre que vraiment on peut pas sauver cette preuve. On peut la sauver mais c'est quand même plus compliqué. Euh donc là c'est le début des preuves correctes et donc c'est cette idée d'inévitabilité. Alors, en gros, ça c'est pas formel euh comme ça dans la preuve, mais l'idée c'est qu'au lieu de regarder le sommet qui a le moins de voisin, on regarde celui qui a moins de voisin de distance 2. Et là, il y a beaucoup de cars possibles. Euh mais c'est une combinatoire qu'on arrive à faire à la main. On va être capable d'identifier fini de configuration pour ces pour ses voisins. Donc ça c'est quelques configurations. Ça c'est dans l'article de 95. Donc là, les sommeils sont écrits de manière un peu différente, des points noirs, des points blancs et cetera, ce qui correspond au nombre de voisins. Euh et en fait dans la preuve de 95, il y en a 633, dans la preuve de 76, il y en a 1400. Mais on peut montrer que cette ces ensembles sont inévitables, que en gros, on a soit l'un de ces cas-là ou alors éventuellement on dans des cas qu'on sait trivialement résoudre, enfin facilement résoudre un petit peu comme le le le voisin, bah le cas des voisins 4 par exemple. Et euh le truc qui est amusant, en 76, on a dit "Bah oui, il y a 1400 K, donc il fallait l'ordinateur." En fait, c'est pas du tout ça. Les 1400K, surtout en 76, ils ont été construits à la main. Et euh Ken Apple, son fils s'appelle Andrew Apple, il est professeur d'informatique à Princeton aujourd'hui. Il était adolescent à l'époque. Il a dû euh participer là à la à l'élagage des cas sur la table de la cuisine à l'époque. Donc 1400, c'est beaucoup mais c'est pas ça qui est vraiment beaucoup hein. Ce qui va vraiment être beaucoup, c'est l'opération de recoloriaiage qu'on a fait. C'est le ce raisonnement qu'on a fait sur les trucs avec les quatre voisins. Si c'est comme ça, je recolorie comme ça, comme ça, comme ça. C'est là qu'il va y avoir une coubinatoire énorme. C'estd que juste traiter un seul de ces cas-là, en particulier les cas qui arrivent après qui sont plus gros, bah ça ça prendrait un temps qui serait plus grand que d'écrire toutes les maths qui ont été faites jusqu'à maintenant. Enfin bon, il y a des comparaisons un peu comme ça. Euh voilà, donc c'est là qu'arrive le le calcul. Donc j'espère que ça restera euh un petit peu frais dans nos têtes demain parce que on va s'arrêter ici et du coup ben on finira le la preuve des quatre couleurs. Je dirai deux trois mots sur la la formalisation et puis après je montrerai l'interface de preuve. Voilà. Merci beaucoup. Merci. Est-ce qu'il y a des questions? Oui. Ben oui, plein de questions. Ben, je fais un des deux euh sur les donc sur les choses qu'on a démontré là, sur les deux exemples que je vous ai donné, il y a un exemple qui a été fait en HOL et l'autre qui a été fait en coque. Est-ce qu'il y a une raison de d'utiliser plutôt HOL ou plutôt cof? Euh alors le en en fait, tu mets le doigt sur un truc où euh parce que le discours est est vrai euh Coque est mieux armé pour les calculs que HOL et il n'empêche que euh ils ont préféré le faire en HOL pour diverses raisons parce que il y a pas mal d'analystes qui avaient été formalisées par en HOL parce que je crois qu'il connaissait John Harrison, des choses comme ça. Euh et du coup, je pense que ça met plus de temps à être vérifiant en Hol mais enfin n'empêche qu'on a la preuve en HOL et ça et ça passe. Euh oui, vous avez dit que le lambda calcul quand on rajoute leage, c'est plus sur complet. Ouais. Sauf si on rajoute la récursibilité. Ouais. Mais ça, est-ce qu'on peut le faire dans le formalisme de L de calcul ou pas? La récurivité dans le formalisme de rock. Bah le est-ce que dans le l de calcul on peut exprimer le fait qu'il y a l'autoapplication tout en ayant le alors simplement typé? Quand on est dans le lampe à calcul simplement typé, on peut plus appliquer x à x donc on a pas et on peut pas faire de point fixe donc on peut en l calcul simplement typé en fait on peut construire assez peu de programme là en dans la partie de la théorie du type que j'ai montré juste en ayant ce ce récurseur sur les entiers sur les listes et sur des choses plus complexes on peut déjà faire beaucoup de choses. OK. Euh mais par contre finalement c'est pas tellement ce qui des fois ce qui est en pratique est un petit peu agaçant, c'est pas tellement des questions de calculabilité du genre telle fonction, elle est juste pas définissable parce que les fonctions qui sont pas définissables, c'est les fonctions qui grandissent extrêmement vite. À la limite, on peut faire des des trucs pour calculer quand même, c'est que des fois ça nous empêche de définir les fonctions de la manière d'une manière aussi simple qu'on aimerait. Donc quelquefois on est un peu embêté par par ce trucl. Euh après, il y a des versions de types qui sont assez complexes. On peut quand même écrire X appliqué à X dans certains cas, mais n'empêche que ça va quand même terminer. Donc là, on rentre dans des trucs logiques un petit peu euh poussé et qui finalement sont pas pas le truc le plus le plus important. Ça veut dire que le il est quand même défini dans un système de type où c'est cohérent qui permet le deamel, il nous permet de deveniring complet. Euh mais on en a besoin pour ça. On a besoin d'avoir le ou alors des fois on peut tricher aussi à certains types un peu bizarre, on peut faire des constructions, on peut retrouver le lettre mais bon. Euh donc la l'intérêt du système de type pour un langage de programmation comme Okamel, c'est pas de garantir la terminaison puisque justement on veut on veut pas la terminaison. Enfin, on aimerait bien avoir un langage où on peut écrire tous les programmes qui terminent et pas les autres. Mais ça ça n'existe pas. Le problème de l'arrêt indécidable. Euh donc il garantit d'autres choses. Euh en gros, il nous permet de d'exécuter les programmes efficacement, de compiler sans avoir des erreurs d'exécution bizarre, des secfold ou des choses où on pense qu'on a un entier, en fait, on a une chaîne de caractère et ça fait n'importe quoi. C'est plus à ça que ça sert. OK. Mais c'est une bonne remarque quoign. Ouais. Mais les types en langage programmation finalement sont introduits pour d'autres raisons que qu'en logique. Bien. Y a-t-il une autre question? Moi, j'ai euh Oui, le langage de coque, ça ressemble au Camel, mais est-ce que c'est indépendant? Est-ce que c'est indépendamment ou bien c'est le même noyau qui est fait en même temps? Alors, non, c'est pas le même noyau. Euh et c'est assez amusant parce que les deux ont été développés dans la même équipe et l'un pour implanter implémenter l'autre. Euh et euh alors par contre ce qui se passe dans le cas de LINE, alors c'est un petit peu eux ils disent c'est le même, on utilise le même langage et sauf que il y a une condition de typage plus stricte pour les termes liges qui sont vus comme des des termes de preuve et ceux qui servent à implémenter le langage. Alors du coup, je pense que ça simplifie certains trucs d'implémentation mais cela dit c'est une publicité qui est un petit peu je sais pas si mensongère mais on a dit que c'est un peu exagéré parce qu'en fait euh on pourrait penser que du coup L est plus rapide que Rock alors qu'en fait il est plus lent. Il est bout de frappé il est écrit en ligne il est présenté comme bout de frappé. Ouais, il est présent. Ah bah il est bout Ouais, il est bout de frapper. Ouais, il est une 4 et après ils ont toujours Mais il y a deux niveaux de typage du coup il y a un typage fort pour les termes qui sont vus des termes preuves de de ligne ou des objets liges et puis un typage plus restreint. On a droit au trec pour la partie qui écrit le proveur. OK, on va s'arrêter. Je propose qu'on remercie