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

Euh d'abord, merci beaucoup pour l'invitation. Je suis très content d'être ici et de parler dans ce cadre. Donc moi, j'ai un background un peu différent euh des de Mikael et Benjamin parce que moi, je suis vraiment mathématicien. J'ai fait j'ai fait une test de math, j'ai plein de papiers de maths. Je suis vraiment amateux et puis je suis tombé dans les assistants de preuve un peu par hasard parce que bah en tant que mathématicien, on réfère des papiers. J'avais l'impression de référer de plus en plus de papiers soit un peu faux soit beaucoup faux. Et j'étais un peu frustré par par cet état de fait mais cet état de fait, on peut même pas tellement le reprocher au mathématicien. C'est c'est le système qui est comme ça. Il y a un système de publish or pich où il faut publier beaucoup de papiers et à la limite le fait qu'il soit juste et secondaire pour se construire une carrière. Et ça m'emballait pas particulièrement comme principe. Et donc j'avais entendu parler des assistants de preuve. Donc, je me suis demandé si les assistant si les assistant de preuve avaient un espoir d'être un jour une partie de la solution à ce problème. Si si chacun avant de soumettre un papier devait le vérifier dans un assistant de preuve et ben au moins ce problème des papiers faux serait partiellement résolu. Et puis même quand on parle pas de papier faux, il y a souvent des papiers disons avec des définitions qui sont pas parfaitement précises. Non pas parce que l'auteur est pas soigneux, mais parce que il a dans la tête certaines hypothèses et toutes les personnes de sa communauté savent que quand on écrit ce type de théorème, il y a ces hypothèses qui vont être là et comme elles sont dans la tête de tout le monde, c'est pas la peine de les écrire sur le papier. Et un pauvre doctorant qui arrive 10 ans plus tard et qui est pas exactement dans la communauté, il va lire le papier et il va pas savoir qu'il y a ces hypothèses qui sont là mais qui sont pas écrites. Et s'il a pas un directeur de thèse qui est au fait de ça et qui qui lui dit attention et bah peut-être qu'il va appliquer ce théorème dans un autre contexte. Justement l'hypothèse implicite ne sera pas satisfaite. Et euh et c'est assez dangereux. Même si tout le monde est de bonne foi, même si tout le monde fait des efforts, même si tout le monde essaie de bien travailler, c'est pas facile de construire un corpus, un grand corpus mathématique cohérent sans avoir de garde de fou. Et pour moi, les assistants de preuve pouvaient peut-être jouer un petit peu ce rôle aussi. Donc j'ai commencé à jouer avec, j'ai commencé à formaliser certains de mes papiers, certains papiers d'autres personnes aussi. J'ai trouvé des erreurs dans les papiers d'autres personnes. J'ai trouvé des erreurs dans mes papiers aussi, il faut être honnête. Euh et donc je continue à faire les deux. Je continue à faire de la recherche traditionnelle en math et en parallèle de ça euh je formalise des maths dans une bibliothèque en ligne qui s'appelle mat lib. Alors pourquoi LG? Il y a pas tellement de raison parce que lig et rock comme on vous a raconté c'est essentiellement des systèmes qui sont construits sur les mêmes bases avec de la théorie des types derrière. Et comme je suis un mathématicien, un praticien, en fait, je sais même pas vraiment comment ça fonctionne. Et euh une bonne nouvelle, c'est qu'il y a pas vraiment besoin de savoir comment ça fonctionne pour se servir de ces outils parce que les informaticiens sont très forts et donc ils ont construit des outils. B quand vous fait tourner Windows, vous avez pas besoin de savoir comment Windows ou Linux ou Mac, pas de chapelle, vous avez pas besoin de savoir comment ça fonctionne en dessous. Et ben les assistants de preuve euh aujourd'hui sont suffisamment bien faits que euh en fait il y a pas besoin de savoir toutes les arcanes qui y a en dessous. Et même si en jouant avec j'ai appris un certain nombre de choses. Euh aujourd'hui, je vais faire le naïf. Mais donc je vais je vais essayer de vous présenter Line comme un mathématicien praticien en vous disant regardez voilà en pratique comment ça marche et pas pourquoi ou quel est le mon point de vue juste je vais vous décrire les choses donc ça va être un peu impressionniste. Je vais à la à la fin de cette heure d'exposé, vous vous saurez pas installer ligne, vous saurez pas faire une démonstration avec. Mais je mon but c'est que vous ayez une idée de à quoi ça pourrait ressembler si vous aviez envie d'y passer un petit peu plus de temps ou si vous aviez envie d'encourager certains de vos élèves à regarder aussi parce que je pense que c'est des choses qui sont tout à fait accessibles. Bah des élèves de prépa aujourd'hui. Euh et donc je vais euh je vais faire un truc un peu absurde. Je vais pas vous raconter une preuve facile. Je vais vous raconter une preuve intéressante qui qui met en jeu des maths relativement avancés mais accessible niveau prépa. Et donc je vais vous la montrer dans ligne mais avant je vais vous la faire au tableau. Donc j'ai aussi pensé à ceux qui sont venus ici en espérant faire des maths et qui ont peut-être l'impression d'être dans un tracnard. Donc voilà les 20 minutes qui viennent, elles sont pour vous. Il y a pas de vidéo projecteur, il y a rien. Il va y avoir des définitions, des théorèmes, des bouts de démonstration. Euh comme toujours, vous m'arrêtez, vous me posez plein de questions. Euh c'est quand même le but principal. Donc le théorème que je vais vous raconter, c'est un théorème sur des applications de R2 que je vais appeler des semi-contractions. Je vais dire que F alors R2, c'est pas important. Vous pourriez prendre votre espace vectoriel, voir votre espace métrique favori. Donc je vais je vais dire que F est une semi-contraction. Ah oui, j'ai un gros défaut. Euh, je suis chercheur au CNRS et c'est une bonne nouvelle pour mes étudiants que j'enseigne pas beaucoup, j'écris très mal. D'accord. Donc, il faut pas essayer de lire ce que j'écris. C'est juste un support. Il faut écouter ce que je dis. C'est quoi la bonne nouvelle pour tes éurs? C'est que j'en ai pas. Ah oui, d'accord. Je tê pas sûr. C'est ça. Euh c'est une semi-contraction si elle ne dilate pas les distances. Donc si vous préférez elle est un lipsitienne. Si euh pour tout xy la distance de f(x) à fite au sens large que la distance de x à Y. C'est pour ça que c'est une semi-contraction et pas une contraction. Si c'est une contraction forte, on sait exactement ce que ça ferait. ça aurait un point fixe et ça tirait tout le monde exponentiellement vite vers ce point fixe. Quand on met une unité large ici euh ça ouvre tout de suite un petit peu plus la classe d'application. Euh les premiers exemples auquels on peut penser bah c'est les contractions strictes. Comme je vous je vous ai dit, on tend vers un point. Mais l'autre exemple de base, c'est les translations. Les translations, ça rentre dans cette classe là. Et le théorème que je vais vous écrire dit que en fait ça a tendance à ressembler à des translations. Moi je fais des systèmes dynamiques. Donc j'ai envie de prendre F, j'ai envie de l'itérer, j'ai envie de me demander qu'est-ce qui se passe quand j'ai itéré beaucoup de fois. Et donc il y a un théorème de Colberg et Nemman. Colberg et Nemman de 1983 qui dit que ça se comporte comme une translation. Il existe un vecteur V tel que pour tout X, j'itère fn x fn x, je divise par n et ça converge vers v. Autrement dit, OK, peut-être que localement ça transfte pas, mais il y a une sorte de vecteur de translation asymptotique. Autant n ça se comporte en gros comme x + nv à un facteur négligeable par rapport à n près. Alors, il y a quelque chose de bizarre dans cette énoncé, c'est la date 1983. C'est quand même relativement tard pour un énoncé qui est complètement élémentaire comme ça et que les gens auraient pu démontrer un siècle avant. Euh je pense qu'il y a plusieurs raisons à ça. Une des premières raisons, c'est que il faut se poser la question, hein. Une deuxième raison, euh c'est que c'est pas évident d'envisager que ça puisse être vrai parce que euh ces hypothèses sont quand même extrêmement faibles. et se dire que les hypothes extrêmement faibles comme ça vont quand même contraindre la classe des applications pour avoir un théorème comme ça, c'est pas du tout évident. Souvent, c'est plus dur de trouver le bon théorème que de le démontrer. Et ça, c'est un exemple. Et je pense que la troisième raison, c'est qu'en fait c'est pas un théorème facile. C'est c'est pas un théorème dur, c'est un théorème astucieux. Si vous essayez de vous dire "OK, une semi-contraction vous décrivez localement, vous essayez de voir un petit peu, vous essayez de démontrer, vous vous allez pas y arriver. Il faut une idée un peu astucieuse pour pour ce trucl-là. Euh je connais plusieurs preuves dans la littérature et celle que je vais vous raconter maintenant qui est dû à Carlson au début des années 2000, je trouve elle est elle est très jolie. Donc c'est aussi pour ça que j'avais envie de vous la raconter aujourd'hui. Donc démonstration de Carlson disons dans les années 2000. Question. Oui, distance. Oui, c'est c'est euclidienne. Euclidienne. Euclidienne, c'est très important. D'accord. R2 Euclidien, c'est faux avec la norme du supe. Euh donc la démonstration de Carlson, elle va utiliser la sous-additivité. Donc le point, l'objet central si vous voulez, ça va être un qui va alors une première remarque, c'est qu' si je prends deux points x et y, je regarde fn x et fn y, il reste à distance borné par la distance de x à y. Donc si je sais démontrer cette convergence là pour un point x, je l'obtiens pour n'importe quel autre point x parce que la différence entre fn x et fn y reste borné. Donc je vais juste le démontrer pour x = 0, juste pour me simplifier la vie. Et si je prends x = 0, le l'objet que je vais essayer de regarder, ça va être la distance entre 0 et fn de 0. Cette suite là, il se trouve que c'est une suite sous-additive dans le sens suivant. Si je regarde un + m, donc c'est la distance de 0 à fn + m de 0. Et là, j'ai envie de comparer ce qui se passe pas par rapport au temps n. Et donc ben je vais utiliser triangulaire. Je veux dire que c'est plus petit que la distance de 0 à fm de 0 euh plus la distance de fm de 0 à f + n de 0. Et qu'est-ce que je reconnais? Le premier terme ici c'est um par définition et le deuxième terme ici c'est pas un mais c'est fm que j'ai appliqué au point O et FM que j'ai appliqué au point FN de O. Alors je sais que ma la transformation FM elle contracte les distances. Donc cette distance là, elle est plus petite que la distance entre O et fn de O qui est exactement un. Donc un + m est plus petit que un + UM. C'est ce qu'on appelle la sousjetivité de la suite u. Et euh quand on a de la souditivité, il y a un lem très connu qui s'appelle le lem de féqueté qui va vous dire que euh un sur n converge. Je sais pas si vous le donnez en col mais moi je sais que je l'avais eu en exercice de col. Alors, je sais plus c'était en supou ou en SP mais voilà c'est classique mais c'est facile hein parce que en fait un sur n ça va tendre vers l'ymphe des UK sur K. Et comment on démontre ça? On prend N0 tel que UN0/ N0 est proche de l'ymphe. Et ensuite quand n est beaucoup plus et quand n tend vers l'infini on écrit n c'est k x n0 plus un petit reste. fait la division euclidienne de n par n0 et en faisant ça et en divisant par n, on voit que un/ n est plus petit que un0 sur n0 plus un petit machin euh qui tend vers 0 et donc à partir d'un certain rang un sur n est plus petit que un 0 sur n0 plus un petit epsilon euh et donc si un0 sur n0 avait pris proche de lymphe ça dit qu'à partir d'un certain rang un sur n est est plus petit que lymphe + 2 epsilon Ça m'avait pris l'heure enc. Euh bref, un sur n converge. Donc c'est pas mal. Appelons la limite a vers une limite aa qui est positive ou nul. C'est pas mal ça. On sait déjà que le point fn de 0, il a une certaine vitesse asymptotique de fuite qui est linéaire qui est ce a. Autrement dit, au tempant n, on est à peu près sur une sphère de rayon n de rayon a x n. On a fait la moitié du chemin. On a montré un contrôle de la norme et maintenant il va falloir montrer un contrôle de la direction vers l'infini. Et c'est là que ça devient un petit peu plus astucieux. Euh alors, il y a un cas qui est facile, c'est si cette limite a est nulle et bah on a gagné un sur n tend vers 0 et c'est bon. pardon la taille tend vers 0 et donc fn de 0 sur n lui-même tend vers 0, c'est bon et le donc la difficulté c'est si a n'est pas nul, il faut contrôler la direction. Et pour contrôler la direction, voilà l'argument de Carlson. On va introduire un petit epsilon positif euh et on va regarder la suite un - a-s x n. Alors, un il se comporte comme a x n. Celui-là, il croit strictement moins vite. Donc cette chose là, ça se comporte comme epsil x n. Ça tend vers l'infini. Et comme ça tend vers l'infini, euh une suite qui tend vers l'infini, elle a des records. Il y a forcément des moments où elle va dépasser toutes les valeurs précédentes. Parce que si à partir d'un certain rang, elle dépassait plus les valeurs précédentes, bah elle resterait coincée sous un seuil qu'elle dépasserait jamais. Donc là, elle tend vers l'infini, donc elle a des records et je vais considérer un tel record. Elle a même des records arbitrairement grands. Ben donc je vais prendre soit grand n un record pour cette suite. Qu'est-ce que ça veut dire? Ça veut dire que pour tout i plus petit que n, je vais avoir UI moin A- e I qui est plus petit que un moin U grand NO a - eps x grand N. OK? et je vais le réécrire un tout petit peu différemment parce que c'est ça dont j'aurais besoin. Après, je vais je vais regarder U N - I. Donc je change entre I et N - I. J'ai envie de regarder un - i - un et ben il est plus petit que euh A - epsil n- i a - e n. Et si j'ai bien fait les choses, les n disparaissent. C'est pour ça que j'ai mis le n- i ici. Et donc c'est plus petit que moins a- eps x i. Très bien, pourquoi pas? Alors qu'est-ce qu'on va faire avec ce record? J'ai envie de dire que la direction de ce point au temps grand N et ben elle va me forcer tous les points intermédiaires à être à peu près dans la même direction aussi. Et c'est comme ça que je vais obtenir un contrôle asymptotique de la direction. Comment j'ai fixé la direction? Alors, on est dans un espace clidien, donc je pourrais l'écrire avec un produit scalaire, avec un vecteur, mais soyons un peu général, je vais l'écrire avec une forme linéaire. Donc je vais prendre soit h une forme linéaire de norme 1 euh qui vaut exactement un en fn de 0. fn de fn de 0 fn de 0 c'est un point qui est à distance de l'origine exactement un et donc je prends une forme linéaire qui enregistre la l'information qu'il est de taille un comme ça avec le signe de ce côtélà parce que c'est ce que j'ai envie de faire si vous préférez h c'est exactement le le produit scalaire avec mo fn0 divis par Et donc une forme linéaire en gros ça vous dit une direction. Et donc quand j'affirme que tous les points intermédiaires, ils vont être à peu près dans la même direction que fn de 0, et ben il faut que je calcule H sur le point FI de 0 et puis que je vérifie que c'est de l'ordre de AI ou quelque chose comme ça. Donc re est-ce que c'est effectivement le cas? On peut regarder H appliqué à FI de 0. Euh bah là, je vais introduire de force mon point Fn de 0 parce que c'est sur lui que j'ai une que j'ai une information. Donc je vais dire que c'est h de fi 0 - fn0 + h de fn 0. OK. Alors h elle est c'est une forme linéaire de norme 1. Donc c'est plus petit que la norme de fi de 0 fn0. J'utilise le contrôle de norme sur h et le deuxième terme alors là je vais pas écrire de d'inégalité h de fn 0 je sais exactement ce que c'est. C'est un. Donc là pour le deuxème terme j'ai une égalité c'est - un. Et alors là je suis en train de regarder la distance entre fi de 0 et fn de 0. Mais fi est une semi-contraction. Donc cette chose-là s'est bornée par la distance entre 0 et fn- i de 0, c'est-à-dire un - i. Donc c'est plus petit que un n - i- un. Et si je me suis bien débrouillé, oui, je me suis bien débrouillé. Euh c'est exactement ce que j'avais écrit au-dessus. Et donc c'est plus petit que a- epsil x i. Je vais le réécrire ici parce qu'il se passe un truc assez amusant. C'est que h de fi de0 il est plus petit que a e i et là il y a plus de n. Il y a plus de mention du point FN de0. Il y a plus rien de tout ça. Ça vous parle le jeu du temps i plus que Ah si, ça c'est juste pour tous les I plus petits que N. Absolument. Je l'ai pas écrit et j'aurais dû le dire. Je l'ai écrit 3è. Ouais. Ah oui, on sait qu'il y a des records aussi grands qu'on peut. On sait qu'il y a des records aussi grands. Est-ce qu'on pas dire qu'il y a du N dans H? H dépend de grand N. Alors H dépend de grand N et le grand N, il dépend de epsilon. C'est ce que je vais faire tout de suite. Maintenant, je vais prendre une suite epsil K tend vers 0. Pour ce epsilon K, je vais prendre un grand record que je vais appeler NK. Et disons que je vais prendre plus grand que K. Donc ma suite de record va tendre vers l'infini. J'applique cet argument et ça me vend une forme linéaire que j'appelle HK. Cette fois, je vais me me rappeler cette dépendance. Et cette forme linéaire HK, elle se comporte bien pour tous les I qui sont plus petits que NK. Mais NK il tend vers l'infini donc il va pas y avoir de problème. Et maintenant cette suite c'est une suite de forme linéaire de norme 1. Je suis en dimension 2. Donc là tout est la bouleité est compacte. Je peux extraire une sous-suite qui converge. Quitte à extraire. On peut supposer que HK converge vers une forme linéaire. Alors bah H, je suis désolé H infini comme ça il y aura moins d'ambiguité. Voilà. Euh que va vérifier ce H infini? Et ben, normalement, j'ai tout fait pour. Euh, il va vérifier que h infini de fi de 0 euh il est plus petit que Ai. Et ce pour tout i parce que si je me fixe un i, à partir d'un certain rang, il est plus petit que le NK. Donc l'hyp l'ingégalité là-haut, elle est vraie avec HK et epsilon K pour K assez grand et je peux passer à la limite dans cette ingité là pour obtenir ça. Et donc ça c'est vrai pour tout. Donc là, essentiellement, on a fini. Faut juste que je fasse un dessin. Euh voilà, un dessin. Supposons que H infini, ça soit le produit scalaire avec - E1. Juste pour simplifier, sinon vous faites tourner, ça ne change rien. Voilà la zone où h infini est plus petit que AI. Et donc là, c'est le point de l'abscisse AI. Donc à partir d'un certain rang, enfin mon point f pas à partir d'un certain rang pour tout i, mon point fi de 0, il est dans ce demi-plan à distance ai de l'origine. Mais en plus, je vous rappelle que a c'est essentiellement la norme de fi de 0. F de0, il est dans une boule de rayon euh a + epsil x i. Donc si j'avais des talents géométriques, ça serait mieux que ça, mais c'est pas le cas. Euh voilà, un cercle un cercle de rayon a + epsil x i. Et donc fi de 0, je sais qu'il est dans ce demi-plan et je sais qu'il est aussi à l'intérieur de cette boule. Donc il est à la fois bah il est dans l'intersection entre ces deux zones. Donc il est dans dans cette petite lunule. D'accord? Et plus epsilon est petit et plus l'angle de cette lunule est petit. Et donc ça montre que euh ça montre aussi la convergence en direction de fi de 0 sur i euh vers la direction qui est dictée par la forme linéaire. comme ça, si vous voulez le faire proprement, euh vous regardez les valeurs d'adhérence euh et les valeurs d'adhérence seront forcément horizontales parce que parce que le epsilon disparaît à la limite ou vous pouvez faire un calcul de norme, c'est la même chose mais le ce qui se passe c'est le dessin qui le dit, c'est pas le calcul. Oui. D'où le fait que ça marche pas avec la norme infinie. D'où le fait que ça marche pas avec la norme infinie parce qu'avec la norme infinie le dessin est jusqu'à la toute fin on peut faire le même argument. C'est pour ça que j'écris avec une forme linéaire. Avec la norme infinie, ça marche encore avec la forme linéaire. Et ça vous dit que votre point, il est dans un demi-espace comme ça et dans une boule bien ronde comme ça. Et malheureusement euh ça ça fixe pas les directions. Voilà. Dès que la norme est strictement convexe, ça va passer. Euh si la norme est pas strictement convexe, euh cette preuve ne va pas marcher. Et en fait, si vous regardez dans les notes, c'est pas juste que la preuve ne va pas marcher, c'est que le résultat est faux et on peut construire un contreexemple qui est pas très compliqué et que je vous laisse en exercice pour quand vous vous ennuierez parce que je vous ferai du lin. Et donc voilà, c'est la fin de la démonstration. Et j'aime bien cette démonstration parce que il y a il y a une astuce, c'est pas trop compliqué, ça brasse un peu de math. Euh et maintenant j'ai je vais vous la raconter en ligne. Euh est-ce qu'il y aura moyen de Alors, le vidéo, normalement, je sais faire. Hop, la lumière. C'est bien comme ça. Hop. Donc juste pourquoi j'ai pris cette preuve? Euh parce que c'est pas une preuve qui parle de truc fini. Souvent une une idée qu'on peut avoir priori quand on n pas joué avec l'assistant de preuve, c'est l'ordinateur, c'est génial parce que ça permet de représenter dans sa mémoire des objets super compliqués et ensuite on peut faire des calculs sur ces objets super compliqués. C'est certainement vrai dans dans certains cas, mais l'assistant de preuve, c'est pas juste ça. C'est d'abord on fait des preuves. Alors, une preuve, OK, c'est une suite de symbole qui respecte certaines règles. Les ordinateurs, ils manipulent très très bien les suites de symboles qui vérifient certaines règles. Et donc, le fait que ça représente des objets finis ou infinis, en fait n'est pas pertinent. Le but c'est c'est vraiment de faire des démonstrations. Euh donc ça ressemble ça ressemble à un langage de programmation. Vous avez vu COC bah c'est c'est le même genre. C'est il y a une syntaxe assez précise. On peut pas faire n'importe quoi. On peut écrire des définitions. Voilà une définition. Tout à l'heure je vous dis que c'était qu'une semi-contraction. C'était une fonction euh telle que pour tout point x à y, la distance de f(x à f est plus petite que la distance de x à y. Bah là, je vous je traduis exactement de la même manière. Alors évidemment, il faut quand même savoir qu'on est dans un contexte où on a des espace métriques et c'est l'hypothèse que j'ai marqué juste au-dessus et qui une fois qu'elle est là est en place pour tous les énoncés à suivre euh dans le fichier. Donc en plus de définitions, on peut démontrer des énoncés sur les définitions. Heureusement. Euh alors un lè que je vous ai que j'ai utilisé sans le dire, c'est que la composition de deux semi contraction, je prends F et Gux applications d'espace X vers Y et Y vers Z. Je suppose que les deux applications sont des semi-contractions. Alors leur composition est une semi-contraction. On est d'accord que c'est évident. Comme Michela l'a dit, l'ordinateur n'est pas très malin. L'ordinateur, il faut lui dire les choses. Et donc là, je lui ai dit la preuve. La preuve est illisible. Vous êtes pas censé comprendre ce qu'elle dit. C'est juste comme la preuve est triviale, je lui ai dit euh j'ai j'ai pas essayé de faire quelque chose de lisible. J'ai essayé de faire quelque chose d'efficace. Euh je pourrais faire quelque chose de plus lisible, tout aussi efficace un petit peu dans l'in comme dans comme dans coque. Il y a des tactiques, des espèces de couteau suisse qui vont faire les choses pour vous. Et donc voilà, j'espère que ça marche. OK. Euh là, je lui ai dit euh "OK, tuas tu as le droit de regarder ce qu'il y a à l'intérieur de la définition semi-contraction et après débrouille-toi." Et quand les choses sont évidentes, il y arrive. Et quand les choses sont pas évidentes, il y arrivent pas parce que la machine est bête et là on n pas un truc dia qui tourne derrière qui va faire des choses compliquées. Là, le but c'est que ce soit rapide en fait, rapide pour que ce soit interactif. Donc voilà, ce grind, je sais même pas comment on traduit ça en français, mais voilà, c'est un truc d'automatisme. Essaie de voir si c'est facile et si c'est facile, fais-le. Alors, comme je vous ai dit, c'est un c'est comme un langage de programmation. Donc, il y a une syntaxe assez stricte. Euh si j'oublie un crochet ferment, euh, il va raller qu'il comprend pas. Vous voyez à droite déjà vous vous voyez qu'il y a du rouge qui est apparu sur mon écran. Le rouge c'est dire il y a un problème et à droite lui me donne un message d'erreur. Et quand il y a pas de message d'erreur et qu'il y a à droite un goals accomplished, c'est que c'est bon, il est convaincu par la preuve et on peut passer à la suite. Alors la suite, qu'est-ce que j'ai mis? J'ai mis que l'itération d'une semi-contraction est une semi-contraction, chose que j'ai aussi utilisé implicitement quand je vous ai fait la démonstration au tableau. Euh et la preuve, on va faire une récurrence quand on a des entiers. Quoi d'autre? Une récurrence sur n euh pour le cas zéro, bah je vous ai pas dit que ça c'est f itéré n x. Et ben pour le cas 0, il faut voir que fér 0 fois c'est une semi-contraction. F itéré 0 fois c'est l'identité. Il s'agit de vérifier que la distance de x à Y est plus petite que la distance de X à Y. Le système fait sait faire ça tout seul. Donc on va utiliser une autre tactique, une autre sorte de couteau suisse qui s'appelle simplificateur qui ne fait pas la même chose que dans rock parce que ça serait trop simple. Même si vous allez remarquer plein de similitudes les récurrence, on appelle ça induction à la fois dans Rock et dans Lin. Rock est très très Line est très très inspiré de Rock par beaucoup de côtés et un petit peu de Isabelle par d'autres côtés. Euh donc pour le cas de base de la récurrence, le simplificateur si on lui dit "Tu as le droit de regarder l'intérieur de la définition de semicontraction", il se débrouille tout seul. Et le cas n + 1, on dit au simplificateur débrouille-toi mais tu as le droit à utiliser quelque chose. Qu'est-ce que tu as le droit d'utiliser? Tu as le droit d'utiliser comp. C'est quoi comp? C'est le lem qu'on a démontré auudessus, le lem semi-contraction point comple. Et donc ce lem comp il prend deux hypothèses. Il prend en fait quand on applique un théorème, on mange des hypothèses. C'est comme quand on applique des fonctions, on mange quelque chose et puis on renvoie autre chose. Et donc là qu'est-ce qu'il mange? Il mange deux deux hypothèses. Le fait qu'une première application une semi-contraction et le fait qu'une deuxième application une semi-contraction. Ici euh il il mange mon hypothèse de récurrence. C'est mon hypothèse de récurrence, c'est que F itéré n fois est une semi-contraction. Et il mange aussi le fait que F tout court est une semi-courcraction. Donc cette chose-là va vous renvoyer le fait que euh f^ n composé avec f est une semi-contraction. Alors après, il faut se rendre compte que ça c'est la même chose que fn + 1 euh et le simplificateur va le faire pour vous. Donc ça correspond vraiment à la preuve qu'on a envie de faire. Si on devait écrire les détails sur un papier, on les écrirait comme ça ou si on devait expliquer les les détails à un étudiant de début de sup. On l'expliquerait comme ça aussi. Qui est-ce qui a écrit? Qui écrit ça? C'est toi ou la machine? Moi. Alors là, tout ce que tu vois à l'écran, c'est moi qui l'écrit. La le rôle de la machine, c'est pas d'écrire des choses, c'est de comprendre ce que je lui dis. Ça s'appelle assistant de preuve euh en français et le terme est pas très bon. On devrait appeler ça un vérificateur de preuve. Moi, je tape une preuve et Line regarde et me dit euh soit je suis convaincu, soit je suis pas convaincu. Quand L n'est pas convaincu, ça apparaît en rouge. Elle me dit non, là ça va pas. Il me faut plus de détails. Et là par exemple grind, ça n'aurait pas été Alors euh bah on peut regarder. C'est ça qui est bien, c'est que euh alors je pense que grind ne va pas marcher et je te dirai juste après pourquoi. Voilà, là on voit que grind ne marche pas. Là, il te dit à droite grind failed. Et pourquoi? parce que grind couteau suisse assez puissant mais qui va juste travailler avec ce qu'on lui dit de regarder. Alors que le simplificateur lui dans toute la bibliothèque qui est derrière, il y a plein de lemes qui sont enregistrés et où on dit qui que le simplificateur doit essayer de les appliquer dès qu'il peut. Et donc c'est pour ça que c'est deux tactiques différentes. Grind est plus puissant mais va utiliser moins de lem déjà enregistré dans dans la bibliothèque. Et donc là grind ne doit pas savoir que f itéré zé fois c'est l'identité alors que le simplificateur lui le sait. Ça a été défini où ça? Alors de quoi? Donc f itéré 0 fois c'est l'identité. Ça alors c'est un lè qui a été démontré quelque part. Euh on peut aller voir la définition de l'itération N. Euh c'est défini dans un autre fichier de la bibliothèque. Oui. Alors là c'est même pas dans si là c'est dans Matli Lib je vous parlerai un petit peu plus tard après avoir raconter la preuve de ces problèmes de bibliothèque et de où les choses sont agencées. Et donc si on va voir la la définition de l'itération d'une fonction un tout petit peu plus bas, vous voyez un premier lem qui s'appelle iterate zero qui dit que f itéré 0 fois c'est l'identité et vous voyez au-dessus ce ad qui vous dit simplificateur dès que tu vois f^ 0 n'importe où tu le remplaces par l'identité en appliquant ce lem et c'est c'est pour ça que simple se débrouille bien dans le fichier cardson juste par curiosité si le lem qui fonctionne enfin qui tont dont il a besoin là ça s'appelle iterate zer grind mais que tu lui dis qu'il faut appliquer iterate zer est-ce que ça va suffire ou est-ce qu'il y a alors et ben on va faire ça grind semicontraction et iterate zer alors non ça ça n'a pas marché ça n'a pas marché ça n'a pas marché fallait autre chose. Voilà. Mais donc le quand le simplificateur marche, c'est parfait. Comme je vous ai dit, moi je suis un utilisateur de ces choses-là. Euh j'essaie de de vous convaincre que vous aussi vous pouvez l'utiliser. Pourquoi il y a Pourquoi il y a pas une un une fonction l'équivalent de simplificateur qui lui dit essaye toutes les fonctions possibles? Alors, il y a aussi il y a aussi toute la postulie. Ouais, ça marche. Oui. Ouais. Non mais exactement comme enfin je un théorème on dit en utilisant le lemah on pourrait aussi dire l'un des l précédents doit servir. Donc je les essaye tous même si ça n'a aucun sens. Une explosion l'occurrence. Non non tout celle qu'on a prédéfinie. OK. F. Du coup, voilà, je voudrais démontrer que euh voilà, je prends une fonction f de r dans r, je vais vous montrer que féré 0 fois, c'est l'identité. Donc, je vous ai dit que on peut faire le simplificateur parce qu'il saura le faire, mais on peut aussi lui dire explore toute la toute la bibliothèque. Je suis désolé, ça risque de ne pas marcher. Mais ce exact point d'interrogation, ça explore toute la bibliothèque, ça essaye tous les lem et de voir s'il y en a un qui s'applique dans cette situation. Et effectivement, si on va voir à droite, il me dit "Try this, apply exact iterate 0 f". Voilà. Donc il y a des il y a des fonctions de recherche comme ça qui vont essayer l'élève. Ça c'est métal. Du coup, qu'est-ce qu'il a cherché en dehors du Exact? C'est on le laisse pas avec les confation, c'est quand on tape, ça va proposer un truc pour remplacer du coup. Tout à fait. Mais c'est pas juste métap parce que là, la preuve est complète quand même. Sans qu'on clique dessus. Oui. OK. parce que euh exact point d'interrogation en interne a renvoyé exact iterate zero f mais ça rend ça plus explicit il faut pas le laisser parce que exact point d'interrogation c'est une tactique qui explore toute la bibliothèque ça prend du temps euh donc autant le remplacer par le truc précis qui va pas exp explorer la bibliothèque entière et qui va juste mettre la bonne chose. Continuons la preuve. le que j'ai utilisé implicitement là. Oui, vous utilisez des d'objets sur votre lettre, ça veut dire vous contrayez point à chaque fois et tout. Alors, j'ai pas compris la question. Quand vous créez quand je crée un quand vous créez point direct avec votre LEM, ça veut dire vous rajouter une propriété objet. Alors non euh c'est vraiment des il y a pas du tout de notion de programmation objet en ligne. C'est vraiment les les l'emm c'est comme des fonctions indépendantes les unes des autres. Après, il y a un système de nommage qui est fait que les lèves sur les fonctions, typiquement, on va les appeler function point quelque chose, mais c'est juste un système pour se rappeler et pour rendre les choses faciles à utiliser mais il y a pas de notion d'objet derrière. Donc lem existence de record. Quels sont les entrées de Solem? J'ai une une suite U de N dans les nombres réels. J'ai une hypothèse sur cette suite U qui est que U tend vers plus l'infini en plus l'infini. C'est ce que le atop veut dire. Et j'ai un entier grand N. Et la conclusion, c'est que il existe un petit n au-delà de ce grand n qui est un record, c'est-à-dire que un bat toutes les valeur de um précédente. Donc c'est un truc que j'ai utilisé implicitement ici que je vous ai expliqué à l'oral. Euh quand on fait du lin, on peut pas ou du rock, on peut pas expliquer à l'oral. Il faut expliquer tous les détails et ce ce lem qui a l'air stupide. Je vous ai dit bah si on avait pas de record alors on serait coincé en dessous d'un maximum et on le dépasserait jamais. Et ben, il va falloir dire l'argument en mettant quelques détails. Et les quelques détails, c'est ça. Donc c'est un peu plus long même si ça c'est censé correspondre exactement à ce que je vous ai dit. On va regarder le on va dire si c'était pas le cas. Le BU contrat, ça veut dire on va faire un raisonnement par contradiction. Euh bah si c'était pas le cas, s'il y avait pas de record au-delà du temps grand N, et ben ça ma suite resterait éternellement bloquée en dessous du maximum avant le temps grand N. Et c'est juste ça que je dis à l'ordinateur. Alors il faut réussir à lui dire d'une certaine manière. Et donc je définis ce grand M qui est quoi? Qui est le maximum de ma suite jusqu'au rang N. Et ensuite, je démontre par récurrence que un est tout le temps plus petit que ce grand M. Euh, je le démontre par récurrence en séparant deux cas. Soit n est plus petit que grand n et à ce moment-là un est plus petit que le maximum, soit n est plus grand que grand n strictement. Mais à ce moment-là, euh mon hypothèse par l'absurde me dit que il est plus petit que une valeur de u auparavant. Et cette valeur de U auparavant, par mon hypothèse de récurrence, elle est plus petite que grand M. Et donc U lui-même est plus petit que grand M. Et c'est fini. Et donc ma suite est tout le temps bornée par grand M, mais comme elle tend vers plus l'infini en plus l'infini. Ah oui, merci. Ah ouais, je suis désolé. Euh mais comme elle tend vers plus l'infini en plus l'infini euh il existe il doit exister un entier où un est plus grand que m + 1. C'est la définition de temps vers vers l'infini en plus l'infini. Et donc on a d'une part montré que un était tout le temps plus petit que grand m et on a montré qu'il y avait un moment où c'était plus grand que grand m + 1. Et ça c'est une contradiction et c'est fini. Euh Mikaela vous a dit que euh les preuves on peut les faire en forward ou en backward. Euh moi je suis plutôt forward parce qu'en fait ça correspond au flow que je vous ai raconté là-bas. Donc je construis mais on peut tout à fait faire du backward aussi en ligne. C'est ça dépend vraiment du goût des gens et du type de preuve aussi. Donc l'argument que je vous ai raconté, il y a des moments où il faut avoir des idées entre guillemets. Il faut avoir l'idée d'introduire le maximum de mat jusqu'au rang grand. Il faut avoir l'idée de faire une récurrence forte. Il faut avoir l'idée de séparer les les cas N et plus petit que grand N ou plus grand que grand N. Une fois qu'on a eu ces idées, normalement tout est facile, il y a plus qu'à dérouler les définitions. Et c'est exactement ce que je fais là. Euh dérouler les définitions et se débrouiller tout tout seul. C'est ce que Grind fait là, là et là parce que je suis Flemar. J'aurais pu écrire tous les détails, ça aurait pris deux ou trois fois plus de lignes. Et le but du jeu, c'est quand même on explique les idées et on ne rajoute des détails que si l'assistant de preuve réussit pas à se débrouiller tout seul. Mais c'est c'est suffisamment bien fait pour que souvent ça réussit à se débrouiller tout seul. Après, cela dit, si au début de la preuve j'avais mis by Grind, euh évidemment il aurait pas réussi. Alors là, ça commence à être long. Euh vous vous doutez bien que j'ai pas pu taper ça directement comme ça sans faire la moindre faute de syntaxe. Euh et donc c'est un c'est la manière d'utiliser ces assistants de preuve, c'est des assistants de preuves interactifs. C'est-à-dire que euh on commence la preuve. Alors ici euh donc exactement comme tout à l'heure dans COC, vous voyez, il y a une fenêtre qui vous dit toutes les informations qui sont en cours. Là quelles sont les données en cours? On a une suite U de N dans R. On sait que cette suite tend vers euh l'infini en plus l'infini et on a un entier grand N. Et notre but, le truc qu'on doit montrer, c'est que tout tout à l'heure en rock, c'est c'était en dessous du petit trait, c'était le truc qu'on devait démontrer. Donc là, il y a ce symbole là qui veut dire essentiellement la même chose et que vous vous avez vu tout à l'heure dans les exposés aussi. Euh le but, c'est de montrer qu'il existe un n plus grand que grand n tel que bla bla. Donc si j'applique un raisonnement par contradiction euh et ben il va me contredire cette hypothèse. Alors il sait intervertir les quantificateurs sans se tromper normalement et le sens des inégalités. Et donc on va savoir que pour tout plus grand que grand n il existe Ouais. Ouais il a bien travaillé. Il a mis une inégalité stricte, il a renversé c'est bien. Et donc il faut arriver au fait que on a quelque chose de faux. et je commence à définir le grand thème. Voilà, j'ai défini mon grand thème qui apparaît maintenant dans mon contexte. Et quand je démontre euh je dis que un est plus petit que grand m pour tout n et ben je suis entré dans une sous-preuve et dans cette sous-preuve mon but c'est de voir que un est plus petit que que grand m et je fais la récurrence et puis bah je peux appliquer des lèes. Et là par exemple, j'ai appliqué mon LEM pour dire que je veux voir que un est plus grand que grand n qui est défini comme un maximum. Et donc bah il s'agit de voir que un appartient à l'ensemble dont j'avais pris le maximum. Et bon bah la grind fait le travail et puis je sais pas pourquoi il réapparaît tout le temps en haut. Vous faites échappe? Oui, je passe mon temps à faire échappe. Oui, oui, parce que j'ai OK, bah on va vivre avec alors. Mais sinon, si j'aime pas la salle, vous pouvez le laisser moi. Je pense qu'il est en haut, il ne cache rien donc on va le garder. Et donc là, on arrive dans la deuxième partie de la récurrence où on a supposé que petit N était plus grand que grand N. Et alors là, j'ai l'hypothèse de récurrence qui est à ma disposition. Donc c'est-à-dire que pour tout petit M plus petit strictement plus petit que petit N um UM est plus petit que grand M. Et j'ai mon hypothèse absurde 10 qui est tout là-haut et grind il va combiner les deux et il va enchaîner trois signalités toute seule et il va il va voir que on que euh on a bien un n plus petit que grand m. Donc une preuve, ça ça s'improvise pas comme ça, c'est on la remplit petit bout par petit bout et à chaque fois on voit ce que le système demande et soit grind ou un ouou une autre tactique surpuissante termine et c'est très bien, soit c'est pas le cas et on rajoute des détails. Euh donc je vois que je suis allé beaucoup plus lentement que ce que je pensais, mais c'est pas grave. Euh on va continuer un tout petit peu la preuve. On va finir la preuve. Euh, on peut introduire des notations. U, c'est exactement la suite un que j'avais introduite. C'est la distance entre f de 0 et 0. Et on veut montrer que u est sous-additive. Alors, le subadditive ici, j'ai pas eu besoin de le définir. C'est quelque chose qui était déjà défini dans la bibliothèque sur laquelle je m'appuie. Et pour démontrer que U est sous-additive, comment on avait fait? On avait dit que um + n, c'était la distance entre f + n de 0 et 0. J'avais appliqué l'unité triangulaire pour entrer le point fn de 0 au milieu de force et ensuite j'avais utiliser la semi-contraction pour dire que la distance de fm + n de 0 à fn de 0 s'était bornée par la distance de fm de 0 à 0 et j'avais dit que ça c'était um et làà vous normalement vous reconnaissez exactement la preuve que je que je vous ai faite au tableau avec cette syntaxe qui est faite pour imiter justement la syntaxe mathématique des suites de calcul Et la grosse différence, c'est que quand je vous ai fait la suite de je vous avais juste écrit la suite d'inégalité. Là, quand je l'explique à Line, à chaque fois pour chaque inégalité, j'ai besoin de lui justifier pourquoi est-ce que cette inégalité est vraie. Là, vous vous voyez la première le premier pas, c'est une c'est une égalité qui est vraie par réflexivité. Le deuxième cas, il est vrai en appliquant le lem de linget triangulaire. Le 3è lem, il est vrai euh en faisant un un rewrite que M et N commute. Bref, il faut appliquer les lèes pour justifier chacune des étapes. Mais euh donc c'est un peu plus détaillé que ce que je vous ai dit au tableau, mais c'est pas fondamentalement beaucoup plus détaillé. Euh une fois qu'on a fait ça, euh j'introduis la limite, j'affirme que euh un/ n tend vers la limite. Alors, il y a une lettre n bizarre parce que c'est le filtre des voisinages. J'ai pas envie de vous en parler. Euh non mais j'avais envie de vous en parler mais je vais pas assez vite. Euh il y a une différence avec ce que je vous ai dit c'est que au tableau je vous ai dit le lemme de feté vous dit vous avez une suite un qui est subjective alors un sur n converge. Et là j'avais été un peu flou parce que je vous avais pas dit dans quoi ça convergeit. En vrai, ça converge vers une limite qui peut être moins l'infini si votre suite décroit trop vite. Mais si la limite est moins l'infini, c'est vachement moins pratique parce que après tout alors dans l'application, c'était pas le cas parce que ma suite était toujours positive. Mais donc dans la bibliothèque Matlib sur laquelle je m'appuie, il y a différentes versions du LEM de FQT mais la version qui est la plus pratique à appliquer ici c'est le cas où la suite un sur n est bornée inférieurement parce que comme ça je sais que la limite sera un nombre réel et je serai pas embêté avec desah pour passer de l'un à l'autre et donc là pour appliquer ce lem j'ai besoin de vérifier que un sur n est borné inférieurement alors c'est très facile parce que c'est borné inférieurement par zéro parce que c'est positif ou nul N'empêche qu'il faut le dire. C'est quelque chose que vous que je vous avais pas du tout dit quand je l'avais fait au tableau et je considère pas que je vous avais arnaqué. C'était pas c'était pas une erreur. C'était juste c'était évidemment vrai pour vous et pour moi et donc on avait même pas besoin de le dire. Et ben là quand on fait de la vérification de preuve, il y a besoin de dire tous ces détails. Donc c'est parfois un peu fastidieux plus que quand on interagit et qu'on se comprend à demiot. En même temps, ça évite ça garantit qu'on dit pas de bêtises. Une fois qu'on a fait ça, donc la limite, elle est positive ou nulle sans problème. Ensuite la suite un - a - eps x n tend vers l'infini. Bah là, je vous avais dit c'est équivalent à epsil x n donc ça tend vers plus l'infini. Ben là, c'est la même preuve, sauf qu'il faut dire plus de détails parce que bah travailler un peu avec les limites, il faut faire attention. Alors, c'est pas c'est pas fondamentalement compliqué, mais c'est un peu plus long. Euh bah là, j'avais envie de vous parler de Exact. Là, on applique un lem un peu compliqué euh qui est pas évident à trouver dans la bibliothèque, mais euh si on sait pas comment ce lem s'appelle, il y a ceux exact qu'il trouve assez facilement dans la bibliothèque. Et donc la suite continue encore et encore. Euh donc c'est un peu long, hein. C'est un peu long. C'est pas horriblement long, mais c'est un peu long. Mais euh c'est vraiment les mêmes arguments que ceux que je vous ai fait là. Euh là, c'est un en un temps grand N fixée, on peut trouver une forme linéaire H qui se comporte bien jusqu'au temps grand N. On commence par utiliser un record. Euh en ce record, on trouve une forme linéaire qui a la bonne norme et qui se comporte bien comme on veut. Alors là, tout à l'heure, je vous ai un peu arnaqué mais c'est pas grave. J'ai dit soit h une forme linéaire de norme 1 qui vaut- sur fn de 0. Euh là on est dans R2 donc ça marche très bien mais la formalisation que je suis en train de faire je la fais dans RD et quand on est sur un espace vectoriel de dimension zéro il y a pas de forme linéaire de norme 1. Il y a que la forme linéaire nulle et donc elle est de norme zéro. Et donc en toute rigueur, si on veut faire cette formalisation sur un espace RD général, et ben la forme linéaire qu'on va obtenir ne sera pas de norme 1 mais de norme inférieur égale à 1. On n' pas l'habitude de penser à ces cas limites mais quand on formalise on est bien obligé parce que sinon le système n'est pas d'accord. Il est il est pas il est c envie. C'est pas possible de l'arnaquer mais c'est justement l'intérêt de la chose. On peut pas éviter les cas limites. Par contre quand on a fini on est sûr de soi. Euh et ensuite euh on va prendre une soussite de CHK. Alors là, il y a quelque chose d'assez amusant, c'est que j'ai utilisé l'axium du choix. Si on regarde ce qui se passe là, ça ça me dit en cas fixé, je peux trouver une HK qui vérifie l'invité qui m'intéresse. Dire que pour chaque cas, je peux trouver un HK qui marche, c'est pas la même chose de dire que il existe une suite HK qui marche pour passer de l'un à l'autre. C'est une forme de l'axium du choix dénombrable. dénombrable mais on a du mal à s'en passer mais même l'action du choix tout court, moi j'ai du mal à m'en passer et donc bah là c'est un choix est-ce qu'on l'accepte comme axium ou pas parce que comme on vous l'a expliqué dans les exposés précédents, c'est pas quelque chose qui est euh qui est introduit de base dans la logique de ces systèmes et donc ça doit venir comme un axium supplémentaire mais la bibliothèque Matlip sur laquelle je m'appuie et qui est surtout utilisée par des mateux les les mat ont pas beaucoup de problèmes avec l'axium du choix et en fait à la ligne 1, on suppose l'axium du choix et on s'en sert tout le temps après. Donc d'un certain point de vue, c'est pas génial parce que ça veut dire que parfois on peut pas extraire de programme à partir de preuv mais si le but c'est de faire des preuves, bah c'est pas grave. L'axium du choix c'est pratique. Donc voilà, là j'applique l'axium du choix pour prendre ma suite et puis après je vais extraire une sous-suite convergente. Là c'est encore très constructif. Mais c'est pas grave, je suis pas en train de mettre les choses à l'intérieur de la mémoire de mon ordinateur. Je suis en train d'appliquer des théorèmes. Et théorème constructif ou pas, c'est des théorèmes qui s'appliquent très bien. C'est des suites de symboles comprises par le système. Alors évidemment pour pouvoir extraire une sous-suite comme ça, il faut savoir que le dual est propre, que la boule unité est compacte, mais ça c'est des choses qui ont déjà été démontrées dans la bibliothèque. Et donc je peux extrême ma sous-suite convergente et passer à la limite et continuer la preuve. Et bon, je vois que c'est la fin donc je passe vite. Mais la suite de la preuve euh c'est du même tonneau une fois qu'on a compris un peu la syntaxe. Euh c'est pas beaucoup plus compliqué. Est-ce qu'on modélise le le dessin? Alors on modélise pas le dessin euh on on fait le calcul et c'est un peu frustrant parce que l'intuition elle est dans le dessin mais certains pourraient dire que c'est pas une preuve. Donc euh il faut trouver un truc un argument plus formel. Euh alors, on peut le faire soit à base de valeur d'adhérence, soit euh voir que une fois qu'on est dans la luule, on peut estimer la norme entre FI de 0 sur i et puis le vecteur V qui dirige l'hyperplan et voir qu'elle est petite avec un une sorte de cochich ou un truc comme ça. Et je crois que c'est ça que j'ai implémenté ici parce que ça a l'avantage de marcher aussi dans des dans des espaces de Hilbert parce que là je l'ai raconté dans R2 mais en fait la preuve marche très bien en dimension infinie aussi. Il y a pas de différence. Bon, il faut prendre des limites faibles mais c'est un détail. Euh, je suis en retard. Je voudrais juste vous montrer qu'il faut faire attention. On pourrait se dire "OK, une fois qu'on a formalisé une démonstration, c'est bon, on a fini et donc on sert plus à grand-chose. On peut faire une confiance aveugle en le système en un sens." C'est vrai parce que ça vérifie les preuves. Si vous donnez un théorème et qu'après vous donnez une démonstration du du théorème, vous avez une garantie à 100 % que la démonstration est bonne. Enfin, si le système est content et donc votre théorème est démontré. Ce qui est pas évident, c'est euh est-ce que le théorème que vous avez écrit dit vraiment ce que vous pensez qu'il dit ou pas? On pourrait se planter dans les définition, on pourrait se planter dans les énoncés et en fait c'est des choses qui arrivent relativement souvent. Et je voulais juste vous en donner un exemple ici. Euh voilà une autre version euh du théorème de Colberg et Neyman que je vais démontrer en deux lignes. Le théorème dit c'est essentiellement le même. Il existe un vecteur V dans E tel que alors je regarde la fonction qui en entier n associe fn de 0 que je multiplie par le scalaire 1/ n et donc cette suite là qui est dans mon espace vectoriel converge en plus l'infini vers ce point V. Voilà une preuve. Euh, j'affirme que le vecteur V é= 0 va convenir. Euh, et parce que en fait à partir du rang 2, c'est ce que ça dit là, à partir du rang 2, cette suite va être égale à zéro. Vous avez le droit de pas être d'accord mais n'empêche que là, il y a il y a il y a pas de rouge, donc le système est convaincu. Vous êtes peut-être pas d'accord, mais vous avez tort. Parce que si Line vous dit que c'est vrai, il y a pas de doute. Où est la subtilité? La subtilité, c'est que là, j'ai pas préciser ce que c'était que ce 1/ N. N est un entier. Si je dis rien de spécial à Line, il va se dire "Et bah j'ai un entier. Euh, un sur n, bah ça doit être un entier aussi. Ah non non, c'est la division tronquée. Je peux prendre un entier, je peux le diviser par un autre entier et ça va me faire la partie entière de la division dans les rationnels. On a enregistré une division sur les entiers dans la bibliothèque parce que parce que c'est un truc qui sert souvent. Et donc là, comme j'ai rien dit, Yaline, il voit là, il voit un entier, il dit "Bon, on divise par un entier, ça doit être un entier aussi, ça doit être la division dans les entiers ça. Donc ça doit faire l'entier zéro." Mais alors, est-ce que ça a bien un sens? Est-ce que je sais faire agir les entiers? sur mon espace vectoriel E. Bah oui, parce que E c'est un groupe additif. Et dans les groupes additifs, on a défini une action des entiers, c'est euh n appliqué à x, c'est x + x + x n x. Donc le système se dit qu'il a compris ce que je voulais lui dire parce que ça correspond à des choses qu'on a déjà définies dans la bibliothèque. Et donc il est parfaitement content, il comprend ce que c'est mais comme ça c'est l'entier nul. euh l'entier nul appliqué que bref ça fait zéro et donc ce la est démontré donc il faut faire attention c'est pas le système va tout faire pour vous c'est il faut vraiment avoir un esprit critique et il faut comprendre ce que ça dit il y a des gens qui s'amusent à utiliser de l'IA pour démontrer des énoncés et deux fois sur trois trois fois sur quatre ils connaissent pas bien les assistants de preuve et les énoncés qu'ils écrivent ne correspondent pas du tout à ce qu'ils pensent que ça veut dire et souvent c'est totalement inutile. Donc pour raconter tout ce que je viens de vous dire euh il faut quand même il y a pas mal de maths. Là je vous ai parlé des nombres réels, je vous ai parlé d'espace vectoriels normés euh je vous ai parlé de la boule unité du dual et compact. Je vous ai parlé de prendre des sousites. Je vous ai parlé de plein de choses en fait. Et si j'avais dû vous définir toutes ces choses-là pour vous faire la preuve, au lieu de prendre 230 lignes, ça aurait fait 20 ou 30000 lignes. Rien que pour définir les réels, c'est quoi les réels? C'est les classes d'équivalence de suite de cochie de rationnel. Donc il faut définir ce que c'est que des suites de coches rationnelle. Il faut définir les suites de il faut définir ce que c'est que des rationnels. Il faut il y a plein de choses qu'il y a avant. Et donc pour formaliser des maths, on peut pas partir de rien. Il faut des grosses bibliothèques dans lesquelles il y a beaucoup de choses qui sont mises. Et là je m'appuie sur cette bibliothèque qui s'appelle Matlib et dont je vais pas plus vous parler aujourd'hui parce que parce que j'ai plus le temps, mais je vous en parlerai demain. Merci. Est-ce qu'il y a des questions? Oui. Oui. Si on peut vérifier qu'une partie de la preuve pour aller pour gagner du temps, c'est risqué péril évidemment. Est-ce qu'on peut lui demander d'admettre des lèves? Tout à fait. Euh tout à fait. On peut dire euh "J'écris tel lem et puis je suis désolé mais j'ai pas envie de te le démontrer". Et euh quand je dis ça, c'est pas c'est pas juste une figure de style. C'est euh Je suis désolé mais j'ai pas envie de te voilà. Et donc là, il me dit "Gaals accomplish". Donc il considère que j'ai terminé la preuve. Évidemment euh c'est pas génial. Et donc ensuite euh surtout si je fais un autre théorème qui utilise celui-là et donc il y a des commandes pour dire est-ce que tu peux me vérifier que tous les lèes sur sur lesquels ce théorème repose ont vraiment été démontrés qu'il y a pas de soris ailleurs mais il n'empêche que quand on construit une bibliothèque en fait on fait ça souvent on admet des trucs on se concentre sur les parties intéressantes et puis après on reprend les trucs qu'on a admis et puis on les fait on se rend compte qu'on s'était planté et on répare tout derrière mais même ce qu'on a fait avant ça c'est quand même en fait c'est comme quand on écrit un article de math quand on écrit un article de math c'est jamais linéaire on commence par le premier lè mais on se dit c'est lui qui non on commence par le milieu on trouve un lem on se dit que ça va être important et puis que ça va servir et puis ah mais il y a peut-être et on remplit les trous au fur et à mesure et une procédure de construction de preuv formalisé ça ressemble beaucoup à une procédure de on fait des maths remettre la vraie preuve parce que je me sens plus à l'aise. Donc là, on a utilisé donc des actions supplémentaires, action du choix et puis on a inversé des des quantificateurs à un moment. Donc c'est pas purement constructif. Tout à fait. Et donc ça produit quand même quelque chose qui est un certificat d'une certaine manière ou Ah c'est une oui oui. OK. Mais dans la preuve c'est il y a écrit qu'on a action de c'est c'est une preuve une preuve au sens mathématique mais qui utilise l'axium du choix. Oui, c'est une preuve quand même. Et quand on utilise ça, du coup quand on cherche un théorème, on voit facilement qu'est-ce qui a été utilisé. Justement par exemple, on prend un résultat qui est très loin dans la bibliothèque qui repose sur beaucoup de choses. On peut savoir facilement si alors euh j'ai envie de dire que non parce que tu vois là si je demandais qu'est-ce que ça utilise dans la bibliothèque, ça ça utiliserait des dizaines de milliers de définitions et de résultats. Donc ça serait pas vraiment exploitable, tu vois. Voir que ça utilise la théorie des espaces uniformes pour construire la compétion de Q. Dès que je parle de R, ça utilise la théorie des espaces uniformes. Mais mais lui demander explicitement genre est-ce que ça utilise du choix par exemple? Enfin, s'il y a des choses par alors euh pour les axiomes, oui, mais en fait des axiumes dans Matlib, il y a juste l'axium du choix et il y a essentiellement tout qui utilise l'axium du choix. Donc euh euh alors je vais pas retrouver la la syntaxe exacte mais si je fais ça, c'est pas la syntaxe. Bon non, je vais pas retrouver la syntaxe. Euh mais donc je suis sûr que cet énoncé utilise l'axium du choix. Il faut savoir que comme on a aucun complexe avec l'axium du choix, euh le tiers exclu est démontré à partir de l'axium du choix. Il y a un argument astucieux assez joli qui déduit le tiers exclus de l'axiom du choix. Donc c'est c'est pas besoin d'admettre les axiumes tiers exclus et axiom du choix. L'axium du choix suffit. Mais en tant que mathématicien praticien, moi je m'en moque parce que je suis juste en train de faire des démonstrations. Est-ce que tu travailles dans un domaine des mathématiques où c'était possible de faire ça? Et peut-être qu'il y a d'autres domaines des mathématiques ou ce genre de d'approche te semble peut-être plus difficile? Alors euh Matlib couvre à peu près euh toutes les mates jusqu'au niveau Greg disons, plus euh des pics dans plein de directions de recherche en fonction des des motivations des gens. Pour moi, tout est formalisable euh à condition d'y passer du temps parce que comme tu as vu, c'est quand même un peu lourd, mais euh je vois aucun obstacle intrinsèque qui empêcherait de formaliser n'importe quel théorme. Et combien de temps ça rajoute pour écrire un article par exemple? Mom j'ai papier et je veux je veux le vérifier en pourcentage de temps plus 200 % plus 50 %. Ça dépend énormément parce que ce qui prend du temps euh c'est de formaliser les prérequis. Tu vois là si je veux formaliser la preuve de Carlson et que tous les prérequis sont faits, ça en une après-midi, c'est bon. Euh si il faut que je reconstruise les nombres réels, ça va me prendre un an. Et le problème c'est que pour les maths de recherche actuell, la plupart des prérequis ne sont pas formalisés. Et donc là euh il y a peu de résultats de recherche qui sont formalisables sur mes travaux. La plupart je peux pas les formaliser. Il y en a quelques-uns que je peux et à ce moment-là bah je suis très content de le faire mais la plupart du temps, c'est pas possible parce que ça serait trop lourd. Mais c'est c'est parce que c'est récent parce qu'on peut imaginer qu'il y a une communauté qui s'active et que c'est cumulatif. Oui. Oui. Surtout que c'est open source donc n'importe qui peut venir et rajouter des choses. Mais malgré tout les les maths c'est gros. Il y a beaucoup de choses et ça prend beaucoup de temps à construire. Surtout que si on va faire les choses bien euh ça prend du temps. Il faut c'est exactement ce dont je parlerai demain. Est-ce qu'il y a Est-ce qu'il y a des des concurrents à Matle? Alors oui, alors des concurrents, des partenaires, des partenaires parce que parce que c'est euh donc dans rock, il y a plusieurs bibliothèques euh qui permettent de il y en a une qui s'appelle Mathcompe qui fait plein de types de math avec disons que c'était plus algébrique au début mais maintenant il y a Matrompe Analysis qui rajoute une composante d'analyse avec la théorie de l'intégration et tout Dans Isabelle Choel, il y a aussi une bibliothèque centrale. Après, les différences, c'est un petit peu sur les modèles de gestion de la communauté et sur à quel point on est plus orienté math ou info. Tu vois là le fait d'utiliser l'axium du choix à partir de la ligne 1, c'est un truc qu'on a qui ne fait pas peur au Mattheux mais qui peut déranger dans certaines communautés. Donc c'est des choix et ça ça fait que tu as des bibliothèques qui sont construites un peu de manière différente et tu choisis celles qui correspond le plus à ce que tu as envie de faire. C'est c'est une richesse en fait. Est-ce qu'il y a des domaines disons qui sont plus adaptés? Moi je pensais par exemple domaine un peu formalisé quand même théorique des catégories ou des domaines algébriques qui nécessite moins de connaissance ou d'action du choix par exemple. Ouais. Oh théorie des catégories, il y a souvent des axumes du choix quand même. Mais euh alors en j'ai envie de dire que plus c'est proche des axiomes et plus c'est facile à formaliser. Moins il y a euh moins il y a de points de suspension dans les formules et moins il y a d'agitage de main et plus c'est facile. Donc j'ai envie de penser que le pire ce sera la géométrie différentielle. Euh la théorie des catégories euh on pourrait dire que c'est facile. En fait, c'est pas si facile que ça parce que il y a souvent des identifications, des petites triches dans la littérature, des choses où bah il y a on a quand même un raisonnement fluide où on va identifier les objets qui sont pas formellement les mêmes. Là Matlib, R et R2, c'est pas la même chose, hein. R2 c'est les fonctions de 01 dans R alors que R c R c'est les paires de points réel, c'est pas la même chose. Et donc tous les endroits où on fait des des identifications comme ça, on en fait tout le temps en fait. Et ben quand on commence à formaliser, on se rend compte que il faut faire un peu attention et ça pose parfois des difficultés à des endroits où on s'y attend pas trop et ça a tendance à être le cas en théorie des catégories. en théorie des nombres, beaucoup moins. Donc la théorie des nombres se formalise très bien. Euh cela dit, je parlais de géométrie différentielle. Il y a eu un très joli projet mené par Patrick Masso où il a démontré le théorème du retournement de la sphère. Vous avez traitement vu des vidéos qu'on peut prendre une sphère et on peut la déformer continuement sans qu'il y ait de pli pour à la fin de la déformation. Donc elle a le droit de se traverser elle-même mais on n' pas le droit de bref à la fin de la il faut que ça reste une immersion en permanence à la fin de la déformation avoir échangé l'intérieur et l'extérieur. C'est un théorème qui avait été démontré à la fin des années 60 par SMIL de manière non constructive. C'est-à-dire que il savait que ça existait par des arguments de topologie algébrique abstrait et il savait pas comment faire. il avait pas d'exemple et au fil du temps euh il y a plusieurs constructions explicites qui ont été faites et il y a des démonstrations plus conceptuelles qui ont été donné aussi. Et donc Patrick Massau a mené une formalisation de ce théorème. Donc ce théorème est démontré en ligne. Façon constructive ou pas? Alors euh bah il y a l'action du choix partout. Non c'est pas il a fait un dessin et il a montré que ce dessin convenait. Il il a utilisé un processus de déformation qui initialement dû à Gromof avec des corrugations. Si vous avez jamais vu ça, vous pouvez regarder sur internet, il y a des très belles images. Et donc c'est un théorème abstrait qui s'applique de manière beaucoup plus générale que pour le retournement de la sphère et dont le retournement de la sphère est un cas particulier. Vous disiez que c'était difficile de formaliser de la géométrie différentielle dans ce truc là. Est-ce que géométrie algébrique c'est plus facile? Euh oui, sauf quand on triche. En géométrie algébrique, souvent on fait des identifications euh canoniques et on fait comme si c'était des égalités. Et en fait, souvent c'est pas des égalités, parfois c'est même pas des identifications canoniques. Donc il y a du travail mais c'est des choses qui se font et ça avance raisonnablement. Est-ce que les risques d'erreur comme ce que vous nous avez montré de collage, elles sont suffisamment peu nombreuses soit tranquille quand on connait une qui fonctionne ou alors euh ça dépend euh quand tu écris un énoncé, tu tu le formalises là il y a un risque. Par contre, si ensuite tu formalises des conséquences de ce théorème pour formaliser des conséquences de ce théorème, tu vas appliquer le théorème que tu as démontré. Et là, si tu as raté son énoncé, en fait, il va pas s'appliquer pour pour démontrer les trucs que tu veux. Donc euh le le vrai test, c'est "Est-ce que ton théorème est applicable pour en déduire des conséquences?" Le jour où il est applicable, euh c'est bon. Mais tant qu'il a pas été appliqué, euh il y a un risque. Question. Il y a eu des grosses migrations sur MATI en 2025. Ça vous a impacté sur votre travail sur les gross ils ont changé les types, ils ont changé. Alors en fait moi je suis un des mainteneurs de Matlib donc quand il y a du quand il y a du travail comme ça à faire, je suis plutôt du côté de ceux qui le font et euh et je le fais parce que je pense que c'est important. Donc en fait Line c'est un truc qui est pas qui qui est pas un produit fini. dans ce sens, il est beaucoup moins mû que rock mais il est en train d'évoluer en permanence. Et euh donc du point de vue du logiciel, c'est plutôt des améliorations. N'empêche que nous à chaque fois on paye les pota cassé et donc bah on répare MAT libéral une fois qu'on a fait les réparations, bah c'est on on se rend compte que c'est mieux et qu'ils ont eu raison de faire les modifications au-dessus. Donc c'est en évolution constante mais plutôt dans la bonne direction. Donc c'est c'est plutôt bon signe. Il y a-t-il d'autres questions? Sinon, je propose qu'on remercier