X-UPS Days 2026: "Formal Proof Verification" – Micaela Mayero 2

Donc aujourd'hui, je vais vous parler d'analyse réelle, mais avant je vais faire un petit rappel de tout ce qui a dit hier que enfin essayer hein, je veux pas avoir cette prétention de faire un rappel de tout ce qui a été dit dans les trois exposés. Euh donc au niveau des preuves formelles, c'est une science jeune. Elle a que 50 ans. Alors 50 ans c'est jeune quand même. Euh les assistantes à la preuve, c'est c'est pas de la vérification, donc c'est vraiment euh prouver pour euh enfin vraiment avoir quelque chose de réellement prouvé comme on fait en math voir voire mieux qu'en math. Donc vraiment toutes les hypothèses du début à la fin et en particulier ce sont des outils et des enfin des assistants parce que par j'ai l'impression que certains hier euh pensaient que peut-être ça pouvait aider à faire la preuve tout seul. Ça ne fait pas la preuve tout seul. Il y a des outils euh automatiques, en particulier sur la logique du premier ordre où on appelle ça un peu les SMT solvers qui qui sont des outils thématiques qui font certaines preuves mais des preuves simples tout seul. Là c'est pas du tout l'outil ne fait pas la preuve. Il faut que l'utilisateur connaisse la preuve. il l'a il l'a saisi. Alors l'outil aide parce que vous vous souvenez en haut à gauche, c'était pareil en ligne, c'était en c'était sur la sur la droite plutôt enfin l'autre gauche. Enfin voilà euh à droite. Euh l'outil à chaque à chaque ordre, à chaque tactique qu'on lui donne, il il change qu'il y a à démontrer puisque il applique les il applique les règles et donc il change il nous indique ce qui reste à démontrer. Ça aide l'utilisateur mais ça ne fait pas la preuve à sa place. Euh alors, il y a plusieurs prouveurs, on a vu qu'il y en avait plusieurs, j'en ai cité plein hier. Et donc là sur les deux jours, vous allez en voir deux. Euh alors c'est il y en a pas un qui est meilleur que l'autre c'est-à-dire que les les querelles de clocher là où les prouveurs se pourrissent, c'est les uns et les autres. Ça c'est moi je suis pas du tout d'accord avec ça. C'est comme le langage de programmation, il y en a plein. Il y a des raisons à ça et ça dépend ce que vous voulez faire. Donc il y a à la fois Rock et LINE sont très bien pour faire pour faire des maths. Rock est aussi très bien pour faire la preuve de programme. Euh je pour faire des maths, je peux je ne peux pas ne pas citer Mizard. misard à une bibliothèque absolument colossale de formalisation des mathématiques dans un langage proche de celui des maths. Euh donc n'a rien inventé hein, c'est juste voilà. H donc il y a il y a plein de prouveurs et ça dépend beaucoup de ce que vous voulez faire. Donc moi, je suis vraiment pour cette biodiversité et chaque prouveur a ses avantages, ses inconvénients. On essaie d'améliorer en s'inspirant les uns des autres. C'est mais c'est une bonne chose. Euh il y a aussi plusieurs bibliothèques de formalisation des maths. Donc j'ai un peu la même chose que ce que j'ai dit tout à l'heure. Euh HOL par exemple HOL Lite euh a une très grande bibliothèque de d'analyse. Donc on et et il y a des il y a il y a tout un plan de recherche en ce moment enfin en ce moment depuis quelques années déjà où on essaie de traduire ou de développer des outils pour de traduction de preuvrouveur vers un autre. Alors, c'est pas forcément évident parce que comme vous l'avez vu, il y a ils sont basés sur des logiques différentes et des systèmes différents. Donc, c'est pas toujours pratique euh facile de traduire quelque chose euh où il y a l'action du choix en ligne 1 comme euh comme disait Sébastien hier, en dans un prouveur où on essaie de pas en vouloir ou on en veut pas ou voilà. Donc euh alors je vais je vais revenir aussi sur le danger des axiomes. Euh hier on a parlé de on peut énoncer un théorème ou un lè qui est faux. Alors en principe on appelle ça un axiome du coup mais il y a pas que les axiomes, il y a aussi les les admittes quand on alors en rock ça s'appelle admit et puis en ligne ça s'appelle sor. Donc j'ai mis j'ai mis les deux. Euh donc on admet quelque chose. Alors c'est souvent on l'admet pour le prouver plus tard parce qu'on se dit "Oh là là ça m'énerve ce truc. Euh voilà je je vais supposer que pour l'instant c'est bon et puis je vais continuer ma preuve ou donc c'est vraiment une méthode que d'ailleurs qu'on fasse les preuves en avant ou en arrière, ça change rien de ce point de vue-là. C'est-à-dire on admet des résultats intermédiaires parce que soit parce que ils sont triviaux mathématiquement mais que ils sont un peu pénibles à prouver. Voilà. Ou soit parce que ils sont pas triviaux mathématiquement mais on se dit "Oui, mais j'ai quelque chose d'encore moins trivial. Je vais supposer que ça c'est vrai pour pouvoir l'avoir dans le contexte." Mais n'empêche que un jour ou l'autre, il faut quand même l'éprouver parce que voilà. Ou alors ou alors avoir suffisamment de recul. Je vais je dis ça mais je vais dire un peu le contraire tout à l'heure. On en parlera. Euh alors toutes ces ces outils ont commencé par la recherche, on l'a vu hein, la recherche en logique, la recherche en math. Euh et donc c'est pour et par la recherche que tout ça est arrivé. Mais maintenant, depuis alors euh il y en a qui l'utilisaient déjà depuis longtemps pour l'enseignement, mais là maintenant c'est ça bouillonne. Euh je disais la formalisation des maes bouillonne mais l'utilisation des des outils d'aide à la preuve pour l'enseignement bouillonne aussi. C'est il y a deux bouillons euh qui qui sont pas forcément décorrélés d'ailleurs les uns des autres. Et donc c'est c'est pas mal utilisé pour l'enseignement. Donc je vais essayer de J'espère que je pourrais aller jusqu'à un quart d'heure de retard. Euh enfin qu'il faut que je finisse. OK. Super. Super parce que un quart d'heure de retard en plus du quart d'heure de décalage. Non non non non non quand même. Sinon on aura pas de pause. Deux fois un/ fait ouis. Et alors je reprends la phrase de Sébastien tout à l'heure. Il a dit tout à l'heure enfin hier tout est formalisable. Ouais, modulo un certain nombre de contraintes quand même et en particulier une des contraintes fortes qu'on a pas encore vraiment résolu. Alors ça s'est amélioré, c'est la contrainte temporelle parce que formaliser, il y a une question hier, je sais plus d'où ça venait, c'est combien de temps on met pour formaliser un le un théorème? déjà bon évidemment ça dépend du théorème mais je veux dire ça peut être très long et ce que je vais montrer tout à l'heure donc là on va s'orienter un peu alors je vais parler un peu enseignement mais aussi recherche et les recherches que je vais montrer ça on les a commencé en ça fait 25 ans qu'on les a commencé et voilà et finalement d'un point de vue mathématique on en est qu'au début alors alors ça c'est en rock parce que parce qu'on est académique après ligne ils ont une puissance de frapp on peut pas on peut pas lutter Mais je veux dire c'est voilà donc il faut vraiment mettre énormément énormément énormément de moyens humain voir il y a maintenant je bof oui enfin oui euh pour oui voilà il oui je on pourra en reparler plus tard voilà pour pouvoir formaliser les maths et et misard qui a une énorme bibliothèque misard ça fait 50 ans qui qui formalisent leur bibliothèqu Donc alors donc c'est l'inconvénient de la biodiversité a une difout Non parce que comme les ça dépend de quelle math on fait ça dépend quelle math on veut faire typiquement si vous voulez faire des maths constructives il faut bien des outils qui soient constructifs et voilà et et alors moi pour le coup je fais des maths classiques dans un outil constructif, mais pourquoi pas? Enfin voilà donc et un des avantages de ça dépend des outils, si vous voulez en extraire un programme après euh bien que je alors on peut extraire à partir de de choses un peu classiques, c'est possible. On peut par exemple sur l'équation des ondes, on a extrait une constante d'approximation. Voilà. Donc on peut quand même extraire certains contenus calculatoires et ça tous les outils le permettent pas. Donc voilà. Euh alors quel est là aujourd'hui on va parler des réels, des nombres réels. C'est quoi le problème avec les réels? Euh bah le les réels, c'est pas des flottants. Euh donc là si on ces trois exemples là, ils viennent de n'importe quel langage de programmation. en particulier, ils ont été tapés en eau camel mais ça pourrait être autre chose. Ce serait ce serait pareil. Vous voyez bien que ça c'est pas des chiffres c'est pas des chiffres un peu bizarres, un peu ésotérique comme 10^ 16 ou 10^iss 15, c'est pas c'est des c'est vous voyez que c'est des c'est des nombres tout à fait ordinaires. 1000 c'est pas c'est pas quelque chose d'incroyable et puis 7,5 c'est pas non plus quelque chose d'incroyable. D'accord? Et ce qu'on remarque, c'est que dès la troisème décimale et ben on a on obtient un résultat différent juste parce qu'on a pas mis les parenthèse au même endroit. Donc là, on parle de l'associativité de l'addition et l'associativité de l'addition, bah elle est très vite pas associative rapidement dans les dans les dans les ordinateurs parce que tous les nombres justement ne sont pas représentables. Alors, je vais pas vous faire un petit cours sur les flottants mais euh quand vous êtes quand vous tapez 1è, 1/10 n'est pas représentable avec un processeur binaire. Si vous avez un processeur décimal, il existe quelques processeurs décimaux. Dans ce cas-là, vous pouvez représenter un 10, mais sinon, c'est pas représentable dans un processeur binaire. Donc du coup du coup bah c'est une approximation avec une norme d'erreur, une mentisse, vous savez quand on parle l'exposant, la mentisse, ce genre de chos. Donc du coup bah ça fait des approximations et mais nous on nous on veut faire des preuves. Je veux dire quand vous vous faites des preuves, si vous si vous supposez que vous n'avez pas l'associativité de l'addition, vous faites plus de preuve. Enfin, je veux dire c'est pas c'est pas une preuve, pas c'est pas des maths. D'accord? Donc nous on veut des preuves et ben c'est ce qu'on veut. Et donc du coup on veut quand même pouvoir avoir dans un prouveur bah des vrais réels, ce que j'appelle les vrais réels, pas pas des flottants. Enfin pour moi les flottants, c'est c'est faux réel. Enfin, c'est une approximation des réels. Et donc bah après, on se pose la question comment on fait pour formaliser les réels puisque des réels, il y en a plein. Donc vous avez les réels exacts, les réels non standard, vous avez des réels constructifs, vous avez des réels classiques. Bon, alors les nombres flottants qui sont quand même une approximation des réels. Vous avez de l'arithmétique d'intervalle qui sont aussi une approximation des réels. Donc c'est comme quand vous faites un programme, bah vous demandez quelle structure de données je vais prendre. Est-ce que je vais prendre des listes, des listes chaînées, des tableaux, des je sais pas quoi. Bah là c'est un peu pareil. Comment est-ce qu'on fait pour formaliser les réels? Et là on en revient un peu à la biodiversité. C'est-à-dire que euh moi pour le coup, je vais faire des réels classiques mais à NIMEG au Pays-Bas, eux, ils ont choisi de faire des constructifs parce que ils sont ils font des mates constructives et donc c'est forcément pas les vrais réels. Euh pas les pas les mêmes réels, pas pas les vrais. Si c'est des vrais réels. C'est quoi quelle est la différence entre nombre réel exact et nombre réel classique? nombre réel exact et nombre alors nombre réel exact c'est c'est c'est dans les dans les ordinateurs, on on suppose on alors je je vais pas en parler mais on on suppose que votre réel il est exact jusqu'à une une décimale que vous que vous fixez. Donc en fait, c'est une sorte de limite et puis vous dites bah euh je donc c'est Bum qui avait développé le premier c'est réel exact et donc vous pouvez calculer des choses en disant je veux que jusqu'à la 25e décimale je suis sûre que mon résultat est exact. Donc c'est ça se rapproche plus des enfin des flottants que des réels. On c'est c'est difficile de dire ça. Mais en tout cas c'est pour ça que ça s'appelle des réels exacts. C'est pas du tout la norme i3e 754 des flottants. Alors euh donc on se pose toujours d'un point de vue math, on se pose la question euh alors les réels, bah les réels déjà c'est pas dénombrables, hein. Donc on peut pas définir ça comme on a défini les entiers de péano euh avec un type inductif. Alors, il y a je mets simple avec un type inductif simple parce que il y a des tentatives et il y a même eu des formalisation où euh on définit les réels avec un type coinductif. message. Voilà, c'est une c'est une technique qui permet de de définir les digits par des par des streams, des choses comme ça, mais c'est pas enfin voilà, je c'est encore vraiment en balbuiment. Alors embalbucement depuis 20 ans mais c'est pas voilà, c'est pas c'est pas quelque chose qui est très bien stabilisé. Ouais. Voilà. Merci. Donc on peut axiomatiser les réels. Alors je viens de dire tout à l'heure que c'était pas terrible mais je vais y revenir. On peut les construire. Pour les construire bah il y a la méthode de Cochi Cantor, les coupures de DD King, tout ça, on le trouve dans pas mal de livres. Le Lando, Bourbaki aussi fait une construction des réels, ce genre de choses. Vous pouvez avoir les réels au premier ordre ou au second ordre. Alors au premier ordre, c'est pas tellement utilisable parce qu'en fait au premier ordre, on peut pas quantifier. Donc au premier ordre, c'est Tarsky qui avait fait ça qui disait tout polynôme de degré amber amé une solution. Alors mais sauf que le pour tout polynôme bah ça c'est pas du premier ordre. Donc en fait c'est pas finiment axiomatisable ou ou définissable que donc dans un système on peut pas faire quelque chose de de non de non fini. Euh et en logique, bah on se demande si on veut des classiques, des intuitionnistes. Donc la logique classique, c'est ce qu'on connaît tous, c'est comme à l'école, hein. Et la logique intuitionniste, bah le la la l'analyse intuitionniste, c'est Bishop qui est qui est qui est la référence qui est vraiment le livre de référence à un bouquin jaune où il y a vous avez tout. Alors ce qu'il faut savoir c'est que l'analyse intuitionniste, vous n'avez pas les mêmes énoncés que l'analyse classique. C'est pas seulement les mêmes preuve, c'est les mêmes énoncés. Par exemple, vous prenez le théorème des valeurs intermédiaires et ben euh tout est défini, vous avez des des normes où tout est inférieur à epsilon puisque vous ne pouvez pas décider est-ce que quelque chose est égal ou pas un inter ou dans un intervalle ou des choses comme ça. Donc c'est même les énoncés qui diffèrent. Alors les nombres réels dans rock, je vais me focaliser dans dans rock. Euh donc les premiers nombres réels, ils sont apparus assez tard. Euh en en 2000, ils ont été axiomatisés. Je vais revenir dessus parce que j'arrête pas de dire qu'axiomatisation c'est pas bien. Sauf que euh quand c'est trivial, on peut axiomatiser. Je je vais en en reparler juste après. Les opérations sont des fonctions totales. Ça ça je sais que vous allez quand je vais parler de ça, vous allez tous bondir de votre chaise. Je j'anticipe parce que je sais. Euh et puis la comparaison est décidable. Donc c'est ça donne un aspect classique, c'est-à-dire que on peut décider, mais ça vous le faites aussi. Vous le faites quand vous fait vos preuves, ça vous ça vous dérange pas de dire est-ce que un réel est égal à é. Si r est égale à 0 machin, bah donc là on va supposer que c'est décidable. Et ça c'est ça c'est purement ça c'est purement classique puisque on ne peut pas en fait dans la vraie vie, on ne peut pas décider si un nombre réel est décidable ou pas. Est-ce qu'un nombre réel est égal à pi? il peut être égal à 3 14 15 9 et puis après euh autre chose, je sais plus ce qu'il y a après le 9 d'ailleurs mais euh et voilà. D'accord. Et que ce soit pas égal à PI. Euh donc il y a une autre bibliothèque des réel qui est née à peu près qui est née en même temps par Milan Nik qui est une bibliothèque constructive des nombres réels. Donc ça c'est vraiment l'école constructive de Nimeg ou Naimeg une bibliothèque en 2013 qui a été faite par-dessus celle des réels justement parce donc c'est une extension c'est vraiment une extension et un peu plus convieval entre 2000 et 2013 il y avait des tas de d'outils de choses qui n'existaient pas en 2000 quand la bibliothèque des réel a été faite au départ et en 2013 bah COC a évolué COC a s'est modernisé Et donc il y avait des choses qui qui étaient plus sympa. Et donc c'est la bibliothèque Coclico, c'est une extension, elle est vraiment construite au-dessus des réels. Elle ne fonctionne pas sans sans les réels et en particulier elle étend complètement la notion de fonction totale plutôt que la fonction de type dépendant. Je vais y revenir. Et puis la bibliothèque des réels, elle a été aussi en 2020 augmentée en introduisant une partie commune euh réelle constructive. Euh c'est un travail que je voulais faire depuis longtemps mais en fait Vincent Séria euh l'a fait et c'est très c'est parfait. C'est-à-dire que maintenant la bibliothèque de rock, vous avez un socle commun qui vous permet d'avoir des réels constructifs jusqu'à un certain point et des réels classiques et puis après il y a divergence entre les deux. Alors euh les réels de la librairie standard de rock, du coup ils sont formés de 17 axiomes. Euh ces 17 axiumes, alors je vais pas m'attarder de je vais m'attarder sur celui-là, sur l'inverse et puis l'axium qui est là. Et et c'est là où où où en principe vous bondissez parce que vous voyez que l'inverse c'est une fonction qui va de R dans R. Donc on peut écrire 1/ 0, 3/ 0, x/ 0, enfin c'est c'est pas et c'est pas un problème parce que on a cet axiome qui dit que lorsqu'on va simplifier donc le la notation ici c'est pour 1/ R donc ça c'est 1/ R x R. Donc lorsqu'on va simplifier cette notation 1/ R x R pour dire que c'est égal à 1, on ne peut le faire uniquement que quand R est différent de 0. Donc en fait on on postpone on on retarde on retarde la les la fait le l'argument qui est que le dénominateur doit être non nul. On le retarde plus tard lors de la simplification. Et ça, ce que je disais ici sur euh plutôt que les types dépendants, donc ça ça existait déjà dans la librairie standard mais uniquement pour l'inverse parce que l'autre solution c'est quoi? Ben l'autre solution ce serait d'avoir ici un type qui serait pas R mais un type qui serait R à coller avec la preuve que R est non nul. Donc en fait si vous écrivez si vous écrivez 3 sur 2x, d'accord? Bah vous devez écrire 3 x l'inverse donc 2x avec la preuve que 2x est différent de 0. Et cette preuve là, cette preuve-là euh bah faut il faut l'avir. Donc ça veut dire soit vous avez un ax un lem intermédiaire comme quoi 2x est différent de 0 ou soit vous mettez le lambda terme directement lorsque vous écrivez ce trucl. Alors maintenant si je veux écrire 4 sur 5, d'accord? Bah, j'écris 4 fois l'inverse de 5 avec la preuve que 5 est différent 0 et cetera et cetera. C'est hyper pénible. C'est c'est vraiment quelque chose de de pas pratique quand quand on fait de la formalisation parce que on a on finit par avoir des des termes qui sont dépendants. C'est donc là ça dépend de la preuve et c'est pas vraiment waouh et c'est pas ce qu'on c'est pas ce qu'on souhaiterait. C'est pas ce qu'on souhaite pour vraiment pour des raisons commodité mais la correction est là. C'est-à-dire que c'est pas inconsistant de faire comme ça. Alors, c'est vrai que ça ça gêne au début, hein. Même même les gens qui sont pas forcément mat d'origine, ça gêne. Euh les étudiants s'en accommodent très bien parce que de toute façon, il voi très bien dans la pratique qu'au bout d'un moment et ben ils vont quand même devoir montrer que leur dénominateur, il est non nul, mais c'est juste retardé. l'axium d'ordre total dont je vous parlais tout à l'heure. Alors ça c'est des oou. Ça c'est des ou euh je vais pas m'attarder sur cette notation mais c'est des ou. Donc là, on sait décider si un réel est inférieur à un autre ou s'il est égal ou s'il est supérieur. Et donc du coup, ça donne un aspect vraiment classique à la librairie. Et l'axium de complétude aussi est un aspect classique pour des raisons pour des raisons internes à coque. Je ça je m'attarde pas non plus. La dérivée maintenant par exemple une fois qu'on a ces 17 axiomes, donc là ils sont pas les 17, il y a des points de suspension mais c'est c'est des axiomes de base tout à fait élémentaire. Il y a aussi l'axium d'Archimède, je l'ai pas mis là mais il y a l'Archimédia. Enfin voilà, c'est euh alors une fois qu'on a ces actions et ben on peut définir la dérivée. Alors la dérivée euh elle est définie sur un domaine. Alors vous voyez le le raisonnement en fait quand quand j'ai développé cette librairie. Alors déjà le le but c'était pas de développer la librairie. Je l'ai développé pour faire pour prouver autre chose parce qu'il y avait pas de réel d'enco à l'époque et euh et donc il y a j'avais pas vraiment fait une réflexion vraiment poussée sur cette librairie mais j'ai pas poussé la le fait de faire des fonctions totales au bout du raisonnement. C'est-à-dire je l'ai fait pour l'inverse parce que c'était pratique mais pour la dérivée je l'ai pas fait. Vous voyez pour la dérivée, la dérivée c'est elle est ici, elle retourne un type propositionnel, une proposition. Donc en fait, il faut lui donner f et d étant la dérivée de f sur le domaine. Donc sur le domaine. Et puis montrer que x donc la dérivée c'est la limite de f(x) - f(x0) divis par x - x0 quand x tend vers x0. Et donc du coup cette dérivée en x0, il faut bien vérifier que x0 appartient au domaine. Donc là on n'est pas on n'est pas dans une fonction totale. Donc le et la librairie Coclico, c'est ce qu'elle fait. Elle pousse le raisonnement. 15 ans plus tard, elle a poussé le raisonnement en disant et ben on quand on va écrire une dérivée ou une limite, on s'en fiche de savoir si c'est dérivable. On s'en fiche dans un premier temps de savoir si la limite existe et quand on fera des preuves dessus, au bout d'un moment, bah un jour quand même, faudra bien prouver qu'elle est dérivable et que et que la limite existe. Ouais. Tu as prononcé plusieurs fois le le mot fonction totale. Qu'est-ce que c'est? Alors, ben fonction totale, c'est ça. Fonction totale, c'est exactement ça. C'est-à-dire que c'est l'inverse d'une fonction partielle en quelque sorte. C'est-à-dire que c'est on n pas euh la fonction elle prend n'importe quelle valeur et puis elle rend des valeurs dans un autre ensemble. Il y a il y a pas de restriction sur le l'ensemble de départ des valeurs comme comme il y aurait ici. Plus de notion de domaine de définition. Il y a plus de notion de domaine de définition. C'est ça le domaine de définition, c'est tout R. Donc là, on peut c'est que c'est pour ça que je disais ouf qu'on peut écrire 3/ 0. 3/ 0 ça vaut n'importe quoi. Alors dans certaines bibliothèques 3/0 ça vaut 0 parce qu'on l' par exemple en en HOL Lite quand on le dénominateur est nul ça vaut zéro mais c'est pas faux non plus. Alors, depuis euh la refonte de qu'a fait Vincent Ceria en rock, ça vaut zéro aussi parce qu'il en avait besoin pour la partie constructive de poser que c'était euh que n'importe quoi sur zéro, ça faisait zéro parce que voilà. Mais euh donc il y a le le domaine de définition en fait, il est il est total euh de R vers R. Euh et donc du coup, on peut montrer par exemple, bah il y a aussi la continuité de la la dérivée et puis on peut montrer la dérivée de la la constante. Bah la dérivée de la constante euh donc ça c'est la définition d'une fonction constante, c'est-à-dire à x bah on associe un un un y qui n'est pas x qui n'est pas lié à x et puis la la fonction nulle à tout x on associe 0. Donc la la le la dérivée de la constante, c'est bien zéro. Ou la dérivée de la fonction identité à x, on associe x et ben c'est bien 1. La dérivée de x c'est bien 1 dans le domaine de définition et cetera et cetera. Donc une fois qu'on a qu'on a fait toute cette librairie, qu'on a développé tout ça, on peut montrer plein de choses. Par exemple, l'unicité de la limite. Donc si on a une suite, donc là on a pris l'exemple d'une suite qui prend donc c'est un entier naturel et qui renvoie un réel. Si la suite converge vers une limite L1 et qu'elle converge vers une limite L2, alors L1 = L2. Unicité de la limite. Et donc alors là, la preuve est coupée, c'est fait exprès. C'est pas parce que c'est juste pour montrer que la preuve est très très longue. Je vous la montrerai tout à l'heure en démo, mais euh ça c'est tiré. Alors, dans la bibliothèque standard, il y a pas de commentaire aussi jolis comme ça. C'est dommage d'ailleurs, ce serait ce serait quelque chose qui serait intéressant. Là, les commentaires sont faits pour les étudiants, sont faits pour les étudiants de L1. Et donc, on explique que bah comment on va montrer que L1 é= L2, bah c'est que il y a une la distance, elle est aussi petite qu'on veut entre L1 et L2. Ensuite, quand on on va unefolder la convergence, bah il y a les epsilon qui vont apparaître puisque la dérive puisque la limite c'est il est pour tout epsilon machin et cetera la valeur absolue de un - l est inférieure à epsilon. Voilà. Donc on va leur montrer ça. Donc il y a aussi des petites choses. Et là vous voyez on a des accertes. Je vous montrerai mieux tout à l'heure. Là on fait une preuve en avant en quelque sorte parce que on on a besoin à un moment où on est sur epsilon/ 2 et donc on suppose que epsilon/ 2 est positif sachant que epsilon est est positif et cetera. Enfin voilà, il y a des petites preuves comme ça. Bah justement, c'est l'heure de la démo. Alors euh sauf que je l'avais préparé tout à l'heure. Alors, je vais perdre un peu de temps parce que j'ai dû rebouter. Ouf! Alors euh donc on était sur la Alors, je vous montre rapidement le fichier. Donc ça c'est le fichier Air Limite qui est issu de la c'est celui qui est dans la dans la librairie standard. Donc il y a des il y a des choses alors c'est du calcul. Il y a marqué calculus mais c'est c'est pas vraiment du calcul. On ne calcule pas avec les réels avec les réels de de rock. On fait on fait pas de calcul, on fait des preuves. C'est donc il y a des il y a des résultats qui intermédiaires qui sont nécessaires. Euh il y a aussi alors qu'est-ce que je voulais vous montrer? Euh donc on se place sur un espace métrique. Donc on a la définition de ce qui a un espace métrique. Donc ça ressemble au coup hein. Je pense que dans dans ligne ils ont la même chose. Dans Bizar ils ont la même chose. Enfin il y a des choses un peu un peu partout dans light pareil enfin des choses comme ça. Et puis alors la limitation de cette bibliothèque là pour l'instant c'est que c'est des fonctions à un argument. On est dans air flash on n pas de fonction je vous parlerai après des des fonctions à plusieurs arguments. C'est en train d'être développé dans la partie analyse. Euh donc le lem donc on a du coup l'addition des limites. Donc si deux si deux fonctions si on a une fonction f ici qui a pour limite L, une fonction G qui a pour limite Est-ce que vous voyez mon curseur ou pas? Ouais. une une fonction G qui a pour limite L prime et ben la fonction F + G, elle a pour limite L + L' et cetera. Enfin voilà. Donc et puis ici euh la multiplication qui est beaucoup plus compliquée parce que la multiplication, il y a les domaines, il y a les domaines de de d'application qui se il y a pas mal de choses à faire, c'est de la composition. Euh bref, donc ça c'était juste pour que vous voyez à quoi ressemble ce genre de preuve. Et donc ça par rapport si je réponds à la question combien de temps ça a pris toute la partie limite définition 3 mois peut-être. Voilà 3 mois en 2000 maintenant ce serait plus rapide. Il y a des autres d'automatisation qui ont été développées. Donc 3 mois en l'an 2000 maintenant c'est beaucoup plus rapide. Oui. Est-ce que c'est ça interroge sur l'utilité de effectif d'utiliser ces outils? Bah le problème c'est que si on les utilise pas, ils vont pas se développer en fait. C'est alors comment dire Ouais. C'est-à-dire que c'est un peu comme les langages de programmation. Euh l'utilité c'est d'avoir des preuves vraiment correctes quand on quand quand on prouve des théorèmes qui soient un peu compliqués où on veut être sûr que la preuve est correcte. C'est très bien d'avoir ces outils. Et pour pouvoir utiliser et pour pouvoir prouver des lèmes un peu compliqués, ben on est obligé de partir des maths de base. Donc effectivement dans l'absolu, montrer l'unicité de la limite ne sert strictement à rien. Ça, je suis d'accord. Mais c'est un théorème qui est utile pour montrer plein d'autres théorèmes qui sont beaucoup plus compliqués et qui eux sont utiles. C'est c'est quand même les uns sur les autres. Oui, on on bien sûr travail de 3 mois, il a été fait, maintenant il est fait. C'est bon. Absolument. Tout à fait. Absolument. C'est c'est la c'est la base. C'est c'est la bibliothèque. C'est ce qu'on appelle les bibliothèques. Donc voilà, c'est Oui. Ouais. J'ai cru voir au tout début là que tu redémontrais que sur 2 + eps/ 2 est ég. Ouais. Il y a pas quelque chose qui a été fait sur les fractions que tu que tu peux tout de suite réutiliser ou alors c'est parce que c'est c'est le premier enfin. Alors le si le truc c'est que quand à l'époque de cette bibliothèque, il y avait juste rien vraiment rien. Maintenant maintenant on a plus besoin de faire un truc qui dit x/ 2 + x/ 2 = x. C'est fait par des tactiques du genre lou des ou field ou des des choses comme ça. Les tactiques que j'ai moi-même d'ailleurs développé après cette bibliothèque mais au fur et à mesure. Donc effectivement là il y a ça mais maintenant alors comme Coclico est plus moderne et en fait un des un des buts c'était aussi de moderniser cette bibliothèque. principe maintenant on utilise plus qu'occlico puisque c'est une couche plus moderne qui est basée sur celle-ci celle-ci est vraiment vieillote et et ancienne et sur le calcul de dérivée là le fait de transporter à chaque fois toujours la dérivée euh c'était dans un but particulier ou c'était dans le but bon ça permet d'avoir une une formalisation assez rapide et et puis on verra plus tard enfin ça ça permet d'avoir une formalisation assez rapide. Alors, ce qu'il faut savoir, c'est que de toute façon, l'outil ne va pas calculer la dérivée. C'est pas un outil de de calcul formel. Euh alors, il y a il y a des il y a des des liens entre on peut utiliser un outil calcul formel comme une comme une calculatrice et on va dire et puis après prou montrer le résultat du calcul formel. Donc c'est ce qu'on appelle l'approche un peu sceptique. C'est pas un peu, ça s'appelle l'approche sceptique. Donc on utilise un outil extérieur, on a le résultat et puis après on démontre dans rock ou autre chose que le résultat est correct. C'est mais là c'était vraiment quelque chose d'un peu rapide pour pouvoir parler de dérivées. Euh et dernière question, limite donc là je pense continuité, je pense éventuellement intégration aussi. Oui. Et c'est c'est aussi des choses qui ont été développées à l'époque. Oui. Oui. Alors le l'intégration ça l'a été pas par moi, ça a été par Olivier Desmettre euh 3 ou 4 ans après, mais c'est dans la même on va dire c'est la même époque. Voilà, c'est Et alors moi après je vais vous parler alors c'est l'intégral de Riman et moi je vais vous parler de l'intégral de Leb si j'ai le temps parce que là il y a quelques années on a fait l'intégral de Leb. On me dit qu'il faut que je me dépêche. Bien. Alors euh au niveau enseignement, je vous en avais parler hier euh quelques-uns. Euh ça c'est un fichier pour les secondes. Donc là c'est c'est quand même plus simple voire même les troisè puisque on parle de fonction et en particulier de fonction croissante. Ce que je voulais vous montrer c'était euh c'était ici. Voilà. c'était ici. Et donc là, on vient de définir qu'est-ce que c'est qu'une fonction croissante. Euh bah ça, je je vous répète pas ce que c'est qu'une fonction croissante, hein. Et puis après, on dit que on va montrer que alors on parle de fonction affine, définition des fonctions affines ax + b. et on leur ait dit que si a est positif, alors la fonction est strictement croissante. Et donc on leur fait des exemples. Par exemple, si a est égal à 0, alors il s'agit d'une constante. Donc on leur explique donc ça c'est donné dans le fichier avec des tas de commentaires qui peuvent lire et qui avec les tactiques qui vont bien pour faire leur preuve. Et après c'est à eux de faire la preuve. tout seul sur la fonction croissante. Et ça même en troisème, ça marche plutôt bien euh avec tout avec toutes les explications. Alors la seule contrainte qu'on a c'est qu'il faut qu'il sache lire enfin qu'il sache lire qui qui comment dire qu' il faut qu'il soit il faut qu'il soit motivé pour lire tout le fichier et bien le comprendre. C'est c'est ça que je voulais dire par ça. C'est euh et donc la suite la ce que je vous ce que je vous aiffiché dans le slide tout à l'heure, c'était cela et ça c'est pareil. Donc là, tous les commentaires, les jolis commentaires qui sont très utiles, ils sont c'est à destination d'étudiants de première année d'université, d'étudiants de L1 où ils commencent à faire de l'analyse euh et donc là c'est pareil, on leur donne une première, on leur donne cette fonction là où tout est donné, ils l'ont pas à faire donc il faut qu'ils lisent bien les commentaires. Et alors vous voyez, il y a il y a pas mal de textes parce que on est limité en nombre d'heures. On a très peu d'heures. Du coup, il y a pas de cours magistral, il y a pas tout ça. Les preuves en math, en principe, ils savent les faire côté côté math, mais en principe. Pour ça, je dis en principe. Et nous après, on leur on leur explique ici. Donc eux, c'est pareil, il faut qu'il sach il faut qu'ils lisent aussi euh toutes les explications qui sont là qui sont à la fois lié lié au math et lié à à aux tactiques elles-mêmes de l'outil. Et donc ce que ce qui est important, ce que je voulais vous faire remarquer ici, c'est ça, c'est au bout d'un moment quand ils savent quand on a fait plein de choses avant sur les antinaturels, sur les ensembles, sur la logique, sur parce que l'analyse ça arrive à la fin en fait. L'analyse c'est vraiment le c'est vraiment la fin parce que c'est ce qu'il y a de plus compliqué en fait pour eux. Et ben on va pas, on en a marre de reprouver que de est différent de zéro. aucun intérêt et donc on leur dit quand même il y a de l'automatisation et donc euh on peut utiliser des la tactique LRA qui est une tactique automatique qui a ring, il y a field qui sont des tactiques automatiques qui font des tas de choses automatiquement et et donc suivant le niveau auquel on se place et ben donc tout au début il y a rien d'automatique parce qu'on veut qu'ils comprennent bien comment fonctionnent les maths et c'est intéressant pour eux ils n'ont pas idée que quand on écrit 4/ sur 5 et ben il faut que bah le prouveur il faut que 5 il soit différent de zéro. Voilà. Et donc ça il y a des il y a des choses et ça leur permet de de bien voir que bah les maths ça va jusque il faut tout montrer jusqu'en bas quoi. Jusqu'en bas et donc voilà. Donc mais au bout d'un moment il y en a marre. Donc au bout d'un moment quand même dans la vraie vie, nous en tant que chercheur bah de toute façon on utilise beaucoup les tactiques automatiques parce que notre but c'est de prouver des théorèmes un peu compliqué et pas de prouver que 5 est différent de zéro. Voilà. Euh alors euh voilà et puis après bah du coup ils peuvent ils peuvent faire la même chose. Enfin ils ont ils ont plein de lem plein de lem à faire. Euh où est-ce que c'était? Si je reviens ici. Hm. H euh oui. Alors ce que je disais par rapport à l'axiomatisation euh là il y a 17 axiomes. Les 17 axiomes en fait il y a il y a pas d'incohérence. Alors comment est-ce qu'on est sûr qu'il y a pas d'incohérence? Bah déjà il il y a une preuve de non. Alors la le premier axium de complétude que j'ai que j'ai fait, il était faux parce que j'avais oublié de dire que l'ensemble était était non vide. Donc déjà voilà donc c'est pour ça que il y a des tas d'anecdotes comme ça sur des axiom faux et et pas seulement quand on est jeune doctorant hein. Il y a il y a des gens très bien en particulier Gillek par exemple m'avait raconté que quand il était allé à la NASA travailler en PVS avec César Munos, il il faisait des preuves sur des des preuves d'avionique sur des des leur but donc c'était en 2000 et leur but c'était en 2015 de faire atterrir deux avions tout seul sur la même piste avec un programme prouvé correct. Bon, de ils avaient ils s'était donné 15 ans pour faire ça. On n'y est pas tout à fait encore. Donc euh voilà, tout ça pour dire que c'est long parce qu'en fait on on se dit "Ah bah il y a plus que ça à prouver mais le il y a plus que ça." Waouh! Voilà, parfois il peut être compliqué. Bref, et donc il il disait euh ils avaient besoin justement du théorème des valeurs intermédiaires et donc il avait posé en axiome. Ils sont dit au moins quand même c'est un un lim trivial. Donc la notion de trivial est très subjective en fait. Et donc quand ils ont posé l'axiom, il y a l'intervalle AB et ben un mathématicien et je suis sûr que vous dans votre tête AB a A il est plus petit que B hein. Sauf que si vous lui si vous l'écrivez pas et ben la donc la tactique grind et ground c'est le même nom tactique en j'ai découvert que c'était le même nom tactique en ligne. Donc ligne peut-être que c'est inspiré de PVS, je sais pas. Euh c'est des tactiques automatiques et ben du coup il il arrivait à tout prouver et donc ils se sont dit quand même quand même quand même il y a un truc qui va pas et donc ils ont relu leur axium et donc ils avaient oublié de préciser que quand on parle de intervalle à B et ben A il faut qu'il soit plus petit que B. Et donc effectivement quand ils ont rajouté cette hypothèse et ben voilà c'était plus raisonnable déjà. Donc euh poser des axiomes, c'est vraiment là les axiomes sont tellement triviaux, mis à part la complétude sont tellement triviaux que et puis euh depuis 20 ans qu'elle est utilisée cette librairie, on sait qu'on peut pas prouver le faux mais euh voilà, il faut faire faut faire très attention. J'avais euh un autre collègue euh Jean-Louis Criville là qui qui me disait "Ah ouais, mais non, mais ça sert à rien." C'est un peu la remarque de Pascal tout à l'heure, à quoi ça sert? Euh de on pourrait on pourrait poser tous ces axiomes triviaux, tous ces axiomes, bah le la limite, l'unicité de la limite, tout ça, on pourrait l'axiomatiser, on pourrait le poser en axiom puisque de toute façon c'est tellement trivial. Et et je lui avais répondu ça, je leur avais dit "Non, mais on peut quand même se tromper." et il m'avait dit "Ah mais c'est pas de ma faute si les gens sont nuls." Mais non, en fait même enfin même quand les gens sont pas nuls, on peut quand même parce qu' on suppose l'être humain suppose quand même qu'il y a des choses qu'il y a des que la machine ne suppose pas quand même. Euh alors euh on parle un petit peu recherche euh maintenant, ça va pas durer trop longtemps. Donc comme on l'a dit hier, il y a plusieurs prouveurs, il y a aussi plusieurs bibliothèques et il y a plusieurs bibliothèques même dans un même prouveur. Parce que hier Sébastien, il a il a il a cité Matcomp et Macomp Analysis. Euh nous on en développe depuis 20 ans, enfin pas depuis 20 ans mais elle s'appelle pas comme ça depuis 20 ans, mais on en développe une autre qui est Rock Numanalysis qui est dédié à l'analyse numérique. Pas que l'analyse, l'analyse numérique. Euh donc c'est des travaux qui ont commencé en 2005 par des projets ANR sur l'équation des ondes. Alors, il s'avère pour la petite histoire que François Clément, alors François Clément et Vincent Martin, c'est des numériciens, donc c'est des mathux, des vrais maths, des mathux de qui font des maths, enfin des des vrais maths, euh des numériciens. Et euh donc François François Clément, j'étais allé le voir au début de ma thèse parce que moi je voulais faire une thèse sur l'analyse numérique dans les enfin prouver des problèmes d'analyse numérique. Et donc il m'avait soumis ce problème d'équation des ondes en 97 et sauf qu'il y avait même pas de réel et donc il m'avait et donc j'avais regardé je et donc du coup ce problème qui m'avait soumis en 97, il a été prouvé en 2012. Donc j'ai fait ma thèse sur la différenciation automatique, donc avec des réels et des outils de différenciation automatique, ce qui était un petit peu plus abordable à l'époque, mais parler de gradient, parler d'intégral, l'équation parler de dérivées partielle alors qu'il y a même pas de réel. C'était juste c'était juste pas possible. Donc ça c'est pour la petite histoire. et Sylvie Bol donc qui elle fait du rock et est en particulier elle est spécialiste des flottants aussi pas des réels, enfin des flottants. Moi moi c'est les réels, c'est les flottants. C'est on fait bien la différence. Euh et Vincent Martin qui est arrivé dans le projet après vers euh vers 2012-23, lui il est en particulier spécialiste des éléments finis. Et donc c'est les éléments finis dont je vais vous parler un tout petit peu maintenant. Et avec les donc Catherine Lelait avec Guillaume Il Kion et Sylvie Boldau est à l'origine de la bibliothèque Coclico. Florian Fessol a prouvé le le théorème de l'Axmilgram. Alors, il a pas fait que la preuve du théorème de l'Axmilgram et de CA. Il y a Laxmilgram et CA. il a pas fait que cette preuve pendant sa thèse. Il a fait d'autres choses sur les flottants mais ça lui a quand même pris une bonne partie de sa thèse. Donc et puis Udamousin qui a euh fait la preuve de d'unisolvance euh pour les éléments finis simplifiaux simpliciaux euh de éléments finis de la grange en particulier euh P1. Donc euh et elle ça a pris toute sa thèse de définir euh c'est quoi un élément fini, d'appliquer l'élément fini de la grange et avec la preuve d'unevance qui va bien. Donc ça vous donne un peu un ordre de Alors, elle l'a pas fait toute seule en plus on l'a beaucoup aidé. Donc euh c'est en temps euh en temps humain, c'est pas c'est c'est assez important. Euh alors comment est focus sur la forus de formalisation? Comment est-ce qu'on formalise? Comme je disais tout à l'heure, il faut connaître les preuves. Donc on pour ça, pour connaître les preuves, on utilise des livres, des livres de math. Donc ça c'est les livres qu'on a qu'on a utilisé. Alors euh voilà, il y en a peut-être d'autres mais on a utilisé ça. Par contre, pas que pas que parce que dans les livre de math quand vous faites des preuves papier crayon en math, vous écrivez euh je d'après l'hypothèse machin, on a ça. Donc autre chose, le donc là le donc il peut être cher le donc. Et donc et donc le donc et ben il faut il faut comber les sauts de ces donc d'où par le théorème machin on en déduit que wou. Donc donc ça ça c'est quelque chose où il faut combler les sauts et puis il faut aussi mettre en place les choix de formalisation. Donc je vous en ai parlé pour les réels mais par exemple il y a il y a je vais en parler tout à l'heure il y a plein d'autres choix de formalisation. Mais pour ça, Vincent et François, donc Vincent Martin et François Clément, ils ont refait ils ont complètement refait des preuves mais vraiment détaillées pour combler les sauts des preuves mathématiques que l'on trouve dans les bouquins. Je vais vous en montrer un petit extrait. Euh alors, je l'avais préparé tout à l'heure comme Alors, voilà. H Alors, pour que vous en ayez un aperçu, alors c'est un document qui est en en travail, c'est pour ça que les parties vertes puis il y a des annotations dessus, mais c'est pas très grave. Hm. H par exemple, voilà, par exemple là, typique Non, ça ça c'est un peu trop euh donc pour les éléments finis de la grange. Alors, les éléments finis la range. Je sais pas si vous en faites beaucoup. Si vous faites, je sais pas si c'est au programme, c'est pas c'est pas au programme zéro. Euh, c'est pas grave, c'est c'est pas gênant. Et et je et et je répondrai du coup à la question aussi en même temps. Ah, c'est oui. Euh, c'est pas ce que je voulais faire. Bon euh je répondrai aussi à la question de comment on traduit les schémas. Il y avait une question hier qui disait "Mais les schémas comment on les traduit?" Et ben les schémas, on les traduit bah tout là, toute la suite qui est ici, ça en fait ça c'est pour l'être humain, c'est pour nous euh et en particulier nous qui devons Alors, maintenant François Clément, il fait plein de preuves, il c'est devenu euh vraiment il fait plein plein de preuves. Mais au départ, il y avait que Sylvie et moi qui faisions des preuves et donc euh il fallait qu'on comprenne aussi leur preuves détaillées. Alors, c'est pas qu'on est spécialement nul en math, mais mais bon voilà, il faut fallait quand même qu'on et et donc ces schémas, ils sont aussi là pour que nous on comprenne bien ce qu'on veut. Euh c'est quoi les théorèmes, à quoi il s'appliquent et donc la formalisation, elle est vraiment là euh par exemple. Voilà, donc on a on a ce genre de preuve détaillée. Euh vous voyez ça bah bon ça typiquement c'est des binomiaux mais tous les détails sont là. euh avec euh à chaque fois la l'épreuve comment on applique en math. Vous écrivez jamais des choses comme ça. Vous vous faites pas autant de autant de détails. Et donc ce rapport il explique vraiment en détail absolument toutes les étapes de programmation qui nous permet nous de de faire de de faire du coque. Hm. Alors, c'est ces preuves, ça donne ça donne vraiment une autre perspective sur les maths. Euh et et ça ça ce ce trans ce ce cette diapo là, elle vient elle vient des mateux en l'occurrence. C'est c'est les Mateux qui qui ont qui ont remarqué ça. C'est-à-dire que les formulations sont un peu inhabituelles et sont originales par rapport à ce que vous avez souvent l'habitude de faire papier crayon. En pratique, il faut choisir les bons chemins de formalisation en s'appuyant sur des choses formalisées. Comme on a dit tout à l'heure, une fois que les bibliothèques sont faites, et ben elles sont faites. Après, on peut on peut y retoucher ou on peut y revenir quand en ligne par exemple, ils sont passés de de mat 3, enfin de ligne 3 à ligne 4, ils ont ils sont fait derrière moi table race du passé, ils ont tout refait en ligne 4. C'est voilà. Alors nous en rock, on a depuis 30 ans, on n pas pris ce cheminlà. C'est-à-dire qu'on essaie d'être conservatif, on essaie d'avoir une compatibilité ascendante. C'est un choix, il est bon ou mauvais hein, ça je je préjuge pas. Line, ils font l'autre choix inverse. Je voilà, j'ai pas d'avis sur cette question à vrai dire. H et euh alors c'est quand même pratique d'avoir une compatibilité ascendante quand on change de version hein. Mais voilà euh essayer de généraliser les résultats. Alors généraliser les résultats, par exemple quand on parle d'avoir une hiérarchie, on parle de de groupe de monoïdes, de d'anneaux et cetera. Donc ça c'est une sorte de généralisation. Quand on fait des matrices et ben on essaie de pas faire juste faire les matrices. Euh quand j'ai montré les dérivées, c'était dérivé d'une fonction à une variable. C'est pas très général, c'est pas c'est pas voilà. Donc on essaie de généraliser en y concrant un effort raisonnable parce que parfois la généralisation ça demande beaucoup d'efforts et c'est pas seulement euh qu'il y a que ça demande beaucoup d'efforts, c'est qu'ussi dépend ce qu'on veut. Par exemple, je parlais d'une autre librairie de Matcomp. Typiquement, eux, ils sont très générals, ils sont très méta pour les pour l'enseignement c'est inutilisable parce que les notions sont beaucoup trop méta, c'est pas du tout accessible aux étudiants et du coup si on veut aussi pouvoir utiliser cette bibliothèque à la fois pour les étudiants et à la fois pour pour des gens qui sont pas du domaine, en particulier nos les numériciens, ils veulent pouvoir accéder quand même la comprendre relativement facilement la bibliothèque et donc c'est un choix à faire. C'est pour ça que nous on continue à développer cette bibliothèque qui qui est vraiment utile au numéricien et à l'enseignement et là je la compare à Matompe qui où ça c'est elle est c'est pas possible. Donc c'est c'est ça les choix. Line, je sais pas trop de ce point de vue là au niveau généralisation, ça je sais pas où ils en sont. Alors, les éléments finis, quelques quelques rappel, bah c'est ça les éléments finis, c'est-à-dire on veut trianguler ou quadranguler une surface ou un volume et puis pour pouvoir faire des calculs sur chaque petit triangle. Euh donc là, c'est un anévisme cérébral pour voir ce qui se passe au niveau sanguin. Et puis notre objectif à terme, c'est de démontrer euh un code de méthode d'éléments finis écrit en C++ dans Rock. Mais pour pouvoir démontrer ce code, et ben il nous faut toute une librairie qui va nous permettre euh de d'avoir tous les théorèmes qu'il nous faut. Et donc et voilà les manes nécessaires. Donc les méaires bah il y a l'axe migram. Alors l'axe migram on l'a. Les espaces de Sobolf on les a pas encore. L'intégral de l'obeg l'intégral de l'obeg on l'a mais ça fait pas longtemps. Ça fait 2 ans. Les distributions, pas complètement. L'élément fini, on a que l'élément fini. Euh les simplexes, on a pas on n pas les quadrangles. Euh et ça, on l'a pas du tout. Donc voilà, il manque il manque tout un tas de choses. On est construit au-dessus de la librairie Coclico. Donc ce qui est en noir c'est Coclico. Et donc on a quand même rajouté tout ce genre de choses déjà sur les morphismes, les fonctions abéliennes, les monoïdes abéliens, les enfin les les modules space, enfin les les choses comme ça. Euh et puis donc ça c'est là où on en est. Donc on est parti en 2000 de juste 17 axium. D'accord. la librairie coclico un peu qui augmente. Floc, c'est des flottants parce qu'en fait quand on fait de la preuve de programme, on fait aussi, c'est ce qu'on a fait sur l'équation des ondes, on a prouvé la correction du schéma numérique. Donc l'équation des ondes, on approxime sur un maillage sur un schéma un schéma numérique mais aussi l'erreur de flottant puisqu'on on travaille avec un un les numériciens travaillent avec des des ordinateurs. ces schémas numériques, ils sont calculés avec des programmes sur ordinateur. Les numériciens, ils font pas que des preuves papier crayon et et souvent ils ont pas forcément conscience ou quand ils en ont, ils savent pas trop comment faire, bah de qu'ils ont aussi des erreurs de flottant. Donc on a on prouve à la fois l'erreur de méthode et à la fois l'erreur de flottant. Et donc on a des subsets de l'algèbre. Donc ça euh c'est ce qui a été euh développé dernièrement avec les éléments finis simpliciaux. Euh l'intégrale de Leb, on l' on l'a fait avant mais vous voyez c'est récent 22 2022 2023, j'ai bientôt fini. Euh l'axe 1000 g 2017 et ce qui est en bleu, c'est le futur. Donc il nous reste encore pas mal du travail. les les cuboïdes, les espaces de Sobolf, les formules de quadrature. Là, on a un élément fini. Un élément fini, c'est-à-dire un triangle ou un ou une ou un bref un triangle en trois dimensions. Un oui, un simplexe. Voilà, c'est ça. Euh et puis à la fin, le programme vérification. Mais là, on en a encore pour peut-être pas 20 ans, mais enfin je sais, je sais pas, je je je m'avance plus maintenant. Je Voilà. Alors vous, il y a il y a quelques publications en particulier cette publication à Camoa. Camoa, c'est un journal de math. Donc euh ça c'est une publication qui est accessible aux Mateux pour le coup parce qu'elle est orientée pour les Mattheux. Donc euh et c'est donc ça c'est sur l'équation des ondes, c'est pas sur les éléments finis. Euh là on a une publication soumise mais on va en faire une sur les éléments finis accessibles au Mattheux une fois qu'on aura fini l'autre. H alors je peux je peux vous montrer, c'est le dernier truc que je voulais vous montrer, c'est euh à quoi à quoi ça ressemble à quoi ressemblent les théorèmes. Euh voilà. Donc par exemple, donc l'article il fait 79 pages et donc vous avez par exemple ici quelques dans l'article, vous voyez, vous avez l'épreuve de math et puis les définitions en rock qui correspondent. Et puis vous pouvez cliquer ici sur le guide où il y a le où il y a le théorème. Donc avec les avec les schémas. Donc ça ressemble à ça. Donc pour répondre encore à la question comment on formalise les schémas? Ben les schémas on les formalise comme ça ici. Et puis après on définit on définit alors MAPF c'est une fonction MAP sur les sur les familles de fonctions. Donc là on parle de famille de fonction. Euh là on est dans RD hein, on n'est plus dans R. Donc on n'est pas seulement dans R2 ou dans R3, on est dans R puissance D. Euh donc là c'est toutes les les différents éléments finis. Donc c'est on est que du la Grange mais donc ça c'est du P1, P2, P3 et cetera. Enfin bref, voilà. Donc c'est et donc ah oui et le le l'élément fini, la définition, elle est quelque part par là. Enfin bref, c'est pas très important mais euh et donc vous avez le la élément finis, vous avez un élément fini de référence qui est un élément qui a un triangle de dimension 1, un triangle rectangle et puis vous avez une transformation géométrique qui le transforme enfin et inversement euh sur l'élément fini quelconque du maillage. Donc c'est tout ça qu'il faut qu'il faut formaliser. Et voilà. Donc on on en est là. Merci. Est-ce qu'il y a quelques questions rapidement? Ouais. Vous avez évoqué le fait qu'il y avait pas de calcul sur les réels en rock et j'ai pas compris c'était une limitation de rock ou simplement qui manquait de bibliothèque. Non. Alors, quand je dis qu'il y a pas de calcul, j'exagère un peu parce que il y a des calculs sur les sur tout ce qui est entier. Euh par exemple 3 + 4, en fait, ça aussi ça a évolué. C'est-à-dire que au départ 3 c'était 1 + 1 + 1. Le 1 étant le 1 de type R. Donc là, il y avait juste pas de calcul. Maintenant 3, c'est l'entier 3 qui est injecté dans les réels qui est de type R. Donc en fait quand on fait 3 + 4, c'est les entiers de péano et ça fait successeur de successeur, ça fait 7 et après 7, il est de type R. Euh c'est disons que les preuves vous pouvez pas écrire tout est défini en terme de l'M. Donc si vous définissez pi, vous pouvez définir pi en utilisant la formule de sterling ou ou le cosinus ou je sais pas quoi. Mais mais ça va pas ça va être la preuve que c'est pi, mais ça va pas être pi. Vous pourrez pas dire pi 3 14. Et quand par exemple si vous faites 3/2 + 1/2, ben c'est 3/ 2 + 1/ 2 et la preuve de ça et ben on réduit au même dénominateur et puis ça fait 3 + 1/ 2 et puis ça fait 3 + 1 4/ 2. Après on peut simplifier, ça fait 2. pouvez imaginer euh calculer ça ou ou c'est pour alors euh non alors je me demande euh s'il y a pas des bibliothèques par exemple typiquement les bibliothèques de Alberto Safaglion ou des des gens comme ça qui définissent les réels par coinduction, ils peuvent faire un peu de calcul. Donc c'est pas que c'est impossible, c'est que nous pour ce qu'on fait ça nous intéresse pas spécialement parce qu'on veut vraiment des preuves. Mais je sais pas comment c'est les réels de lig et ce qu'ils font du calcul. Alors il y a des notations. C'est des suites d'équivalent euh des classes d'équivalent de suite de cochonnelle et euh d'accord le noyau n' aucune idée de à quoi ça ressemble et c'est juste des démonstrations exactement comme ça. Exactement. Moi, j'imaginais par exemple l'exemple du epsil eps/ 2 + eps/ 2 é= epsil peut-être pouvoir le montrer. Alors ça il y a des tactiques automatiques qui le font. Oui mais disons sur bon simple mais disons si on a un calcul je sais pas de de 10 lignes alors ça alors mais ça dépend le calcul formel pouvez le faire. Oui si ça dépend ce qu'on appelle calcul. Par exemple, si vous si vous avez un truc qui dit euh 3x + 7y + 8 = euh 3 facteur de x euh plus euh je je vais dire un truc complètement bon, je j'essaie d'écrire un truc vrai mais c'est l'exemple est stupide mais ce que je veux dire c'est que ça mais ça ça c'est pas si c'est quand même pas si simple. Enfin, c'est pas ça. Vous il y a il y a une tactique field qui fait ça oura fait ça aussi. Alors ça ça va vous générer la preuve que 3 doit être différent de zéro puisque là vous avez vous allez devoir simplifier par 3 et cetera. Ça c'est pareil, c'est déduit automatiquement. Mais vous les énormes formules que Benjamin, je crois il y a Benjamin qui a sur le théorème des quatre couleurs, il a il a euh je sais plus qui a montré des trucs énormes. C'était toi. Voilà. Il si jamais c'était sur R et des choses comme ça, ça fil de fil des rings montre ce genre de chos. Mais c'est pas Je sais pas si on appelle ça du calcul. Pour moi, c'est pas du calcul. Pour moi, c'est de la preuve. En fait, moi c'est surtout par rapport à la comparaison avec un logiciel de calcul formel. Enfin moi j'ai mais le calcul formel il fait pas non plus rentrer dans une discussion trop longue s'il vous plaît. C'est ça. C'est pas du c'est pas non plus de c'est la définition de c'est quoi un calcul pour moi pour moi un calcul c'est euh c'est je sais pas c'est c'est pi + 3 ça fait et encore enfin c'est ça fait 6 vir quelque chose. Voilà, c'est mais ça mais c'est vrai que c'est la définition. Benjamin hier, il a dit les réductions, il a appelé ça du calcul. Est-ce que une betta réduction c'est un calcul? C'est voilà, c'est la vraie question. Bon, on peut utiliser le calcul de cop de l'autométalisation du calcul symbolique. C'est ce que fait ces chosesl donc ce que fait ce que fait MAPle et tout ça, enfin ce que font les outils calcul formel, c'est ce qu'on appelle les tactiques d'automatisation et ça on le fait. les questions là parce que on discuter un de la pause. Raisonable.