X-UPS Days 2026: "Formal Verification of Proofs" – Sébastien Gouzel 2

[musique] [musique] J'y vais. Donc c'est la suite d'hier. Je sais pas si vous vous rappelez un petit peu ce qu'on dans ce qu'on a fait. Je vous avais raconté une preuve au tableau. Une preuve qui était qui était bien parce qu'elle était elle était jolie et puis elle mélangeait pas mal de math et puis elle était pas complètement triviale non plus. Euh et après je vous avais montré à quoi ressemblait sa preuve dans le logiciel LIN qui est un assistant de preuve comme Rock, comme Isabelle, comme d'autres. Euh jeis pas du tout rentré dans les détails, mais c'était juste pour vous donner une intuition de à quoi ça pouvait ressembler. Euh et j'avais choisi cette preuve parce que ça impliquait des maths un peu compliqués. Il y avait des nombres réels, il y avait des espaces vectoriels, il y avait de la topologie, il y avait des suites extraites, il y avait des espaces propres, il y avait il y avait pas mal de choses comme ça. Euh et un de mes buts c'était de vous expliquer que euh si on veut formaliser des maths, il faut s'appuyer sur des résultats déjà existants parce que parce que sinon il y a juste trop de choses à faire. les maths, c'est énorme. Euh et donc je vais vous parler euh de euh d'une bibliothèque de mathématiques formalisé comme ça qui est celle sur laquelle je me suis appuyé qui s'appelle Matlib et que je vous présente ici au tableau. Vous cherchez Matlib dans Google ou dans votre dans votre logiciel de recherche préféré, vous trouverez ça facilement. Euh c'est une bibliothèque qui a une particularité, c'est qu'elle est complètement open source, c'est-à-dire que tous les contributeurs sont bénévoles et euh considère juste que c'est important de développer cette bibliothèque. Et donc les gens proposent proposent des améliorations, ils voient les tas de la bibliothèque, il disent "Ah mais moi j'adore ces matelas et c'est quand même une honte que vous ayez pas ce théorème." Et on lui dit "Ben, donne-nous ce théorème et il y a des interactions comme ça." C'est pas forcément facile d'avoir euh enfin de de rajouter du code à Matlib parce que c'est quelque chose qui est déjà assez gros et dans lequel il y a des règles de codage. Et c'est un peu comme Wikipédia pour que ça fonctionne bien, il faut qu'il y ait des règles. Il faut que tout le monde adhère à certains principes et donc c'est pas le processus pour avoir des choses dans Matlib est pas forcément très facile ou très lisse. Je vais pas vous vous dire le contraire. Ça prend du temps mais n'empêche que c'est ouvert à tout le monde et donc si ce soir vous vous ennuyez dans votre train en rentrant et et ben je vous invite à installer alors mais peut-être même que vous allez voir un tout petit peu tout à l'heure avec Patrick à quoi ça ressemble en rentrant chez vous. Alors non dans dans le train le wifi de la SNCF ne vous suffira pas pour installer à Matim mais éventuellement avec votre téléphone il y a une chance que ça marche. Euh donc vous pouvez installer Matlib. Il y a les explications sur cette page. Il y a un piège, c'est pour installer MATLB, il faut pas, si vous avez une distribution Linux, il faut pas utiliser le paquet de la distribution. C'est pas bon. Il faut aller voir sur cette page ou sur la page du langage de programmation officielle. Euh et vous pourrez jouer avec Matlim. La première chose à faire, c'est de démontrer des petits énoncés qui vous amusent. Le but c'est pas de contribuer tout de suite à Matib et puis après je je sais pas il y a un exercice que vous avez proposé à vos élèves et ben essayez de voir si vous pouvez le formaliser puis après des choses un petit peu plus compliquées puis une fois que vous êtes à l'aise vous là là vous regardez le contenu de la bibliothèque et vous dites ah mais là c'est ridicule qu'il ait pas cet énoncé de triangularisation simultanée de matrice qui commutent comment ça se fait qu'il y ait pas ça que ça y est pas je vous dirai pourquoi ça y est Euh je vais vous montrer ce qu'il y a en gros. Alors, c'est pas tout à fait euh vrai, mais là sur cette page euh à gauche, il y a un truc qui s'appelle Library Overview. et je vais aller voir en particulier ce qu'il y a dans les maths euh élémentaires entre guillemets. Les maths élémentaires entre guillemets, c'est ça veut à peu près dire jusqu'au niveau agrég. Et en fait cette page là, je crois que c'est Patrick qui l'avait créé, c'est il a pris le programme de la Greg de l'année N. Ça devait être il y a 2 ou 3 ans. 2020. Il y a 2 ou 3 ans. 2020. Il y a 2 ou 3 ans. Si on enlève le Covid entre les deux. Euh et il a regardé ce qu'il y avait, ce qu'il y avait pas. Et au donc il y a 3 ans, en 2020, il y avait pas grand-chose mais au fur et à mesure la bibliothèque s'est développée et maintenant il commence à y avoir euh pas mal de choses comme vous pouvez voir. Euh alors en algè linéaire euh quel est Hamilton, c'est bien le lem de chour, l'exponentiel de matrice, un petit peu de théorie des groupes. Il doit y avoir silo. Ah il y a pas silo, mais c'est peut-être que silo est plus au programme de la Greg. Silo est plus au programme de la Greg. Ça va jamais? Non, ça jamais été. Non, c'est pas parce que tu OK, d'accord. [rires] Bon, si l'o devrait être au programme de la Greg, si l'eau donc est évidemment dans la bibliothèque Matlib, mais il est pas là parce que il y a des gens qui pensent qu'il devrait pas être au programme de la Greg. Donc, il y a un peu de théorie des anneaux, un peu de forme bilinaire, enfin voilà ce à quoi vous attendez, un peu d'analyse réelle, un peu d'analyse complexe, de topologie, euh théorie de la théorie de la mesure, probat, distribution. Alors, et il y a aussi des choses qui n'y sont pas parce que parce que c'est développé par un par des gens qui ont un temps fini. Là, il y a les topiques not yet in matb et donc là vous pouvez voir qu'il y en a un petit peu. Il en il y en a beaucoup moins que ce qu'il y a et puis en plus là c'est un mensonge. Il y a plein de trucs qui sont encore sur cette liste mais qui ont déjà été mis dans Matlip depuis. Bref, ça commence à être quelque chose de bien développé euh grâce, je pense à ce modèle open source qui fait que quand un matu est intéressé, il commence à jouer, il se prend au jeu et puis après il dit bah je pourrais participer. Mais c'est comme ça que ça grossit de manière incrémentale. [grognement] Et là il y a un risque quand ça grossit de manière incrémentale avec des gens euh qui viennent d'horizons différents et qui apportent des cultures différentes, des points de vues différents. à la fois c'est une richesse, à la fois c'est un danger parce que s'il y a quelqu'un qui arrive et qui dit euh je suis prof de prépa et j'adore les matrices 33 parce que mon rêve c'est de faire calculer des déterminants de matrice 33 à mes élèves. Très bien, c'est respectable mais les matrices 44 ça compte aussi. Donc ça serait bien d'avoir pas juste les matrices 33 ou les matrices 44. Il faut avoir les matrices NN. Et puis en fait les matrices, c'est quand même alors ça sert en tant que tableau de nom, mais c'est aussi une abstraction des applications linéaires. Donc à la limite, j'ai envie de dire c'est plus important d'avoir les applications linéaires que les matrices. Et là vous avez le droit de pas être d'accord avec moi, mais moi je suis d'accord avec moi. Euh et si vous introduisez l'application linéaire, c'est quoi le bon degré de généralité? Parce que OK, vous pouvez dire "OK, je prends les applications linéaires sur un espace vectoriel réel de dimension finie, peut-être aussi complexe ou peut-être sur n'importe quel corps tant qu'on y est." Et puis pourquoi dimension finie après tout, il y a pas de raison. Et puis puis pourquoi sur un corps? Parce que il y a des gens qui font de l'algè linéaire sur des anneaux puis parfois même sur des anneaux non commutatifs et puis et puis où est-ce qu'on s'arrête en fait? Et c'est une vraie question. C'est une vraie question parce que la personne qui est intéressée par le déterminant des matrices 33 absolument rien à faire que les enfin est presque embêté que les espaces vectoriels s'appellent pas espace vectoriel mais modules parce que c'est sur des anneaux généraux et qu'est-ce que c'est que cette généralité qui va m'embêter? Et donc il faut il faut choisir un certain degré de généralité et il faut le faire de manière un peu uniforme au sein de la librairie pour qu'il y ait une unité et que ça fonctionne bien. Et donc là il y a il y a un groupe de dictateurs. C'est un groupe hein, c'est collectif et qui essa d'imposer une unité comme ça et de faire en sorte que quand on parle d'une application linéaire, bah c'est la même application linéaire qui va permettre de définir les dérivées d'une application. Et euh quand vous allez parler de groupe de galois, ça va être les mêmes applications linéaires. Et en fait dans tout MATLIB, il y a un seul type d'application linéaire et c'est le même partout. Et donc pour pour faire ça, il faut que toutes les maths qu'il y a dans Mat lib qui sont quand même assez assez variées se parlent les unes aux autres. Et donc là, il y a un travail d'unification à faire. C'est ça. Bourbon. C'est ma phrase d'après. Ma phrase d'après, c'est il y a une approche bourbaquisante là-dedans. Il y a clairement une approche bourbaquisante. Euh et il y a aussi cette approche bourbaquisante du point de vue de la généralité. Parce que si on choisit dès le début de dire que les applications linéaires c'est juste sur des espaces vectoriels sur des corps et ben un jour on est coincé parce que ça nous empêche de développer un certain domaine des maths. Et le but ultime de Matlip c'est pas juste de faire le programme de la Grec. C'est alors c'est très ambitieux, peut-être trop, mais c'est de pouvoir un jour développer la majeure partie des mates de recherche qui se font aujourd'hui. Et pour ça, bah il faut avoir une vision assez large et il faut développer les objets de manière vraiment générale. Et ça parfois c'est un obstacle aussi dont on est conscient et c'est un choix qui a été fait dans cette bibliothèque et c'est un choix qui conviendra pas à tout le monde parce que justement pour calculer des déterminés dans matrice 33 ça rend les choses plus compliquées. Mais Mikala en parlait ce matin que euh c'est important aussi qu'il y ait différentes bibliothèques parce que parfois on n pas besoin du même degré de généralité et la généralité qui semble indispensable à quelqu'un peut être un frein pour quelqu'un d'autre. Et donc je ne dis pas que Matlip c'est la c'est la bibliothèque universelle qui va contenir à tout le monde. Absolument pas. C'est une bibliothèque où on essae voilà les bouquins de Bourbaki. Ils sont très bien pour certaines personnes. Il faut pas les donner à un étudiant. C'est pas comme ça qu'il va apprendre les espaces vectoriels normés. Voilà. Donc c'est bourbquisant de manière délibérée. C'est c'est un choix et c'est un choix dont on s'est rendu compte dans beaucoup d'exemples de de la pertinence. Et donc il y a tout un travail de construction de librairie à faire comme ça où il faut vraiment réfléchir au maths qu'il y a derrière et pas euh juste à l'implémentation. Il faut dire qu'est-ce que j'ai envie de mettre dans la bibliothèque et pourquoi? À quel degré de généralité? Est-ce que ce qu'il y a dans les livres ça convient bien ou en fait est-ce que est-ce que Bourbaki n'est pas assez général? Il faudrait pas qu'on aille un peu plus loin. Je suis sérieux sur certains exemples. Il y a des exemples où on va plus loin que Bourbaki parce que Bourbaki n'est pas assez général. Bref, c'est ça dont j'ai envie de vous parler aujourd'hui de ce processus de construction d'une bibliothèque. Alors de cette bibliothèque encore une fois euh ce que je vais vous raconter aujourd'hui s'appliquera pas à toutes les bibliothèques. Ça ça s'applique à cette bibliothèque matib bourbquisante euh que vous pouvez prendre soit au sens péjoratif, soit au sens mélioratif euh suivant les goûts des uns et des autres. Et donc aujourd'hui, je vais vous parler de dérivées et de calcul différentiel dont Mikael vous a déjà parlé ce matin dans Rock mais en parlant de dérivée en dimension 1. Et moi, j'ai là, je vais vous parler de dérivée, de calcul différentiel en dimension supérieure. Donc la définition classique que vous allez trouver dans les livres, même chez Bourbaki, c'est que vous prenez deux espaces vectoriels. Alors non, chez Bourbaki ça sera pas comme ça, mais vous prenez deux espaces vectoriels réels normés. Est-ce qu'il y a des différentiels comme ça en prépa? Oui. Sur l'espace vectoriel normé? Oui hein. Oui. Dimension fin. Dimension finie. Ouais. Mais là ça ne change rien hein. Voilà. Donc euh F est dérivable. S'il y a une application linéaire continue, alors en dimension finie, elle serait automatiquement continue, mais là c'est important de demander. Telorsque Y est proche de X, fy, bah s'est approché à l'ordre 1 par cette application linéaire. Autrement dit, le on demande s'il y a un espace tangent au graphe de la transformation. Définition tout à fait classique et extrêmement importante parce que quand on veut comprendre les applications, souvent le premier réflexe, c'est de voir si un modèle linéaire nous dit des choses. Donc cette application elle est unique et ça s'appelle alors la dérivée ou la différentielle de f en x. Et il y a plein de notations qui sont pas cohérentes d'un endroit à l'autre. Et je je jonglerai entre les trois notations. Peut-être même parfois TXF quand je mettrai mon chapeau de géomètre différentiel. Euh il y a aussi une notion de dérivée en dimension 1 euh dont Michel parlait tout à l'heure et qui est qui est pas tout à fait celle-là mais qui est un cas particulier de celle-là. Si on identifie si on identifie les applications linéaires de R dans R avec la valeur de ces applications linéaire en 1. Donc c'est la même chose modulo un isomorphisme euh qu'on a tendance à penser totalement transparent mais si un jour on veut formaliser les choses et ben il faudra appliquer l'isomorphisme et donc on pourra par exemple déduire la dérivée en dimension 1 de celle-là. On va pas refaire deux fois la la même chose. On va déduire une théorie de l'autre. Si on veut déduire une théorie de l'autre, c'est important de commencer par la théorie la plus générale qui implique la particulière. Ça peut pas se faire dans l'autre sens. Donc on se dit que c'est la bonne définition, que c'est comme ça qu'il faut faire et puis après on commence à écrire des énoncés. Voilà un énoncé typique. Vous prenez une fonction de R dans R dérivable en en à droite de zéro. Don la dérivée en zé est strictement positive. Alors à droite de 0 f(x) strictement plus grand que f0. Bien sûr, c'est c'est vrai et c'est pas une application de la définition au-dessus parce que là, j'ai pas dérivé dans tout un voisinage de zéro, j'ai juste dérivé à droite. Et donc si on veut pouvoir écrire cette proposition dans votre livre ou dans ou dans votre bibliothèque de calcul formel, bah c'est c'est important de généraliser un peu la définition qui est au-dessus et de l'avoir non pas juste dans un ouvert autour d'un point, mais dans certains domaines autour de points. Et en fait, il y a plein d'exemples où c'est pertinent d'avoir des domaines et pas juste des des ouverts. Donc une fois qu'on a vu cette définition, on la traduit et alors je vais faire exactement comme Michaela ce matin. Elle vous a dit la première fois qu'on écrit la définition de dérivée, on se rend compte qu'il y a cette notion de fonction totale ou pas. Et ce ce qui ce qui est ce qui est important, c'est que une fonction est telle fonction comme dérivée. Il faut inclure le fait que la fonction est dérivable en ce point-là. Et c'est exactement ce que dit euh cette définition as f dévein at, excusez-moi pour mon accent anglais. Euh ça dit que la fonction f euh au point x, alors j'ai même un pointeur, cette fonction f au point x et à l'intérieur de l'ensemble s va avoir cette fonction fe. Ça c'est l de dans f. C'est les c'est les applications linéaires de continu de E dans f. Donc f va avoir f pr f prim comme dérivée dans l'ensemble s au point x. Si bah f yy - fx - f' de y - x, c'est négligeable. Euh par rapport à la dérivée à la différence y - x quand x tend vers s euh quand y tend vers x, c'est ce que dit cette notation. Et là ça disent quand tend vers x à l'intérieur de l'ensemble S. OK? Et ensuite, on dit qu'une application est différenciable à l'intérieur de l'ensemble S au point X si il existe une dérivée. Et là euh c'est pas très pratique à manipuler. C'est exactement ce que Michela vous a raconté ce matin. Ça veut dire que là pour l'instant vous avez pas de moyen d'écrire la dérivée de F. Vous avez moyen de dire f a f prime comme dérivé. Il y avait une question. Oui, en fait, E F, ils sont finis avant ou euh Oui, j'ai pas écrit ce qu'il y a au-dessus là. Pour toute cette section, fixons K un corps normé et E et F deux espaces vectoriels normés sur K, pas forcément de dimension finale. Donc là, je vous ai dit ce que c'est avoir que FA F prime comme dérivée, mais je vous ai pas dit de manière d'écrire ce que c'est que la dérivée de F, mais c'est pas très pratique parce que parfois quand on veut écrire des formules, on voudrait pouvoir mettre la main sur ce que c'est que la dérivée de de f. Et alors, exactement comme Michela disait ce matin, un moyen de dire ça, ça serait f déveait une dérivée, ça mangerait quoi? Ça ça mangerait une fonction, un ensemble, un point. Et puis pour que ça ait vraiment un sens, on dit que ça serait bien quand même qu'on ait le droit d'écrire ça que si la fonction est différenciable en ce pointl. Et donc, il faudrait peut-être aussi lui fournir une preuve du fait que f est dérivable en x. Et donc f dérive, ça mangerait tous ces objetsl et ça renverrait l'application linéaire qui est la dérivée de f en en ce point x à l'intérieur de l'ensemble S. Et en fait ça c'est pas pratique comme Mikaela vous l'a expliqué ce matin avec l'exemple de la division par zéro. Écrire ça à chaque fois ça devient insupportable. Si vous voulez écrire euh la dérivée de cosinus et ben vous aurez besoin de montrer à chaque fois que vous l'écrirez que cos est dérivable. OK, pour cosinus ça va. Mais si vous avez exponentiel de 3 cosinus x + 7x et si à chaque fois vous devez vous taper à la main la preuve de la différence, ça ça devient juste insupportable. Exactement comme la division par zéro. Et donc la la solution dans ce genre de cas, c'est dire et ben la dérivée, on va la définir dans tous les cas et soit la fonction est dérivable, on va renvoyer la la dérivée et soit la fonction est pas est pas dérivable et à ce moment-là on s'en moque parce que de toute façon on l'utilisera jamais. Donc on va renvoyer un truc arbitraire. et un truc arbitraire euh le plus simple à prendre souvent c'est zéro. Donc on prend zéro. [grognement] Euh donc là je vous ai dit à quoi ça devrait ressembler. Et en fait la définition que je vous écrite ici c'est pas tout à c'est pas tout à fait ça. C'est encore pire. C'est euh je dis si la fonction admet l'application linéaire nulle comme dérivée alors je vais utiliser celle-là. Sinon si la fonction est différenciable je vais prendre une dérivée qui marche. Alors là je suis à l'intérieur d'un ensemble. il y a pas unicité des dérivées a priori, donc j'en j'en prends une et si la fonction est pas dérivable, je prends zéro. D'accord? Alors, pourquoi ce choix-là au début, la première fois qu'on a écrit la définition de dérivée dans ligne, on n'avait pas celle-là? Et [raclement de gorge] puis beaucoup plus tard, on s'est rendu compte que c'était très bien de mettre ça. Ça ça implique par exemple que la dérivée de n'importe quelle fonction est mesurable. Ça serait pas le cas si là vous mettiez n'importe quoi. Mais si vous choisissez zéro, dans ce cas-là, les choses se se passe mieux pour certains se énoncés et ça ne coûte rien le reste du temps. Donc autant le mettre ça a des avantages et ça n'a pas d'inconvénient. Donc ça dire que c'est le seul cas au lieu de juste de dire on en choisit une, tu dis vraiment laquelle. C'est ça. Si s'il y a un choix et que zéro marche et ben je vais faire le choix le plus malin. Je vais prendre le zéro. Donc ça c'est une définition totalement non constructive. C'est quelque chose avec lequel le noyau ne calculera jamais. Mais c'est pas grave parce queon va pas demander au noyau de calculer sur cet objet là. On va démontrer les théormes avec cette définition. Donc une fois que j'ai fait ça, ça c'est à l'intérieur de cet ensemble S. Et ben je je donne aussi des définitions quand S c'est l'espace entier parce que souvent quand même euh on utilise les définitions dans l'espace entier. Et puis à partir de ça, on en déduit aussi des définitions spécialisées en dimension 1 parce que en dimension 1, on a envie de penser à F prime comme un réel et pas comme une application linéaire. Mais elles sont toutes ces définitions supplémentaires sont construites [grognement] à partir de ces trois briques de base, disons. Donc le zéro ici, c'est une valeur par défaut qui rend service quand la fonction est pas dérivable. Ça ça fait que quelques théorèmes sont sont vrais, même sans hypothèse. Si je prends l'exemple euh de Mikela de ce matin, elle vous a dit que si vous voulez avoir un lè qui vous dit que x sur x = 1, là il faut une hypothèse que x soit non nul. Par contre euh ce que je vous dis c'est que a + b/ c a/ c + b/ c. [applaudissements] Là, il y a pas du il y a pas besoin de l'hypothèse que C est non nul. Mikela vous a dit que maintenant quand C est nul, on dit que la division par zéro, ça fait zéro. Mais ça permet que ce genre de chos soit vraie toujours. Alors évidemment quand on va l'utiliser, ça sera toujours dans des cas où le dénominateur sera non nul. Mais il n'empêche que si quand vous appliquez ça, vous avez pas besoin de démontrer que le dénominateur est non nul, ça vous épargne un peu de travail. Et la flemme est un excellent moteur toujours. Pardon. Je pense qu'on est tous d'accord que la flemme est un bon moteur. Euh par exemple, tu auras pas en toute généralité F + G' = F + G si je en dimension 1 par exemple. Non, tu auras ça que si tu ajoutes une preuve que F et G sont bien fait. Exactement. En fait, les hypothèses comme ça ne viennent pas dans les définitions, mais pour la validité des énoncés, ça devient et donc voilà. Qu'est-ce que je disais? C'est ce que j'ai dit. Grâce à la valeur pratique zéro que j'ai mise là-haut. Une dérivée, c'est toujours mesurable. Et alors euh il y a quand même c'est il y a il y a une difficulté avec les domaines. Je vous ai dit que c'était important d'avoir des expéditions dans les domaines, mais ça crée des difficultés. En particulier la non unicité de la dérivée. Typiquement, c'est pas unique. Et là, j'ai mis un exemple tout bête. Vous vous prenez deux applications linéaires ly = x et m xy = x + y. Ouais. Tu veux qu'on leur avoue l'exemple le plus choquant d'énoncer unconditionnel ou tu veux on le sur la dérivée des fonctions de R dans R ou euh c'est le slide d'après. [rires] C'est le slide d'après. Ouais ouais oui. Enfin [rires] je je je sais pas si on pense au même mais euh donc ces deux applications linéaires. Bon bah comme l'application linéaire de R2 dans R leur leur dérivée partout c'est elle-même. Euh mais alors si je regarde la dérivée juste à l'intérieur de la droite horizontale, L et M, elles coïncident le long de la droite horizontale. Donc en fait comme dérivée, bah je pourrais utiliser soit L, soit M. Et puis même quand je pourrais utiliser L en à certains endroits et M à d'autres. Et comme ce f dérive within at ici est défini en utilisant cette fonction de choix dont on sait rien, si ça se trouve euh cet objet là il il est très moche. Peut-être qu'il alterne entre elle et M. Donc ça va créer des difficultés. Donc ça c'est un peu pénible mais c'est tellement important d'avoir des dérivées dans les domaines pour tellement d'applications dont je vous parlerai après que bah c'est un prix qu'on est à payer qu'on pardon c'est un prix qu'on est prêt à payer c'est dur à dire et parfois les choses se passent mieux quand même quand les dérivées à l'intérieur d'un ensemble sont uniques. Par exemple si si votre ensemble est ouvert et ben là il y aura pas de gag les dérivées sont uniques. Et quand les dérivées sont uniques et que les fonctions sont dérivables à l'intérieur du domaine, à ce moment-là, la dérivée de la somme, c'est la somme des dérivées. Exactement. Comme tu disais, il faut il faut ces trois hypothèses. On retire une une de ces trois hypothèses, ça devient faux. C'est ça. Donc ce matin, euh Michela a essayé de vous faire hurler en vous parlant de 1/ 0 = 0. Je trouve que vous avez pas hurlé très fort. Donc là, je vais vous faire hurler plus fort. Euh voilà une version du rôle qu'il y a dans Mat lib. J'aiécris la version formelle mais je vais vous lire la version informelle. Vous prenez A strictement plus petit que B pour que l'intégral soit bien ce qu'on pense et une fonction de R dans R qui euh à droite de A et à gauche de B a une même limite L. Alors, il y a un point à l'intérieur de l'intervalle où dérivé. Oui, toutes [raclement de gorge] les fonction sont si la fonction est dérivable, s'il y a un point où la fonction n'est pas dérivable, alors on prend ce point-là et ça marche. Et par contre, si la fonction est dérivable partout, bah là vous avez les hypothèses du vrai théorème de rôle et que vous savez démontrer en regardant un maximum ou un minimum. Bref, je je vais pas vous faire la démonstration de rôle. Euh et donc là ça ce ça a l'air complètement débile de l'écrire comme ça parce que évidemment à chaque fois qu'on va utiliser le théorème de rôle par exemple pour pour démontrer l'égalité des accroissements finis ou je ne sais quoi, évidemment on l'appliquera que à des fonctions dérivables. Donc à quoi bon l'écrire comme ça? Bah c'est exactement ce que je vous ai dit. Comme sur l'exemple là, s'il y a moins d'hypothèses à vérifier et ben ça fait moins de travail pour l'utilisateur. Donc votre théorème est plus facile à appliquer, tant mieux. Moi moi ça me demande un petit peu plus de travail de de le démontrer mais je fais ça une fois et les utilisateurs qui vont utiliser mon mon théorème des dizaines de milliers de fois au moins et ben ils auront un peu moins de travail à faire et donc globalement c'est rentable. Comment tu calcules ça? parce que euh et à un moment donné tu refuses de vérifier ces dérivés avant de calculer la dérivée mais en contrepartie chaque fois que tu faire un produit, une somme de machin ça à chaque fois vérifier que en plus à chaque fois vérifier que c'est vraiment rire. Alors euh c'est [rires] c'est un truc de toute façon que tu seras obligé de faire. Tu vois, quand tu vas dire que la dérivée de la somme, c'est la somme des dérivées, de toute façon, tu vas être obligé de de montrer que les fonctions sont dérivables. Quelle que soit ton approche, tu vas être obligé de le faire. Par contre, il y a d'autres exemples où avec une approche, tu seras obligé de le faire et avec une autre, tu seras pas. Donc, de toute façon, dans le cas où tu seras obligé de le faire, ça ne change rien. Tu ne gagnes pas, tu ne perds pas. Et par contre, dans les cas où tu peux gagner, tu gagnes. Je donne un autre exemple. caricatural. Si je vais écrire l'intégrale sur R de alors je vais essayer d'écrire un truc qui converge euh x2 sur euh log x au carré dx. Ça se trouve même ça ça se calcule ce truc. Voilà. Donc quand j'écris OK euh [rires] OK Alors ben euh x n'est pas compris. Voilà mine de 1x à la puissance 4. Voilà. Est-ce que vous êtes d'accord avec celui-là? Ouais. Autour de 0, ça c'est x2. C'est bon. et à l'infini euh c'est 1/ x2 et c'est bon aussi. Donc ce truclà euh c'est une intégrale. Si je voulais avoir le droit de l'écrire seulement dans les bons cas, à chaque fois que je quand j'écris cette intégrale, je devrais vous montrer que cette fonction est mesurable. Je voudrais je devrais vous montrer qu'elle est intégrable. Et si on poussait le vis jusqu'au bout et qu'on avait pas autorisé la division par zéro, j'aurais aussi besoin de vous montrer que le dénominateur est toujours non nul. Sauf qu'il est pas toujours non nul parce que en plus en zéro, j'aurais pas le droit de dériver, j'aurais pas le droit de diviser par par zéro. Donc en fait ce trucl c'est une fonction qui serait juste bien définie presque partout. Et si vous commencez à vouloir écrire ça en faisant comme on dit qu'on fait dans les livres, dans les livres, on dit on on intègre quand j'écris un signe intégral, c'est que parce que la fonction est bien définie et qu'elle est intégale et qu'elle est bien définie partout ou alors on fait des classes d'équivalen de fonction. Si vous voulez faire exactement comme dans les livres, ça devient juste totalement impraticable. Et donc le point de vue pragmatique dont Michaela a fait la pub ce matin, c'est dire et ben j'ai toujours le droit d'écrire ça mais si je veux montrer un théorème dessus, bah j'aurais besoin de vérifier la mesurabilité et l'intérabilité de cette fonction ou des choses comme ça. Et là si j'avais pas autorisé la division par par zéro, ça serait juste l'enfer. Mais de toute façon sur papier euh c'est exactement ça qu'on fait. on écrit les intégrales et on justifie jamais ou peut-être que à un moment on justifie l'intégrabilité une fois, mais après on écrit intégral et puis on se pose pas plus de questions. Et ben donc le fait d'avoir des valeurs par défaut comme ça, ça colle pas à la théorie expliquée dans les livres, ça colle à la pratique des livres et il se trouve que c'est beaucoup plus important de coller à la pratique qu'à la théorie. Les Mattheux ont souvent tendance à mentir sur ce qu'ils font vraiment et on s'en rend compte quand on fait des mathématiques formalisées. Donc ça a l'air évidemment faux mais en fait c'est bien juste évalidé par ligne parce que vous avez vu tout de suite que la dérivée est nul là où la fonction n'est pas dérivable. Maintenant, je voudrais passer euh en différenciabilité supérieure. Je voudrais passer sur les classes de fonction CN. Alors là, je dois avouer que j'ai plus aucune idée de si on fait du calcul d'IF en plus grande régularité en prépa ou pas avec des applications multinéaires et des choses comme ça. On va dire que oui. Euh donc voilà une définition qu'on trouve dans les livres, un bon livre de référence par exemple dans le bouquin de carton. Euh je prends deux espaces vectoriels réels normés E et F et une fonction entre ces deux espaces et on va définir par récurrence ce que ça veut dire d'être de classe CN. Une fonction0 si elle est continue, ça on dit qu'on sait déjà ce que c'est. Et euh une fonction va être Cn si elle est dérivable et si sa dérivée donc ça vraie dérivée parce qu'elle estable si sa dérivée est euh donc sa dérivée c'est une application de E dans les applications linéaires de E vers F. Mais alors E c'est un espace vector normé. Les applications linéaires de E vers F, c'est un espace vectoriel normé. Donc je peux utiliser ma définition par récurrence et ça a un sens de demander que la différentielle de f soit Cn- 1. [grognement] Donc là, j'ai définis ce que c'était que CN pour tout entier n et on dit que c'est C infini si on est CN pour tout N. Voilà. Bonne définition comme dans les livres. L de E dans F, c'est normé avec la norme d'opérateur. Euh voilà. Et alors évidemment après, on va faire des petits abus de notation parce que c'est comme ça qu'on fait dans les livres. La différentielle seconde, qu'est-ce que c'est? C'est une application linéaire de E dans les applications linéaires de E dans F. Et ça c'est pas très pratique à écrire, mais il se trouve que c'est identifié canoniquement avec les applications bilinéaires continues de E dans F. un objet là-dedans, ça mange un premier vecteur, ça renvoie une application linéaire et donc l'application linéaire renvoyée, je peux lui faire manger un deuxième vecteur. Donc ça mange deux vecteurs et ça renvoie un élément de fouve que l'application qui est construite comme ça, elle est bilinéaire et continue. Et en fait, c'est il y a vraiment une identification naturelle entre les deux, même espace vectoriel normé. Donc on va dire que c'est la même chose. On dans les livres, on dit que c'est la même chose. Et de la même manière la dérivée NM, c'est une application linéaire continue de E. Dans les app linéaires continu de E bla bla bla bla bla. Cette chose-là, c'est la même chose que les applications euh multilinéaires continuent en n variable, même en tant qu'espace vectoriel normé. Donc c'est comme ça qu'on y pense. C'est juste plus pratique à écrire. Donc voilà une très jolie définition qu'on pourrait qu'on pourrait implémenter dans Matlib. Euh sauf que non. Sauf que non parce qu'elle a plein de limitations. Première limitation c'est que c'était écrit sur R. Bon là c'est facile. Enfin il y a plein d'exemples. On fait de l'analyse sur C. Donc on on voudrait aussi savoir ce que c'est que une application CN sur C mais même sur d'autres corps aussi. sur CP, ça sert, ça sert un peu moins mais ça sert sur Cup quand même. Vous avez pas besoin d'être familier avec CP en fait, on aurait envie d'avoir cette notion pour n'importe quel corps normé. C'est pas gratuit, c'est parce qu'il y a des applications où c'est nécessaire de pouvoir parler de ces choseslà. Une autre limitation, c'est que là, je l'ai écrit dans l'espace entier, mais tout à l'heure, j'essaie de vous convaincre que c'était bien de pouvoir parler de dérivées dans des domaines. C'est pareil pour les dérivées itérées. On a on a besoin de pouvoir le faire dans des domaines. Par exemple, quand on fait la géométrie différentielle, il y a des variétés à bord. Les variétés à bord, bah il y a un bord, donc c'est dans des domaines. Et euh c'est pas gratuit. Euh le jour où on formalisera euh la preuve par Perelman de la conjecture de point carré, enfin le jour si euh bah la preuve de Perelman, elle repose sur une classification des variétés de dimension 3 conjecturées par stone et euh c'est des bouts qu'on recolle et les bouts c'est des variétés à bord. Donc c'est inévitable. Si on veut pouvoir faire ces matelas, il faut avoir des variétés à bord et donc il faut avoir des fonctions CN dans des domaines. Donc on peut pas s'en passer si on a une optique bourbakiste. Bourbaki revient. Euh Bourbaki avait compris un certain nombre de choses. Euh Bourbaki a un fascicule de résultats sur les variétés et il fait une hypothèse un peu bizarre, un peu bizarre à première vue, c'est il dit si euh votre corps de base c'est R ou C, ben je suis d'accord pour regarder des variétés de classe CN avec N entier supérieur galin arbitraire ou c'est infini ou euh ou même sur R ou C, je vais regarder des variétés analytiques aussi. Et par contre, si je suis sur un corps qui n'est pas R ou C, je ne regarderai que des variétés analytiques. Il fait comme ça et je vous dirai pourquoi tout à l'heure. Mais même si je vous dis pas pourquoi, argument de d'autorité, Bourbakiqui a certainement une bonne raison de faire ça. Et donc si vous avez envie de formaliser les variétés dans une bonne généralité, vous vous dites "Bah, c'est probablement une bonne idée de faire comme Bourbaki." Et donc il faudrait que je sois capable de dire ce que c'est qu'une variété Cn pour n qui serait soit un entier, soit l'infini, soit ωéga. Je veux pas faire d'un côté les variétés CN ou C infini et de l'autre côté les variétés C oméga et refaire deux fois des théories séparées qui se parlent pas. Parce que après si on démontre un théorème d'un côté, soit on oublie de le transférer de l'autre côté, ça pose problème, soit on le duplique et ça demande deux fois plus de travail. Donc la seule bonne manière de faire quand on boit ça, c'est dire OK si je pouvoir faire de la géométrie différentielle dans la bonne généralité, il faut que ma classe de fonction elle contienne aussi les fonctions analytiques. Et donc bah la définition des fonctions CN dans M libreintes d'application mais même si elles sont à long terme, c'est des choses qu'il faut essayer d'anticiper, bah une définition des fonctions CN dans Mat lib elle va devoir euh résoudre simultanément ces trois difficultés. Et donc je vais vous raconter comment on a fait et je vais pas vous dire la définition qui marche c'est ça parce que parce que c'est pas comme ça que ça s'est passé. L'histoire c'est que au début on s'est pas on s'était pas rendu compte qu'il y avait toutes ces difficultés et donc on a commencé par par écrire une première définition un peu naïve qui marchait pour certaines applications. Puis un jour, on est tombé sur une application plus compliquée, on s'est dit "Mince, la définition au début, elle était pas bonne." Alors, on l'a corrigé et en fait on a itéré ce processus parce que on se rend compte des difficultés au fur et à mesure qu'on développe les applications. C'est pour ça aussi que c'est important de faire des bibliothèques qui vont assez loin parce que c'est en allant assez loin qu'on voit les défauts de ce qu'on a fait au début. On passe son temps à améliorer la bibliothèque motivé par ce qui vient beaucoup plus loin en fait. Donc comment on peut essayer de définir les fonctions CN? Bah on va faire comme dans les livres. On va on va prendre la définition que je vous écrite qui était celle du bouquin de calcul différentiel de carton qui est un bouquin excellent. Euh ben on pourrait définir par récurrence la dérivée NM de F dans l'ensemble S comme la dérivée dans S de la dérivée N - 1 dans S. Je vous ai dit ce que c'était que les les dérivées à l'intérieur d'un ensemble, je peux les itérer. Donc voilà. Et ensuite, je vais dire que F et C, si toutes ces ces dérivées itérées comme ça jusqu'à l'ordre n sont euh bien définies et continues. Alors, [souffle coupé][soupir] malheureusement, il y a cette histoire de non unicité des dérivées dans les domaines. Je vous ai dit que tout à l'heure, si on regardait la fonction l y = x et qu'on regardait sa dérivée dans le domaine qui est l'axe horizontal, ça pouvait être quelque chose de discontinu parce qu'on pouvait faire à certains endroits un certain choix, d'autres choix à un autre endroit et de manière totalement arbitraire. Donc si je disais la définition donné plus haut et que j'ai pas eu de chance et que mon choix de dérivée était mauvais, il se pourrait que ma fonction L y= x ne soit pas C1 sur R0. Et là ça va pas. Ça va pas parce que on va quand même vouloir démontrer les théorèmes à un moment. Et dans les théorèmes, on a alors j'ai vraiment envie de dire qu'une application linéaire euh S1 euh j'ai envie de dire que si une fonction euh est C dans un domaine S et puis que je prends un domaine plus petit T, alors euh Cn et c'est euh F et CN dans T aussi. Il faut que il y ait des énoncés de cohérence comme ça. Sinon ça ça veut dire que j'ai raté ma définition et que je dois retourner à la table de travail. Donc cette définition là euh elle marche pas bien. Et pourquoi? Bah parce que la définition de f dérive within que j'ai écrite tout à l'heure, elle était, je vous ai dit, elle est totalement arbitraire. Il y a ce choix fait par l'axium du choix parce que il faut choisir une dérivée et c'est pratique de l'avoir sous la main, mais souvent ça se comporte pas bien. Donc euh il faut pas utiliser FDIN, c'est un objet qui est pas assez canonique pour nous donner une bonne définition. Donc une deuxième idée, ça serait de dire bah on va se demander s'il existe une bonne suite de dérivée itérée. Est-ce que il existe un choix de dérivée P1, P2, PN tel que PI + 1 dérivée de PI dans S et puis toutes elles sont continues jusqu'au rang N, un truc comme ça. Voilà, c'est ce que j'ai écrit. Donc si je mets deuxième tentative en haut, c'est que ça va pas marcher non plus. Mais euh enfin c'est que ça va pas marcher, c'est que ça ça aura encore des défauts qui seront un peu moins évidents. Donc on bah on va dire qu'une fonction est CN sur un ensemble S. Euh disons pour n en entier. Si euh j'ai une suite d'application euh Multilinéaire tel que PM + 1 et une dérivée de PM sur S. Voilà. et puis euh que la dernière PN soit continue. Donc ça, alors je l'encode par une structure formelle parce que c'est un truc que je vais vraiment utiliser après. Euh c'est la même chose. Je vais dire que F a euh cette suite de d'application PM comme que P convient comme série Taylor de F jusqu'au rang N. Euh si bah euh P0 c'est F et puis euh la dérivée de PM c'est PM + 1 et puis euh alors je voudrais dire que la dernière PN est continue et ça ça marche pas quand n c'est l'infini parce qu'il y a pas de P infini. J'ai juste envie de dire la dernière est continue et en fait une manière efficace de le dire c'est de demander que pour tout entier plus petit que N PM est continu. Bah de toute façon si M est strictement plus petit que N, on le savait déjà parce que c'était dérivable donc c'était continu et donc en fait cette chose-là ne dit vraiment quelque chose que sur la dernière si dernière il y a. Mais donc c'est cette chose que je vous ai écrite là, ça traduit exactement euh la définition informelle audessus. Et alors cette définition a un défaut. Alors pardon avant euh alors là je vous je vous ai dit que P0 ça devait être F et que PM + 1 M point c'est M + 1 que la dérivée de de PM ça devait être PM + 1. Et alors là il y a des trucs bizarres c'est curry 0 et curry left. C'est les identifications. Exactement. C'est les identifications que je vous ai dit que on fait tout le temps. Euh les applications linéaire de E dans les applications linéaires de E dans F, c'est la même chose que les applications bilinéaires de E au carré dans dans F. Et bah dans un bouquin, on en parle pas. Là, on est obligé de les mettre. Sinon, Line vous dit "Ben, je comprends pas de quoi tu me parles parce que la dérivée de ce trucl ça devrait être une application linéaire de E dans les application M linéaire. Et alors que ça c'est une application M + 1 linéaire, c'est pas la même chose. Donc il faut être pédestre, il faut être parfaitement précis, il faut lui dire et ben je prends ce trucl mais je le retransmets par l'identification pour que tu sois content et que tu comprennes de quoi je parle. Donc ça rend les choses un tout petit peu plus pénible mais en fait pas tant que ça. Vous voyez c'est quand même relativement léger ces identifications. Sauf qu'il faut avoir construit la théorie de ces identifications avant. Bref, cette définition, je vous dis, elle ne marche bien et pourquoi? C'est parce qu'elle est pas locale. Il se pourrait que que F soit CN sur S pour toute entier N mais qu'elle ne soit pas C infini sur S. Pourquoi ça? parce que peut-être que euh pour voir que F et C30 et ben vous trouvez une suite de dérivée P0 P1 jusqu'à P30 qui marche. Puis peut-être que pour voir que votre fonction est C40, vous trouvez une autre suite de dérivée Q0 jusqu'à Q40 qui marche. Ça se trouve Q n'a rien à voir avec P. Et pour 50, vous en avez encore une autre suite. Et puis et puis si elles ont rien à voir les unes avec les autres, pour voir que c'est infiniment dérivable, vous savez pas quoi prendre, vous avez pas de suite qui marche. Alors si vous êtes sur un domaine où les dérivées sont uniques, il va pas y avoir ce problème parce que par unicité les P et les Q ils vont être les mêmes et donc tout sera compatible et vous pourrez tout mettre ensemble. Mais s'il y a pas s'il y a pas uneité des dérivés, a priori c'est pas évident que il y ait cette compatibilité. Donc il y a un problème de de localité en en temps par rapport à N. Il y a aussi un problème de localité en espace. Si F C autour de chaque point, il se pourrait qu'elle soit pas forcément CN sur l'ensemble entier. Pourquoi? Parce que autour de X, vous savez que votre fonction est CN, ça vous donne une suite PN. Et puis autour de Y, vous savez que c'est CN, ça vous donne une suite Qn et puis sur l'intersection entre les deux, si ça se trouve, ça ne correspond pas. Alors si ça correspondait, s'il y avait unicité, il y aurait pas de problème. Tout se collerait bien et puis vous trouveriez un truc qui marche bien. Encore une fois, il y aurait pas de problème. Euh si ça correspond pas, alors si vous êtes sur R en dimension finie, vous pouvez utiliser des partitions de l'unité pour recoller les choses et pour résoudre ce problème. Si vous êtes pas sur R, si vous êtes sur C, vous pourrez pas faire ça parce que sur C, il y a pas de partition de l'unité. Si vous êtes sur R mais en dimension infinie, vous pourrez pas non plus parce qu'il y a pas toujours de partition de l'unité. Euh et si vous êtes sur CP, je sais pas. Mais c'est pas important de façon. CP c'est plus facile parce que c'est totalement discontinu, donc il y a moins de gag. Mais euh n'empêche qu'il y a une difficulté et donc bah il faut la résoudre et on va la résoudre en trichant. Euh on va imposer que notre définition soit locale. Je vais dire que f et Cn sur S en en un point X. Si autour de x je peux trouver une suite de dérivée qui convient et puis je vais imposer aussi une définition locale en en temps. Je vais dire que pour tout entier n prime fini, je peux trouver un petit voisinage autour de x où j'ai une suite une suite de dérivée jusqu'au temps m prim n prime. Et ça ça résout à la fois les problèmes de localité en espace. entend vous vous allez dire que c'est de la triche parce que bah non, on choisit une définition qui fonctionne. Cette définition fonctionne. Une fois qu'on a fait ça euh en un point, on dit que F et CN/ S, il y a les CN pour en tout point de S et ça résume de localité, du manque d'unicité. C'est c'est très bien, ça fonctionne très bien pour tout pour tous les entiers jusqu'à l'infini. Alors après, je vous ai dit par contre il faut aussi faire analytique parce que Bourbaki vous l'a dit et en général on fait confiance à Bourbaki. Euh on pourrait par exemple dire que F est analytique dans un ensemble S autour de X euh pardon que F alors je vais essayer de distinguer. Je vais dire analytique si ça admet un développement en série entière. Il y a une classiquement on voit plutôt ça en dimension 1 mais en fait il y a une notion qui marche dans tous ces espace vectoriel normés mais même en dimension infinie. Je vais pas vous en parler juste. Voilà ça existe les notions de fonction développable en série entière dans n'importe quel espace vectoriel normé. Et donc euh ben on pourrait dire que f et c om si elle est analytique. [raclement de gorge] Malheureusement là aussi, j'espère vous faire hurler un peu, euh une fonction analytique en un point n'est pas nécessairement C1 en ce point. Là, c'est pas un problème de formidation, c'est un problème de math. Euh, pardon, c'est par de fonction. J'avais pas compris comment on comment ça résolvait le problème de euh une fonction pourrait être Cn pour tout n mais ne pas être C infini. Mais c'est parce que je suis pas sûr. Parce que être euh être C infini par définition ici, c'est que pour tout nombre naturel N prime fini. Ah oui, d'accord. C'est j'ai une suite jusqu'à N prim. J'ai Oui. Et le M il va jusqu'à N prim. Oui, le M le la quantification. Le M il va jusqu'à N prim. Oui. D'accord. OK. Oui. Oui. C'est là tel que PM + 1 soit une dérivée de PM euh pour M + 1 plus petit que N prime. Absolument. Donc j'ai truqué ma définition pour résoudre le problème. OK, ça marche. Parfois, c'est une bonne manière de faire. C'est juste la définition pour c'est infini vraiment. Oui. Euh bah il y a aussi cette histoire de localité. Là, je l'ai fait en un point et voilà. Donc une fonction analytique en un point n'est pas nécessairement C1 en ce point. Là vous allez me dire ça va pas. Euh n'est pas nécessairement C1 en ce point si l'espace cible n'est pas dans un espace complet. Donc si vous faites il y a plus de complétude en préparable. Non non mais c'est pas grave, c'est pas vos étudiants qui sont là. Euh donc en en dimension finie, le problème n'existe pas parce que c'est toujours complet. Mais en dimension infinie, il peut y avoir des gags. Alors ça va pas parce que je voudrais qu'une fonction c oméga soit en particulier c'est infini et c1 et tout. Donc il va falloir que je change un petit peu ma définition. Alors j'avais fait un slide où je donnais l'exemple de fonction analytique qui n'est pas C1. Euh voilà. [souffle coupé] Si vous avez une question à la fin, je reviendrai. C'est même pas compliqué, c'est juste de la triche quoi. C'est euh on prend une jolie fonction analytique qui va dans un espace et puis en fait elle va dans un sous-espace. Enfin, on regarde le sous-espace engendré par les valeurs de la fonction. Et ce sous-espace, il est plus du tout complet. il devient trop petit pour que la fonction ait des dérivées dans ce nouvel espace parce que naturellement les dérivées ne vivent pas forcément dans le dans l'espace engendré par les valeurs de la fonction. C'est ça le gag. Voilà, il on pourrait imaginer que la dérivée vit toujours dans l'espace engendre mais non voilà, il suffit d'écrire un exemple. Le premier exemple auquel on pense il marche en il marche c'est un contre exemple. Donc ce que je vais faire, bah c'est que je vais je vais truquer encore plus ma définition juste pour que ça marche. Je vais dire qu'une fonction est c oméga si elle est analytique mais si en plus elle a une suite de dérivée et que toutes ces dérivées sont analytiques. Encore une fois, on a le droit de dire que c'est de la triche. Je suis en train de faire une la définition la moins naturelle possible. Si on voyait ça dans un bouquin, on dirait mais il faut que l'auteur pense à faire des définitions élégantes et pas juste des définitions qui marchent. Euh il se trouve que là ça a quand même le mérite de marcher. Donc voilà exactement la définition formelle d'une fonction CN dans un domaine dans Matlib. Euh alors con within at, c'est un peu long à la base. On appelait ça con within at pour dire que c'était plusieurs fois continuement différenciable et puis à un moment s'est rendu compte que le times, il était vraiment trop long et on l'a enlevé. Ce qui fait que là ça veut vraiment plus rien dire. Mais c'est comme ça ça veut dire fonction CN. Donc K c'est le corps qu'on regarde. N c'est le degré de régularité qui est soit un entier, soit l'infini, soit ωéga. J'ai une fonction, j'ai un ensemble, j'ai un point et donc je vais dire que la fonction vérifie tous les propriétés. Si alors si quoi? Si mon entier n c'est si n si c'est un entier ou l'infini, bah je vais demander, je vais prendre la définition de la troisème tentative. Je vais demander que pour tout entier m plus petit que n, il existe un voisinage de x et euh une suite de dérivée successive autour de x euh qui sont bien les dérivées qui fonctionnent. Donc juste sur ce petit ouvert autour de x et jusqu'à l'ordre m. Ça c'était la troisème tentative. Et pour analytique, une fonction analytique, ben je vais demander la même chose que j'ai un petit voisinage et une suite de dérivées successives tel que ce sont bien des dérivées successives et elles sont toutes analytiques. Voilà exactement la définition qu'il y a dans Matlib aujourd'hui. Je ne triche pas, je ne vous cache rien. Et là, on se demande est-ce que vraiment la définition est bonne? parce que il commence quand même à y avoir un degré de complexité tel que on a pu se planter à plein d'endroits. Et puis je vous ai pas dit ce que c'était qu'un espace normé mais il faut voir attention, il faut faire attention à comment c'est défini. Là il y a des filtres de voisinage. Est-ce qu'on a bien défini tout ça? Et puis les séries multilinéaires, là il y a un vrai risque que ces définition soient mauvaises. Là j'aurais pas envie d'axiomatiser un truc comme ça. Donc pour me convaincre la bon j'ai essayé de vous expliquer pourquoi la définition était bonne. Peut-être que je je vous ai arnaqué quelque part. Et donc là le test du feu, c'est essayons de démontrer des théorèmes avec cette définition là. Et en fait, une fois qu'on aura démontré les théorèmes, on reviendra plus jamais à la définition précise. On utilisera juste les propriétés de cette définition parce que c'est ça qui compte. Pardon. Oui. Un point qui me qui me choque un peu, c'est que il a jamais aucune condition sur l'ensemble S. Oui. Oui. Et ça c'est quand même un peu étonnant. Alors, le but du jeu, c'est d'écrire une définition qui euh qui fonctionne bien pour la plupart des ensembles, mais il y a plein d'énoncés, il y a plein de les les conditions analytiques Ouais. sont c'est un peu étonnant qu'on qu'on Bah, cette définition est faite pour marcher euh à peu près tout le temps, mais quand on voudra démontrer un théorème intéressant, il y aura besoin d'hypothèse sur l'ensemble S. Par exemple, est-ce que la dérivée seconde est symétrique? La dérivée de secondde est symétrique. Si s est un convexe d'intérieur non vide. Si c'est est arbitraire, la dérivaison peut être atroce. Donc dès dès qu'on va dès qu'on va vouloir faire des des maths un peu intéressantes, on mettra des hypothèses sur S. Mais on a envie ces hypothèses de les mettre dans les théorèmes intéressants et pas dans la définition. Exactement comme pour toutes les raisons que j'ai expliqué ici. Moins on met d'hypothèse dans la définition et plus elle est confortable à utiliser. C'est un peu le point là de cette définition. Je vous montre deux trois propriétés qui sont vraies. Euh voilà. Crash test. Est-ce que on peut démontrer des trucs un peu cohérents? C'est monotone. Si une fonction est CN et que M est plus petit que N, alors M F est cm. Quel que soit le domaine, OK? C'est une bonne chose. En particulier, une fonction céga et c'est infini, c'est une bonne nouvelle. Je vous ai dit qu'il y avait un gag dans les espaces pas complets pour les fonctions analytiques. Quand quand l'espace est complet, C oméga et analytique, c'est la même chose. Là, c'est un théorème qui est je vous montre pas les preuves, je vous montre des énoncés qui sont aujourd'hui dans Matlib et qui montrent que cette définition fonctionne. Euh alors pour n qui n'est pas l'infini, une fonctionn dans un ensemble en un point. S'il y a un voisinage où elle possède une série de Télor jusqu'à l'endro N et en plus si N c'estga tous les termes de la série de Tor doivent être analytique. C'est pas vrai pour c'est infini cette chose-là parce qu'avec ma définition [grognement] une fonction vous regardez une fonction de R dans R et vous et vous supposez que sur l'intervalle -1/ n 1/ n elle est exactement cn. Plus vous vous rapprochez de zé et plus elle est régulière. Avec ma définition, cette fonction est c infini en zéro. On peut discuter de si c'est une bonne définition ou pas, mais avec la définition que je vous écrite, cette fonction est infinie en zéro et par contre, il y a pas de petit voisinage où elle est c'est infinie. Par contre, en dehors de ce gag de fonction C infini, euh être CN, c'est quelque chose qui passe sur un petit boisinage et c'est ce que dit Solem. Euh autre exemple dénoncé qui fonctionne, une fonction est Cn + 1. Si est seulement si localement, elle a une dérivée qui est Cn. Et en plus, si je parle de fonction C oméga, là il faut que la fonction soit analytique aussi. C'est encore faux pour n é= l'infini pour la même raison que celle que je vous ai dit avant. Donc voilà, encore un autre crash test. Si j'ai deux deux fonctions FG qui sont CN sur un domaine, leur somme est CN. Ça dépend pas du domaine. Je c'est vrai tout le temps. Euh comment on démontre ça sur papier? Euh bah typiquement, on fait une récurrence sur n. Pour n = 0, c'est facile. Et pour n positif, on a envie de voir que f + g est dérivable, pas de problème. Et puis que la dérivée de f + g est cn - 1. Donc là, je fais la preuve sur papier. Donc en pensant à la définition sur papier de des fonctions CN, celle qu'il y a dans le bouquin de carton. Donc pour voir qu'une fonction Sn, je dois voir que sa dérivée est CN -1. Et c'est quoi la dérivée de f + g? Bah c'est df + dg. Et donc j'applique mon hypothèse de récurrence à df et dg et je vois que c'est CN -1 et tout va très bien. Donc ça c'est la protte sur papier qui marche très bien et qui ne marche pas dans mon cas parce que elle va pas s'appliquer à C oméga celle-là. Parce que pour c oméga ma récurrence ne descend pas. Pour c pour c pour c oméga et ben je dois voir que la dérivée c'est oméga et la dérivée second c'est oméga et ça se la queue et ça n'avance pas. Euh donc je vous donne une autre preuve. Euh comme F et G sont des fonctions CN, elles ont des séries de telor jusqu'à l'ordre n [grognement] euh et à ce moment-là la somme des séries telor c'est euh c'est une série telor pour jusqu'à l'ordre n pour f. On l'écrit et c'est trivial. Et donc F + G a bien une série Télor jusqu'à l'ordre N et donc elle est bien CN. Ça c'est une définition qui fonctionne bien avec la c'est une démonstration qui fonctionne bien avec la définition formelle que je vous ai donné avant. Et en fait, c'est [grognement] comme ça qu'on démontre le théorème. On démontre pas avec cet argument inductif qui en plus aurait des problèmes au niveau des univers pour ceux qui sont experts. Donc comme on a pris une définition un peu tordue, ça force à donner des preuves parfois un peu plus compliquées. Alors là, pour la somme c'est pas compliqué mais pour la composition, le fait que la composition de fonction Cn et Cn, ça se fait très très bien par récurrence. Par contre, si on doit donner une formule pour la dérivée NM de F rong, ça existe. He, ça s'appelle la formule de Fad Bruno, mais c'est un peu désagréable à écrire. Bah là, on n pas le choix. On a dû écrire la formule de Fad Bruno pour la composer pour montrer qu'une composée de fonction CN et CN. Bon mais en même temps la la formule de F Brune c'est c'est très pratique après pour obtenir des estimés sur sur les dérivés itérées et donc ça sert aussi pour développer la théorie des distributions. Donc on était très content de l'avir. Alors il me reste 5 minutes. Donc là je vais faire un tout petit saut conceptuel. Je vous ai dit au début, on est motivé par par des applications un peu plus avancées. C le fait de faire cette définition un peu compliquée, c'était pas gratuit, c'était parce qu'on Et donc bah dans Matlib, on est arrivé jusqu'à un cadre où on peut faire ces applications un peu plus avancées et vérifier que ces définitions compliquées des fonctions CN, elles fonctionnent. Et donc l'application un peu plus avancée, c'est les groupes de lit. Euh alors quand on a deux champs de vecteur, disons dans un espace vectoriel, on peut définir un truc qui s'appelle leur crochet de vie et qui mesure vous suivez le flot de V puis le flot de W où le flot de W puis le flot de V, il y a il y a souvent un petit écart entre les deux et ce petit écart, il est mesuré par un champ de vecteur qui est le crochet de lit de VW et pour lequel on peut écrire une formule complètement pédestre. La dérivée de W appliquée à V moins la dérivée V appliquée à W. Quand on écrit la définition comme ça, on se dit que c'est un peu arbitraire et que c'est pas forcément un très bon objet. [grognement] Euh mais il y a une remarque conceptuelle qui dit que c'est un bon objet, c'est que euh le crochet de lit, ça commute avec euh la composition par des fonctions. Vous avez un difféo local, vous prenez deux champs de vecteur, vous les tirez en arrière par votre difféo local. Et à ce moment-là, le tirer en arrière du crochet de lit, c'est le crochet de lit détiré en arrière. Et comme le tirer en arrière c'est quelque chose de complètement canonique, bah quelque chose qui commute avec ça, ça dit que c'est un bon objet. Donc le crochet l c'est un bon objet. Alors à condition d'avoir des dérivées secondes symétriques, mais on sait bien que les fonctions C2 ont des dérivées secondes symétriques au moins sur R. Donc donc le crochet de lit est un bon objet. Et cette invariance, ça dit que cette chose là qui est définie dans l'espace vectoriel, ça passe au cas géométrique des variétés qui sont des objets localement modelés sur des espaces vectoriels. Par exemple, la sphère. sur la sphère où vous avez deux champs de vecteur liss et ben vous pouvez définir leur crochet de lit de la manière suivante. Vous vous prenez un isomorphisme local avec un espace vectoriel, vous calculez le crochet Lit dans l'espace vectoriel, vous revenez sur sur la sphère et l'invariance par diffal vous vous dit que ça dépendra pas du choix de diffal que vous avez choisi et donc c'est quelque chose qui est bien défini sur la sphère. Et donc une fois que vous avez ça, vous pouvez euh faire de l'algèbre sur les groupes de lit. Les les groupes lis, c'est des variétés, donc des objets localement volés sur RN dans lesquels il y a une multiplication, une inversion qui vérifie les règles des groupes mais en plus qui sont lisses. Et quand vous avez une structure comme ça, vous en déduisez une structure algébrique très intéressante sur l'espace tangent l'identité qui s'appelle une structure d'algèbre de lit. Vous prenez deux vecteurs et vous vous savez leur associer un troisième vecteur. Et il y a plein de manières de faire mais voilà une manière de faire. Vous avez vos deux vecteurs dans l'espace tangent à l'identité, vous les poussez partout dans le groupe par multiplication à gauche. Donc vous obtenez des champs de vecteurs sur le groupe. Là vous prenez le crochet lit des champs de vecteurs. Je vous ai dit que c'est quelque chose qui avait un sens. Ce crochet de lit, vous le regardez en l'identité. Donc partant de deux vecteurs en tangent à l'identité, j'en ai construit un troisème. C'est ça le crochet de lit. Alors c'est le même nom que le crochet lit des champs de vecteur mais parce que ça a la même origine si si vous voulez. et euh pardon et tout se passe très bien. Euh pour avoir une adep de lit, faut il faut avoir plein de propriétés euh du crochet lit. Mais là ça va être vrai parce que c'est vérifié par le crochet lit des champs de vecteur en général. Et donc voilà une manière de construire le les crochets de lit sur sur les groupes de lit. Et comme on a défini les fonctions CN sur des corps arbitraires, on est content. Là, ça marche. Si vous voulez faire des groupes de lit sur CP, et ben vous avez des groupes de lit sur CP. Alors pas tout à fait parce que pour quand je vous dis les les crochets sont bien définies, il y avait quand même cette hypothèse que les dérivée secondes devaient être symétriques. Alors quand quand on est sur R ou sur C, les applications C2 ont des dérivées secondes symétriques. Et ça c'est assez facile à voir. Enfin c'est vrai mais avec des hypothèses plus faibles. C'est vrai si votre application est différenciable autour du point et si la dérivée est elle-même différenciable en le point qui vous intéresse. Il y a aucune il y a aucun besoin d'hypothèse C1, rien, c'est juste différenciable et la dérivée est différenciable au point. Si vous essayez de le faire comme ça, c'est plus dur mais voilà donc parce que la dérivée seconde, il y a une formule limite et cette formule limite est complètement symétrique en V et W. OK. Euh et si on est sur un corps arbitraire, les fonctions analytiques, ça a toujours une dérivée symétrique parce qu'une une fonction analytique, c'est un développement en série entière et vous pouvez écrire la la dérivée seconde en fonction du développement en série entière. Et la dérivée seconde en fait, ça va être le deuxième terme de vos développement en série entière mais symétrisé. La dérivée seconde appliquée à une paire de vecteur VW, c'est P2 de VW + P2 de WB. Et ça c'est symétrique. Par contre, en général, si vous êtes sur Cupé, il y a des fonctions C infini dont les dérivées de secondes ne sont pas symétriques. Je suis désolé, j'ai pas le temps de vous faire l'exemple. Euh mais c'est pas compliqué. Vous pouvez même le faire faire à vos élèves. Alors peut-être pas surcuper mais sur vous prenez le produit de deux quantors triadiques et sur cet ensemble là vous pouvez construire une fonction c'est infini. Donc c'est c'est infini sur le produit des deux quant triadiques. Donc on calcule les dérivées juste en prenant des points qui restent à l'intérieur. Vous pouvez construire une fonction comme ça telle que df sur dxy ça fait 1 et df sur dyx ça fait 0. C'est même totalement explicite. Vous pouvez regarder dans les notes. Je crois que j'ai donné les détails. Donc c'est pour ça que là je passe plus vite. Conclusion de l'affaire, euh si vous voulez définir des groupes de lit, euh si vous êtes sur R ou C, ça va marcher dès que votre groupe de lit est disons c'est 3 parce qu'à ce moment-là, les dérivées secondes vont être symétriques. Et puis alors, il faut un tout petit peu plus de dérivées parce que parce que c'est comme ça. Euh par contre, si vous êtes surcupé, les dérivées secondes sur une variété C3 vont a priori pas être symétrique. Donc le crochet des champs de vecteur sera pas bien défini. Et si vous voulez que les choses soient bien définies, en fait vous avez intérêt à être analytique parce que si vous êtes analytique là des dérivées secondes sont bien définies sont symétriques et donc le crochet L sera bien défini. Et donc la la conclusion de cette affaire c'est que vous pourrez définir des structures de d'algèbre de lit sur l'espace tangent des groupes de lit. Si vous êtes C3 sur R ou C, mais si vous êtes surcupé, il vaut mieux être analytique. C'est ce que disait Bourbaki au début. C'est c'est pas pour rien qu' qui faisait ça. Et donc c'est pour ça que c'était important d'avoir cette class de fonction CN qui contenaient les fonctions C oméga. Et tout ça c'est pas du flanc. On l'a dans Matlib et ça marche. Ça marche. Et on a les groupes de lit à la fois sur QP et sur R ou sur C. Donc la conclusion de cette affaire, c'est il y a deux manières d'obtenir des bonnes définitions. Celle où dès le début on est génial et on sait ce qu'il faut faire et on écrit du premier coup la bonne définition. Ça c'est c'est ce qu'on aimerait faire. Euh et il y a la vraie méthode, ce qui arrive dans la vraie vie, c'est que on écrit une définition et puis au début on a l'impression qu'elle est bonne et puis un jour on écrit un théorème. On narrive pas à le démontrer en fait. qu'onarrive pas à démontrer parce que notre définition n'est pas adaptée. Elle elle était bien mais elle était pas suffisamment euh générale pour couvrir aussi cette application. Et donc là pour démontrer ce théorème, bah on répare la définition et puis on répare tout ce qu'il y a entre les deux. Mais ce qui est bien c'est que un assistant de preuve, vous le relancez, vous lui dites "Recompile-moi toute la bibliothèque." Il compile et un moment il vous dit "Ah non, là ça va pas." Bah vous vous réparez à cet endroit-là et vous savez une fois que l'assistant de preuve est content, il a refait tout le travail pour vous et vous savez que tout est cohérent. Et après vous continuez, vous redéveloppez et là vous rendez compte mince pour ma nouvelle application ma définition est pas bonne, il faut que je rechange. Et on itère ça. Et en fait on passe son temps à itérer ça. Et la la définition des fonctions cennes que je vous ai montré, je pense que c'est au moins la 4e ou la 5e itération. Et pour l'instant, elle est très bien celle que je vous ai montré. Et si ça se trouve je vous refis c'est être exposé dans 3 ans, ça sera peut-être plus la même définition. [grognement] Et bah c'est pas grave. Donc ça implique de faire ce qu'on appelle des refactorisations, de modifier la bibliothèque. Et je pense que c'est une morale cette histoire. Il faut être prêt à faire évoluer les bibliothèques. C'est des évolutions qui sont dictées par les applications qu'on découvre au fur et à mesure parce qu'on réussit jamais à tout anticiper. Je vous remercie. [applaudissements] [applaudissements] Merci beaucoup Sébastien. Oui. Oui. Ça tu as dit donc cinq itérations et combien de temps? Combien de personnes? Alors euh je pense que ça entre la première définition et celle-là, il y a bien eu tr 4 ans et euh c'est difficile de dire combien de personnes parce que les fonctions CN, c'est surtout moi qui les ai écrites euh mais les murs que les gens se prenaient c'était il partaient dans d'autres directions. Mo il disit "Ah bah là ça va pas." Et donc là il faut changer un truc. À ce moment-là, c'est plutôt moi qui changé le truc. Euh mais il y a pas que moi qui me suis pris des murs. Voilà. Ce qui m'étonne, c'est qu'il y a pas besoin de refactorisation des mathématiques. Ah, c'est une forme de refactorisation des mathématiques. Là, je t'ai dit que la définition qu'il y a dans cartant [soupir] n'est pas assez générale pour certaines appli le fasicule de résultat de Burbakiqui de géométrie différentielle. D'ailleurs, c'est un fasicule de résultat. C'est un des seuls où il démontre pas les choses parce que la géométrie différentielle se bourbakise pas très bien. Euh dans ce fascicule de résultat, ils font pas ils font pas les variétés à bord parce que c'est encore plus pénible. et et donc tu pourras jamais formaliser la conjecture de point carré avec Bourbaki. Donc c'est alors je sais pas si c'est une refactorisation des des mathématiques mais on continue à écrire des choses de plus en plus général ou dans des directions qui sont dictées par les applications. Quand l'URI fait des infinies catégories, on peut dire que c'est que c'est une refactorisation des mathématiques. Quand Scholsu fait des ensembles condensés, on peut dire que c'est une refactorisation des mathématiques. Sauf que souvent c'est pas des refactorisations, c'est des nouvelles théories qui viennent se rajouter à ce qu'on avait avant. On nass pas ce qu'on avait avant. Mais dans une bibliothèque comme ça, tu as pas envie d'avoir ces espaces vectoriels de dimension finie. Et puis après, il y a Scholzo qui arrive et qui nous dit "Ah mais on pourrait aussi faire des espaces vectoriels en dimension infinie." Enfin quand arrive et nous dit "On pourrait aussi faire des espace en dimension infinie" et ben nous on a tendance à à brûler le truc de dimension finie et à tout refaire à partir de la dimension infinie. Est-ce est-ce que c'est finalement euh euh efficace parce que visiblement l'approche des mathématiques comme ça où les choses se développent sans brûler justement sur avant euh c'est quand même assez efficace. Ah c'est beaucoup plus efficace. C'est infiniment plus efficace. Euh mais quand tu écris un papier, tu as une latitude. Tu comptes sur la fluidité de pensée de ton lecteur. Tu peux très bien utiliser un résultat de la théorie écrite de telle manière et puis un résultat de Schols écrit dans une théorie un peu différente et dire mais les deux ils s'appliquent évidemment à ce que je suis en train de faire et donc je me sers des deux. On passe son temps à faire ça. Et avoir une fluidité d'esprit comme ça, c'est pas tellement compatible avec les math formalisé. Mais on peut dire que c'est un défaut des maths formalisé. C'est c'est plus rigide et c'est à la fois un avantage, un inconvénient. L'avantage, c'est que à la fin c'est un rock mais ça demande de travailler un peu différemment. C'est un rock. Ouais. ça demande de travailler un peu différemment et euh en fait c'est c'est pour ça qu'il faut pas faire que des mathématiques formalisées, loin de là parce que quand tu as rigidifié, tu bloques un peu le progrès aussi. tu dis "Ah ben on a cette définition de fonction CN, moi j'aurais besoin d'une définition un peu différente et bah j'ai pas le droit parce que Sébastien Guisel a dit qu'il fallait faire comme ça. Ça c'est hyper malsin. Et donc les mathématiques sur papier qui croissent organiquement un peu n'importe comment pour inventer des nouvelles maths, c'est beaucoup plus efficace. Est-ce qu'il faudrait pas plusieurs mat avec des philosophies? Ah si, complètement. Complètement. Euh parce que là vous avez le avec option. Tout à fait, tout à fait. Et sont peut-être pas assez fortes pour refaire bah euh cette approche bourbaquiste, elle permet euh de faire beaucoup de math mais il y a un prix à payer comme j'ai essayé de vous expliquer. Et si tu vises un résultat un peu particulier où tu as pas besoin de de toute cette généralité, bah parfois c'est beaucoup plus économique de faire un truc un peu moins ambitieux. euh mais qui va plus directement dans cette directionlà et qui est peut-être plus facile à utiliser aussi pour les spécialistes de la de la théorie en question. Et c'est exactement ce que Michaela a raconté ce matin. Donc oui, je pense que c'est très important qu'il y ait différentes bibliothèques dans différentes directions avec différentes approches. Alors moi, j'aime bien l'approche bourbquiste comme ça parce que parce que c'est ma tournure d'esprit euh mais je suis pas du tout en train de dire que on doit faire que ça par de France on parlait de le forc avec des matri plus plus vieilles et avec une stratégie un peu différente qui va proposer d'autres d'autres orientations? Alors, ben pourquoi pas? Euh c'est bien, c'est de l'open source, donc n'importe qui peut repartir euh de ça à n'importe quel point, enlever les choses qui lui plaisent pas. Après euh ça ça sera quand même des efforts euh à grande échelle, mais euh faire euh un matlip pour les classes prépa où on est là et où il y a plus de filtre et des choses comme ça, euh bah pourquoi pas? Non, c'est pas lisible. C'est c'est magnifique. [rires] Mais j'ai des biais et je les assume et je dis que c'est très bien que tout le monde pas les mêmes billets que moi. C'est et même pire, c'est important. C'est quand même on peut dire que là tu as fait le choix de t'expliquer une histoire super mais où on arrive à une définition qui est un peu dégueu. Faut quand même Oui, absolument. Mais il y a aussi un instant tu as dit mot filtre le fait de au contraire ça pousse dans dans bien des cas ça nous a poussé vers des définitions plus belles quoi. Des théories qui sont vraiment plus élégantes que les trucs qu'on faisait avant quoi. Ah mais moi je suis tout à fait d'accord. Là du coup de ce point de vue là l'exemple que tu as montré aujourd'hui est pas très représentatif. Euh par parfois euh quand vous pensez aux limites euh il y a les limites en plus l'infini de suite de nombres réels euh ou des limites en plus l'infini de fonction et puis ça ça peut tendre vers plus l'infini, vers moins l'infini, vers une limite finie. Euh comme ça il y a assez vite 12 notions limite. Si vous avez envie de dire que si j'ai F qui tend vers L et puis euh et puis que G en L tend vers M, alors Gérond F tend vers M. Euh si vous avez 12 notions de limite euh ça ça fait 144 théorèm et puis le jour où vous rajoutez une 13e notion limite pour rajouter toutes les compatibilités vous passez à 169 théorèm et en fait c'est pas gérable sur papier c'est gérable parfaitement parce que vous dites c'est pareil et ce théorème de compétition limite je l'applique sans avoir besoin de le redémontrer. C'est c'est la pensée fluide mais c'est hyper bien la pensée fluide. C'est comme ça qu'on qu'on avance. Mais n'empêche que quand quand on formalise, on peut pas se permettre de faire ça. Et donc il a fallu trouver la bonne manière de formaliser les limites. Et la notion la la manière qui marche bien, c'est les filtres. Et au début, on se dit qu'est-ce que c'est que et en fait quand on est habitué c'est absolument génial et magnifique. Est-ce qu'on pourrait pas imaginer un système qui justement fait descendre un bout de matbéralité plus bas pour éviter de de voir développer 150 bibliothèques. Un truc un peu automatisé. Alors même sans parler d'IA. Alors, je je sais pas comment faire ça. Ouais, je sais pas comment faire ça. Euh je pense que c'est des beaux projets. Euh et je sais pas du tout comment faire ça parce que tu peux pas dire "OK, j'ai cette définition abstraite et puis euh [soupir] j'ai lag des trucs mais si tu les espaces uniformes, tu as plus R parce que R est construit comme comblion de Qul au sens d'espace." Et donc enlever des morceaux, c'est pas facile. Tout est très interdépendant. Donc prendre une hache pour enlever les les le fichier des groupes de lit, c'est facile parce qu'il y a pas truc de base qui va dépendre des des groupes de lit. Mais il y a d'autres trucs qui sont présentés de manière totalement nonémentaire mais qui servent pour faire des trucs élémentaires. Et donc là euh je pense que c'est pas évident. Par contre, faire une bibliothèque de déguisement de Matlib, tu pars de Matlib et puis tu reformules certains concepts et puis après tu dis à tes étudiants, vous avez juste le droit d'utiliser les concepts reformulés et interdiction d'utiliser les théormes de de Matlib. Ça c'est quelque chose qui est beaucoup plus raisonnable. Après ça s'appelle le prendre de prébace, c'està-dire qu'on une fonction sur un mouvert ou sur à gauche à droite. Vo c'est ça et ça je pense que c'est tout à fait c'est beaucoup plus raisonnable à faire de partir de matlib et de construire une surcouche qui disent vous avez le droit d'utiliser ça ça ça et ça et le reste niet. On perd tous les outils de Bah ça dépend comment c'est fait non? Tu pourrais garder toutes les tactiques et juste dire certaines définitions sont interdites. Non ça non. Si tu dis à ton alors moi je quand je code du ligne, je code du ligne à la main parce que je trouve que ça marche beaucoup mieux. Et pour les étudiants de toute façon, je pense que c'est très important aussi de faire comme ça parce que sinon ils apprendront pas. Et donc voilà, une bibliothèque avec des avec un nombre restreint de trucs utilisables. C'est tout à fait possible. D'ailleurs dans les notes, je crois que je donne un pointeur vers le Natural Number Game qui est une manière tout à fait pédagogique de s'initier à Line et qui est tout à fait faisable par des étudiants de première année de prépa. C'est démontrer les propriétés de base des ensembles des entiers de piano juste avec des axiums de base. Et bah là il y a plein de tactiques qui sont enlevées et on est forcé de comprendre ce qu'on fait à la main. Et bah c'est très rigolo et il y a plein de gens qui accrochent la ligne comme ça. Est-ce que dans l'enseignement, il y aurait une branche des mathématiques ou de l'informatique, je sais pas, qui serait à travailler sur le type de fix. Alors, je pense qu'il y a plein plein plein de choses à faire dans l'enseignement avec Line [grognement] et je suis très mal placé pour y répondre parce que un, j'enseigne pas beaucoup et deux, j'ai jamais enseigné avec Lin. Donc, il vaudrait mieux que tu poses la question à Patrick qui lui a vraiment fait ça avec ses étudiants et en plus a développé des euh des retranscriptions de ligne où le langage est un peu différent. Il appelle ça verbos line où c'est une syntaxe euh en français qui ressemble à des phrases mais une syntaxe assez rigide. et où tu racontes les preuves dans une syntaxe précise, mais c'est quand même du line. Et si j'ai bien compris, ça marche très bien auprès des étudiants. Il faut il faut peut-être qu'on arrête les questions. Peut-être une petite remarque pour terminer. C'est assez amusant parce que en en regardant ta conclusion là, ça m'a rappelé un exposé à l'IHP de Michel Mindz France dans les années 90 où pendant tout son exposé, je crois que c'était sur l'entropie des courbes, il changeait un peu sa définition et à la fin de l'exposé, il disait "J'ai donc démontré ma définition." [rires] Vous avez éclaté de rire et je vois que maintenant on est beaucoup plus sérieux quand il faut savoir qu'en ligne une définition et un théorème c'est des objets qui ont exactement la même nature. Donc démontrer une définition ou démontrer un théorème, pourquoi pas? Bon, merci encore.