Sortie du Frido pour les Matheux

Posté par  (site web personnel) . Édité par BAud, patrick_g, Ysabeau 🧶, Benoît Sibaud, cg et ochukoevidence. Modéré par Ysabeau 🧶. Licence CC By‑SA.
Étiquettes :
63
18
sept.
2023
Science

Le Frido est un livre libre de mathématique libre. L’objectif est de partir de la théorie des ensembles (acceptée avec le lemme de Zorn), et d’aller jusqu’au niveau de début du master en faisant toutes les étapes. Pas pour les enfants.

Anciennement pour l’agrégation

Au départ, le Frido était construit comme une complétion d’une liste de développements pour l’agrégation de mathématiques pour la relation de « si un résultat démontré s’appuie sur un autre, alors l’autre est démontré ».

Après quelques années, il faut bien avouer que cet objectif est en passe d’être atteint… ou pas.

D’une part, le nombre de trous commence à bien s’aménuiser. Il reste relativement peu de résultats énoncés non démontrés (de quoi encore m’occuper quelques années cependant).

Mais, d’autre part, l’aspect « agrégation » commence à devenir tout relatif. D’une part, je n’ai pas du tout suivi les changements de programme, et, d’autre part, les parties hors programme deviennent nombreuses, longues et dures bien faites.

Nouveautés 2023

Théorème de Jordan

Le théorème de Jordan en version continue est complètement démontré en suivant presque pas à pas ce très bon document de Quayle et le Gruiec.

D’ailleurs si quelqu’un peut répondre à cette question à propos de la frontière, ce serait très bien.

Tenseurs d’applications multilinéaires

Il est démontré que l’espace vectoriel des applications multilinéaires de VxW vers R est un produit tensoriel de V par W (vérifie la propriété universelle).

Pas mal de choses sont faites entre les vecteurs, les formes, et le produit extérieur.

Énorme relecture

Quentin Guyot, un lecteur de LinuxFr.org, a fait une gigantesque relecture. Juste pour donner un ordre de grandeur du nombre de typos qu’il a trouvées, sachez que ça majore le castor affairé à 4 états — j’en ai compté 1834.

De ces typos, une trentaine ont rejoint l’erratum. L’erratum regroupe les fautes suffisamment graves pour ruiner une démonstration, rendre un énoncé faux, et dont la résolution n’est pas évidente.

Contribution

Donner des démonstrations

Si vous voulez m’envoyer une démonstration à inclure, n’hésitez pas. Une façon facile de le faire est de m’envoyer par mail une photo d’une démonstration écrite à la main. Il y a des moyens plus sophistiqués ; je vous fais confiance.

Algèbre

Je suis en train d’essayer de créer une liste des phrases (vraies) de la forme

« Tout anneau A est B »

avec A et B pouvant prendre leurs valeurs dans la liste « principal », « euclidien », « intègre », « noetherien », et « factoriel ».

Et aussi les phrases de la forme

« Dans un anneau A, tout élément X est Y. »

où X et Y prennent leurs valeurs dans « irréductible » et « premier ».

Ce que j’ai pour l’instant est dans l’index thématique, thème 6 « anneaux », vers la page 5.

S’il m’en manque, n’hésitez pas à m’envoyer les énoncés avec leurs démonstrations.

Développements d’agrégation

Il y a, au bout du Frido, une vieille liste de développements possible par leçon ; elle n’est pas du tout à jour. N’hésitez pas à m’envoyer des listes de théorèmes par leçon. Donnez-moi les théorèmes sous forme de label dans le Frido.

Si un résultat vraiment intéressant manque dans le Frido, envoyez-moi un énoncé et une preuve.

Plans de leçons

Le règlement est très clair là-dessus, sans doute pour éviter ce genre de plaisanteries. Pas de plans.

Quelques réflexions sur le règlement de l’agrégation

Voici une partie que j’aime bien :

Seuls sont autorisés les ouvrages […] jouissant d’un minimum de diffusion commerciale. […] Cette restriction est motivée par le principe d’égalité des candidats : les ressources documentaires autorisées doivent être facilement accessibles à tout candidat au concours.

(le gras est de moi et les parties coupées parlent d’ISBN)

Les livres qui ne sont plus en vente sont donc interdits. Non, la possibilité d’en trouver certains dans des bibliothèques ou en seconde main ne permet pas à un livre non vendu d’être facilement accessible à tous les candidats.

Quid de l’équité financière ? Sortir des centaines d’euros de la poche n’est certainement pas facile pour tous les candidats. Beaucoup de livres commerciaux (exemple) seraient également interdits. On ne peut pas raisonnablement croire que tous les candidats peuvent facilement claquer 28 euros rien que pour les distributions et les équations différentielles.

Bref, c’est certainement une bonne idée de mettre l’équité entre les candidats au centre de la politique livresque. Par contre, je ne suis pas très sûr que compter sur l’achat de livres neufs pour la garantir soit une bonne idée.

Le Frido est libre au sens de la licence FDL (source LaTeX). Vous pouvez le télécharger et l’imprimer vous-même. Par contre le règlement de l’agrégation interdit explicitement les livres imprimés chez vous, et même par les bibliothèques universitaires.

Et voici donc ma transition vers…

Vente

Suivez le lien pour l’achat du premier volume. Le tout coûte 107 euros plus les frais d’envoi. Je précise que c’est uniquement le prix de l’imprimeur. Moi, je ne prends rien.

Si vous êtes capables de l’imprimer pour moins cher, n’hésitez pas, la licence FDL est là pour ça.

Aller plus loin

  • # Les fans de LISP en syncope

    Posté par  (site web personnel) . Évalué à 5.

    Merci de fermer la parenthèse ouverte avec « (acceptée » dans le premier paragraphe, ça me file des démangeaisons ☺.
    En plus cet oubli est visible depuis le résumé visible de la page d'accueil. À quand une alerte « attention aux parenthésosensibles » ?

  • # Typos, erreurs et preuves

    Posté par  . Évalué à 1.

    J'ai entendu parler d'initiatives telles que lean qui prétendent permettre une preuve validée par l'ordinateur.
    Est-ce que tu as entendu parler de ce genre d'outils ?
    Est-ce que ça pourrait faire une entrée progressive dans un ouvrage déjà énorme tel que le frido ? (Tant d'un point de vue théorique que pratique.)

    • [^] # Re: Typos, erreurs et preuves

      Posté par  (site web personnel, Mastodon) . Évalué à 3.

      Je verrais plutôt, pour cet aspect, notre 🐓…

      “It is seldom that liberty of any kind is lost all at once.” ― David Hume

    • [^] # Re: Typos, erreurs et preuves

      Posté par  (site web personnel) . Évalué à 3.

      Il y a une minuscule partie nommée "Languages" à la fin. J'imagine que c'est un embryon de ce qu'il faudrait pour parler de preuves.

      Personnellement, je n'ai rien contre que quelqu'un rédige quelque chose.

      Par contre, la politique du Frido est que tous les résultats intermédiaires doivent être démontrés --- ou au moins énoncés précisément avec un lien vers une preuve disponible en ligne. Et les mots intervenant dans un énoncé doivent être définis, et si une définition fait intervenir un théorème (genre un 'foobar bleuté' est l'unique foobar à être vert), etc. C'est récursif.

      • [^] # Re: Typos, erreurs et preuves

        Posté par  . Évalué à 5.

        Je pense qu’il suggérait que le Frido, vu sa politique justement de tout démontrer, pourrait quasi être réécrit en Lean ou ce type d’assistant de preuve. Ça permettrait notamment de s’assurer qu’il n’y a pas d’erreurs, et de fournir une formalisation des preuves elles mêmes. Ça fait vaguement penser à la démarche de Knuth d’écrire son TeX book en TeX, la partie textuelle serait une documentation des preuves écrites dans une langue formelle.

        Mais c’est un boulot énorme, encore plus que le Frido sans doute vu que l’assistant vient avec son lot de difficultés propres et qu’il est à peu près fini.

      • [^] # Re: Typos, erreurs et preuves

        Posté par  (site web personnel, Mastodon) . Évalué à 0.

        (genre un 'foobar bleuté' est l'unique foobar à être vert)

        Tiens donc, je me demande vraiment d'où tu tires cette expression « foobar bleuté »…

    • [^] # Re: Typos, erreurs et preuves

      Posté par  . Évalué à 3. Dernière modification le 19 septembre 2023 à 13:42.

      Un assistant de preuve (comme lean, coq ou isabelle) n'a pas le même but qu'un manuel de mathématiques.

      Effectivement, dans un assistant de preuve il faut tout démontrer au moindre détail près. Je m'y suis essayé pour (tenter de) formaliser une preuve d'un calcul. Sans doute que je ne m'y suis pas pris de manière optimale (après tout, c'est la première fois que je manipulais un tel outil), mais j'ai vite abandonné après avoir passé plus de 800 lignes sur une partie triviale du calcul qui n'aurait pas méritée 10 lignes sur un article en papier.

      Mais une des choses qu'un assistant de preuve ne fait pas, c'est expliquer une démonstration ; dire quelles étapes sont importantes, dire ce qui relève d'une méthode habituelle, à quel moment on a besoin d'adapter ladite méthode, etc. Alors que c'est justement le boulot d'un manuel de mathématiques.

      Peut-être y-a-t'il des manières pertinentes d'inclure les assistants de preuve dans des manuels de mathématiques. Mais dans l'état actuel des choses, ça ne peut pas remplacer les démonstrations écrites de manières habituelles.

      PS : Le rapport de 80 entre la taille de la démonstration formelle en assistant de preuve et la démonstration papier tiens sans doute au domaine dans lequel elle se plaçait (en plus de mon inexpérience avec l'assistant de preuve). Dans d'autre domaines, une il y aura plutôt un rapport de 2 entre la taille de la démonstration Coq et la démonstration papier.

      • [^] # Re: Typos, erreurs et preuves

        Posté par  . Évalué à 5.

        Il y a plusieurs manières de gérer "l’habitude", soit tu utilises un théorème classique et dans ce cas une fois démontré il est dans une bibliothèque prêt à être utilisé, en principe …

        Soit il y a des "tactiques" connues qui sont codées dans l’assistant de preuve qui permettent de déduire une partie de la démonstration lui même, par exemple https://leanprover-community.github.io/mathlib_docs/tactic/linarith/frontend.html pour démontrer des choses sur des inégalités sans trop se fatiguer en principe …

        Ultimement et avec une bonne connaissance de l’écosystème, le côté "nouveau" ou "inhabituel" pourrait se déduire potentiellement du non emploi de ces techniques ou théorèmes pour démontrer des choses nouvelles. À l’inverse, le besoin de coder des choses triviales ou très connue devrait se réduire avec le temps et les techniques employées se déduire par référence à ce qui est utilisé dans l’écosystème.

        • [^] # Re: Typos, erreurs et preuves

          Posté par  . Évalué à 5. Dernière modification le 20 septembre 2023 à 11:15.

          J'utilisais Isabelle, notamment parce qu'il me semblait le plus avancé en ce qui concerne son interface, ses outils (sledgehammer) et ses bibliothèques (notamment l'intégration, puisque mon but était de calculer une intégrale, même si je ne suis pas arrivé jusque là).

          Bien évidemment, j'utilisais les tactiques de preuves tout le temps, et surtout sledgehammer pour trouver les bonnes combinaisons de tactiques. En relisant de plus près mon code, je me rends compte qu'en fait parfois, ce que je fais en 5-10 lignes pouvait se faire en une ligne que sledgehammer trouvait, sauf que cette ligne pouvait prendre entre 100ms et 1s (et était illisible). Je crois que j'ai essayé de faire quelque chose qui ne mettait pas plusieurs minutes à compiler à chaque fois que j'ouvrais isabelle. Mais même si j'avais utilisé tout le temps les résultats de sledgehammer, aussi illisibles et lents qu'ils aient été, mon fichier aurait quand même fait plusieurs centaines de lignes.

          En détail j'avais une fonction \alpha_{\sigma} définie de la manière suivante:
          - soit \theta une fonction 2\pi périodique qui vaut 1 sur (-\pi,0) et -1 sur (0,\pi)
          - soit q(a,b,a',b') = 3aa' -ab' -a'b -bb'
          - soit \alpha_{\sigma}(t_1,t_2) = q(\theta(t_1-\sigma),\theta(t_2-\sigma),\theta(t_1),\theta(t_2)).

          Le but final était de calculer la fonction F(t,s_1,s_2) = \int_{\Omega_{t-\max(s_1,s_2)}} \phi'(t+t_1-\max(s_1,s_2)) \alpha_{|s_1-s_2|}(t_1,t_2) dt_1dt_2, où \Omega_\tau est un domaine qui dépend du paramètre \tau et \phi une fonction quelconque. Mais comme je l'ai dit, je ne suis pas arrivé jusque là en isabelle.

          Mais sur \alpha_\sigma, voici le genre de choses que je voulais : si 0 <\sigma <\pi et (t_1,t_2) \in (\sigma,\pi)\times(-\pi,0), alors \alpha_\sigma(t_1,t_2) = 4. Pour un humain, c'est facile : regarder ce que valent chacun des \theta(t_1-\sigma), etc., et remplacer leur valeurs dans la définition de q.

          Mais en isabelle, ça a donné: définition de theta (plusieurs lignes parce que j'ai défini un "real_mod x y = y*(x/y - floor(x/y))" pour ce faire), démontrer que c'est 2-pi périodique (une bonne cinquantaine de lignes parce qu'il a bien fallu gérer ce real_mod), démontrer que ça vaut bien -1 sur (0,pi) (-2pi,-pi), etc. et 1 sur les autres intervalles, puis définir alpha (ça ne pose pas de problème), et enfin démontrer que ça vaut bien ce que ça vaut sur (\sigma,\pi)\times(-\pi,0). Et puis sur une vingtaine d'autres rectangles. Et avec moi qui ne voulais pas des lignes à rallonge (en nombre de caractère et en temps d’exécution) que proposait sledgehammer, ça donne 800 lignes.

    • [^] # Re: Typos, erreurs et preuves

      Posté par  . Évalué à 2.

      Bravo au lecteur assidu et attentif qu'est Quentin Guyot.
      Quelle prouesse.

      "Si tous les cons volaient, il ferait nuit" F. Dard

  • # Le prix est de 27.10 Eur sur le site de l'imprimeur...

    Posté par  . Évalué à 0. Dernière modification le 20 septembre 2023 à 10:43.

    …et non 107 euros comme indiqué par Laurent.

    Ce qui rend le Frido tout de suite moins cher.
    Quelqu'un peut-il corriger ?

  • # Commentaire supprimé

    Posté par  . Évalué à 2.

    Ce commentaire a été supprimé par l’équipe de modération.

  • # Merci pour ce pavé

    Posté par  . Évalué à 2.

    avec 2792 pages, il y a de quoi faire en effet. En plus, le pdf ne fait que 13,8 Mo, j'imagine donc qu'il n'y a aucune jolie image en couleur pour détendre/distraire le lecteur.

    Bien qu'ayant été un étudiant assez moyen en Mathématiques, j'ai toujours adoré cette matière et feuilleter le Frido, ça me rappelle plein de bon souvenirs.

    Alors, bravo et merci. Un bel exemple de "libre".

    Question à l'auteur: le Frido couvre-t-il l'ensemble des thèmes susceptibles d'être abordés à l'agrégation ?

    "Si tous les cons volaient, il ferait nuit" F. Dard

    • [^] # Re: Merci pour ce pavé

      Posté par  (site web personnel) . Évalué à 3.

      Question à l'auteur: le Frido couvre-t-il l'ensemble des thèmes susceptibles d'être abordés à l'agrégation ?

      Il y a quelques années, j'aurais répondu «oui». J'ai réussi l'agrégation vers 2013 quand le Frido ne faisait que 700 pages.

      Par contre le temps passant, le programme a changé, et je n'ai pas suivi.

      Du coup, je ne suis pas certain de la proportion du programme qui est couverte. À mon avis c'est quand même pas mal.

  • # L'auteur est fou

    Posté par  . Évalué à 2.

    Merci pour le travail, plus de 2500 pages.

    Ça m'aurait interessé à une époque (même si j'ai jamais étudié les math pures)

  • # Super travail

    Posté par  (site web personnel) . Évalué à 6.

    Comme à chaque nouvelle annonce du Frido, et après 10 minutes passées à feuilleter le livre, je suis toujours aussi admiratif par le travail colossal que tu réalises, en espérant qu'il serve aux jeunes pour qui ces sujets sont encore d'actualité (moi j'ai arrêté les maths en 2000).

    J'apprécie particulièrement que tu illustres certains passages avec Sage.

    "There's no such thing as can't. You always have a choice." - Ken Gor

    • [^] # Re: Super travail

      Posté par  . Évalué à 3.

      Ah ben j'ai arrêté à peu près au même moment aussi avec la fin des études, mais un si bel ouvrage, ça me donne envie de relire (enfin… la partie que je comprenais à l'époque!!)

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.