Le Frido est un livre libre (licence FDL) de mathématique qui reprend l’ensemble de la mathématique depuis la construction des entiers jusqu’à tout ce qu’on peut placer à l’agrégation : probabilités, distributions, anneaux, groupes, géométrique, etc.
Sommaire
Tout en un
Une particularité du Frido est d’être «tout en un». Un seul livre (PDF de 3000 pages) qui contient toutes les matières : algèbres, analyse, probabilités, etc.
L’intérêt est de pouvoir citer les théorèmes d’algèbre linéaire utilisé en analyse, de mesure utilisée en probabilité, etc.
Un enchaînement particulièrement long et interdisciplinaire est la chose suivante.
- Définir une rotation comme composée de deux symétries axiales.
- Définir les fonctions trigonométriques par leurs séries.
- Définir les applications linéaires et leurs matrices associées.
À partir de là, montrer que la matrice d’une rotation a la forme qu’elle a avec ses fonctions trigonométriques.
Nouveautés 2026
Cauchy-Lipschitz analytique
Le gros morceau de cette année est le théorème Cauchy-Lipschitz analytique en passant par Cauchy-Lipschitz holomorphe. Je suis convaincu qu’on peut faire sans passer par les fonctions holomorphes. En cherchant le label THOooZEBOooQJOSQj dans le PDF, vous trouverez une démonstration quasiment complète sans passer par les fonctions holomorphes. À mon avis le bout qu’il manque est juste un peu de combinatoire qui m’échappe. Si vous connaissez des choses à ce propos, n’hésitez pas à répondre à l’une ou l’autre de ces questions qui sont (je crois) équivalentes :
https://math.stackexchange.com/questions/5111835/analytic-map-on-the-banach-x-times-y
https://math.stackexchange.com/questions/5113042/analytic-picard-lindel%C3%B6f-theorem
Note : j’ai déjà demandé à de l’IA sans succès (mais c’était il y a quelque mois). Je n’ai rien contre une démonstration générée par IA, mais comme je l’explique ici, j’ai quelque chose contre « j’ai demandé à l’IA et voici le résultat ». Si vous me proposez une démonstration par IA, soyez sûrs de la comprendre d’un bout à l’autre dans tous les détails. Sinon, ça ne me sert à rien. Quand les IA font des fautes, c’est toujours subtil — et on ne les découvre que via une lecture très attentive de chaque ligne.
Groupe symétrique
Démonstration de la décomposition en cycles des éléments du groupe symétrique.
Problèmes d’ordre
L’ordre des chapitres dans le Frido est l’ordre logique mathématique, et non l’ordre pédagogique. Les théorèmes se démontrent uniquement avec des théorèmes démontrés plus haut. Du point de vue de , les
\ref pointent toujours vers des \label plus haut. C’est une grosse contrainte.
Quelques exemples de dépendances qui m’ont fait déplacer des parties cette année ?
En théorie des groupes, la formule des classes demande les rationnels, les rationnels sont le corps des fractions, donc demande les anneaux.
Le symbole de sommation demande de savoir la décomposition en cycles des permutations (groupe symétrique) pour montrer que la somme ne change pas si on change l’ordre de sommation; la décomposition en cycles demande le théorème de Lagrange qui demande les rationnels et donc les anneaux. Les anneaux demandent le symbole de sommation pour écrire le terme général d’un idéal engendré par une partie.
Il faut donc découper la partie sur les anneaux en plusieurs parties. Quant au symbole de sommation, sa définition est découpée en plusieurs parties en fonction du niveau de généralité.
Tout cela pour dire que le Frido n’est pas arrangé par ordre pédagogique et encore moins par ordre de difficulté. Le principal déterminant à l’ordre et au découpage des chapitres est l’impossibilité de faire des références vers le bas.
Avant 2026, j’étais parvenu à mettre la construction des entiers, rationnels et réels dans le même chapitre avec seulement ce qu’il fallait d’anneaux pour dire que les rationnels sont le corps des fractions des entiers. Maintenant que je me suis rendu compte des boucles de dépendances dont je parle plus haut (parce que j’ai démontré la décomposition en cycles), j’ai décomposé en plus de chapitres.
- entiers relatifs (les naturels sont admis)
- groupes
- anneaux
- rationnels et réels
Partition de l’unité
Il y avait trop d’énoncés différents sans démonstration. Il reste maintenant deux théorèmes : un qui donne une partition de l’unité subordonnée à des ouverts et un autre spécifique dans le cas des compacts. Le deuxième est démontré; la démonstration du premier est dans mon interminable liste de choses à faire.
Neutralité en moyenne
Lorsque je dois écrire «La personne qui lit doit rester attentive», j’écris
\randomGender{Le lecteur}{La lectrice} doit rester \randomGender{attentif}{attentive}.
avec la macro :
\newcounter{rndgendercont}
\newcommand{\randomGender}[2]{%
\setcounter{rndgendercont}{%
\numexpr\value{chapter}+\value{numtho}\relax%
}%
\ifthenelse{\isodd{\value{rndgendercont}}}{#1}{#2}%
}
En gros, ça donne masculin ou féminin au hasard. Plus précisément, ça donnera masculin si la somme entre le numéro du chapitre et le numéro du dernier théorème énoncé est pair et féminin si impair.
La nouveauté 2026 est de faire « chapitre+théorème ». Avant, je faisais « numéro de page+théorème », et j’ai eu des problèmes avec une phrase qui passait d’une page à une autre—et donc une incohérence entre deux appels à randomGender.
Indépendance de variables aléatoires
Définition de l’indépendance d’une famille quelconque d’évènements. Définition d’un -système et lien avec l’indépendance de tribus.
Algèbre
… rien cette année. Étonnamment, cette année, aucun énoncé supplémentaire de la forme «Dans un anneau XXXX, tout élément/idéal YYYY est ZZZZ» n’a été démontré.
Pourtant je suis certain qu’il y en a encore plein qui manquent.
LaTeX et encodage
On a discuté de l’encodage des accents dans les URL.
L’objectif aurait été de faire fonctionner une macro \myurl permettant d’écrire
\myurl{https://fr.wikipedia.org/wiki/Idéal_premier}
Et franchement, ça n’a pas été un succès.
J’ai déjà fait des choses comme
\documentclass[a4paper,11pt]{book}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{hyperref}
\usepackage{xstring}
% Encode certains caractères UTF-8 pour l’URL
\newcommand{\MakeUTFPerCent}[1]{%
\def\result{#1}%
\StrSubstitute{\result}{é}{\%C3\%A9}[\result]%
\StrSubstitute{\result}{à}{\%C3\%A0}[\result]%
\StrSubstitute{\result}{è}{\%C3\%A8}[\result]%
\StrSubstitute{\result}{_}{\%5F}[\result]%
}
% Macro finale
\newcommand{\myurl}[1]{%
\MakeUTFPerCent{#1}%
\href{\result}{#1}%
}
\begin{document}
Lien encodé : \myurl{https://fr.wikipedia.org/wiki/Idéal_premier}
\end{document}
Mais rien ne marche. Et j’en profite pour noter que chatGPT est nettement moins bon en LaTeX qu’en math ou en python.
luatex
Donc passage à LuaTeX, et ça a été assez facile.
- temps de compilation plus long
- texte raccourci : au moment du passage à LuaTeX je suis passé d’environ 3050 à 2775 pages.
Très peu de changements :
-\documentclass[a4paper,twoside,11pt]{book}
+\documentclass[french]{book}
+\RequirePackage{luatex85} % Pour xy (voir https://tex.stackexchange.com/questions/328602/lualatex-and-xypic)
et
-\usepackage{listingsutf8}
+\usepackage{listings}
Passage à 5 volumes
Comme à chaque mois de septembre, une version figée est commercialisée pour celles qui voudraient avoir du papier (et aussi parce que la dernière fois que j’ai lu le règlement de l’agrégation, la commercialisation était obligatoire).
Le nombre maximum de pages étant de 750 par volume, le nombre total de page étant de 2872, j’ai dû passer à 5 volumes. Et c’est là que je suis content d’avoir dès le départ, dans mes scripts, mis le nombre de volumes en variable.
Laurent est un pédant
Je suis un insupportable pédant. Et je propose même de fonder un club. Dans des discussions non mathématiques sur LinuxFr.org je suis parvenu à me fritter à propos (au moins) de l’utilisation correcte de
- novlang
- exponentielle. Plusieurs fois.
- Pluton — mais là le troll n’a pas pris. On ne peut pas toujours gagner.
Le Frido aussi est un peu pédant par exemple si est un polynôme, il est démontré que
. On pourrait croire que c’est seulement une notation, mais non. C’est un théorème.
Le Frido démontre aussi que si on induit la topologie de vers le cercle et qu’on construit la tribu de Lebesgue à partir de là (boréliens, complétion), on obtient la même tribu que si on induit directement la tribu de Lebesgue de
vers le cercle. C’est important pour prouver des isomorphismes d’espaces de Lebesgue
avec
.
À part ça, le Frido est un pédant de notations. J’ai horreur des abus de notations, et je prétends que la formule d’Euler ne contient pas le nombre
.
L’Humanité
L’Humanité a publié un article sur le Frido. Encore un en 2027 et le Frido rentre dans des critères d’admissibilité de Wikipédia :).
Aller plus loin
- Ma page perso sur le Frido (251 clics)
- Achat du premier volume (106 clics)
- Les sources LaTeX (75 clics)

# Règlement
Posté par Colin Pitrat (site web personnel) . Évalué à 6 (+4/-0).
Il n'est dit nul part dans le règlement que les notes personnelles du candidat sont interdites. Ce sont les notes personnelles en général. Ce qui paraît logique, si un copain et moi on prend chacun des notes et on se les échange, ce n'est pas autorisé.
Donc selon mon interprétation, si le Frido, ce sont tes notes personnelles, il est interdit pour tout le monde.
Mais je ne pense pas que le Frido rentre dans la catégorie des notes personnelles, justement parce qu'il est édité et publié.
D'ici à dire qu'il "suffirait" à un candidat qui veut prendre ses notes personnelles de leur coller un numéro ISBN et de les mettre en vente quelque part au format papier, il n'y a qu'un pas, que je franchis allègrement.
[^] # Re: Règlement
Posté par LaurentClaessens (site web personnel) . Évalué à 8 (+6/-0).
Question délicate.
La première fois que j'ai tenté l'agreg, il fallait juste un ISBN, je l'ai ajouté à mes notes (qui étaient déjà publiées sur internet, licence FDL), et je les ai utilisé.
À l'époque, un certain nombre de personnes m'ont accusé d'avoir triché. Disons que j'ai trouvé une faille dans le règlement; la faille étant de faire du semblant de croire que la personne ayant rédigé le règlement était sincère en disant que l'objectif était d'avoir des sources les plus accessibles possibles au plus grand nombre.
Quand j'ai repassé l'agreg l'année d'après, le règlement a changé—changé en avril pour la session de juin; je l'ai encore au travers de la gorge.
La raison officielle est que trop de monde avait suivit mon exemple et avait mis des ISBN sur n'importe quoi.
Du coup, le règlement a ajouté
«
jouissant d’un minimum de diffusion commerciale
»
Donc je commercialise le Frido pour satisfaire (très superficiellement) ce critère.
Mais qu'entends le jury par "un minium" ?
10 exemplaires ? 500 ?
je suis prêt à parier que si je me présentais à nouveau, une précision ad hoc serait ajoutée pour exclure le Frido.
De toutes façons, ce règlement n'est pas destiné à être appliqué.
Quelques preuves :
la phrase «Seuls sont autorisés les ouvrages avec un numéro ISBN et jouissant d’un minimum de diffusion commerciale. » est écrite au présent. En principe les livres qui ne sont plus édités sont interdits. Ah ah la bonne blague.
Et ils en rajoutent une couche pour interdire les ouvrages qui ne sont plus édités : «les ressources documentaires autorisées doivent être facilement accessibles à tout candidat au concours.» Clairement les livres qui ne sont plus édités ne sont pas facilement accessibles à tous les candidats, même si ils sont disponibles dans quelques bibliothèques universitaires.
À mon avis, ce règlement a été écrit vite fait pour parer au plus pressé :
Apparemment ça a marché parce que, si beaucoup de monde a fait le coup de l'ISBN, peu de monde aura fait le coup de la commercialisation en auto-édition.
Une étoile pour celui-ci qui est presque certainement exactement ce que le jury avait le plus envie d'interdire (avec raison). Il coûte 0.07 euro par page contre 0.04 pour le Frido.
[^] # Re: Règlement
Posté par Luc-Skywalker . Évalué à 3 (+1/-0).
Comme une grosse arête quoi !
Bravo pour la persévérance. A tous les niveaux ;)
Tu es dessus depuis quand ?
"Si tous les cons volaient, il ferait nuit" F. Dard
[^] # Re: Règlement
Posté par orfenor . Évalué à 3 (+1/-0).
ça fait au moins 10 ans qu'il publie le Frido (cf le tag Frido sur la dépêche)
[^] # Re: Règlement
Posté par LaurentClaessens (site web personnel) . Évalué à 3 (+1/-0).
Les plus vieux morceaux proviennent de TP que j'ai donné à l'université de Bruxelles en 2006.
# Nombre de Fridos valides
Posté par Liorel . Évalué à 5 (+3/-0).
Je me suis souvent demandé, à partir de la règle qui te pose des problèmes d'ordre, s'il existait plus d'un Frido valide.
Pour être plus précis : Appelons Frido une liste ordonnée de tous les énoncés contenus dans le Frido. Appelons Frido valide un Frido dont chaque énoncé est démontrable uniquement en se basant sur antérieurs (par ordre d'apparition). Combien y a-t-il de Fridos valides ?
Ça, ce sont les sources. Le mouton que tu veux est dedans.
[^] # Re: Nombre de Fridos valides
Posté par jch . Évalué à 5 (+4/-0).
Oui. C'est la propriété qui dit qu'un tri topologique produit un ordre total compatible avec (l'ordre partiel induit par) le graphe de départ si et seulement si le graphe était acyclique.
Non. Il se pourrait qu'il n'y ait pas de cycle à 2, mais qu'il y ait un cycle à n > 2.
[^] # Re: Nombre de Fridos valides
Posté par Liorel . Évalué à 3 (+1/-0).
Je me suis mal exprimé, mais tu as compris ma question. Pour moi, "A se démontre à partir de B" n'implique pas "A se démontre à partir de B sans aucun résultat intermédiaire". Dans une relation du type A > B > C, C se démontre à partir de A (l'ordre est transitif).
Et c'est amusant que tu amènes des graphes dans la discussion, j'étais justement tenté d'exprimer ma question en termes de graphes acycliques orientés, et puis j'y ai renoncé en me disant que ça allait amener plus de confusion que de clarté :)
Ça, ce sont les sources. Le mouton que tu veux est dedans.
[^] # Re: Nombre de Fridos valides
Posté par jch . Évalué à 6 (+5/-0).
Oui. J'ai essayé d'être aussi pédant que possible, en hommage à Laurent.
[^] # Re: Nombre de Fridos valides
Posté par LaurentClaessens (site web personnel) . Évalué à 3 (+1/-0).
Il n'y a pas de cycles du tout. Sinon ce serait incohérent.
Pour vérifier qu'il n'y ait pas de cycles, j'ai un script qui lis les sources LaTeX, repère les
\refet\eqrefet qui trouve les\labelcorrespondant. Il vérifie que le label est bien au-dessus de la référence.Ce faisant, on ne peut pas faire une découpe en chapitre naïve
Entre autres parce que les rationnels sont définis comme étant le corps des fractions des entiers.
Limitation de ma garantie
Quand je dis «il n'y a pas de cycles», c'est garanti par un script qui parcours les
refetlabel. C'est pour ça que je mets plein deref.Mais si un théorème utilise un théorème sans faire un
refexplicite, la garantie ne tient plus.Même chose pour les théorèmes qui ne sont pas encore démontrés. Parfois je suis obligé de déplacer un théorème au moment de le démontrer.
[^] # Re: Nombre de Fridos valides
Posté par jch . Évalué à 3 (+2/-0).
Ce ne serait pas bien fondé, mais il se pourrait que ça reste cohérent.
[^] # Re: Nombre de Fridos valides
Posté par Gil Cot ✔ (site web personnel, Mastodon) . Évalué à 3 (+1/-0).
Et si l’on veut visualiser graphiquement la chose, je découvre aujourd’hui qu’il y a une extension vibe-codée pas encore dans l’archive :o
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
[^] # Re: Nombre de Fridos valides
Posté par Gil Cot ✔ (site web personnel, Mastodon) . Évalué à 2 (+0/-0). Dernière modification le 08 octobre 2026 à 15:31.
le lendemain (6 octobre)…
Après, je me demande si pour un pavé1 comme le Frido si un tel graphe sera lisible.
Au dessus du pavé, quel mot utiliserez-vous pour un tel volume ? Un caisson ? ↩
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
[^] # Re: Nombre de Fridos valides
Posté par LaurentClaessens (site web personnel) . Évalué à 3 (+1/-0).
La proposition "il y en a 0 de valide" serait équivalente à "ZFC est incohérent".
Il y en a à priori plein de valides.
Par exemple la proposition 19.156 dans le volume 3 parle de prolongement continu d'une fonction définie sur une partie dense.
Cette proposition est dans le chapitre 19, mais ne dépend que de choses qui sont dans le chapitre 12. Il peut donc être déplacé n'importe où (au moins) dans les chapitres 13, 14, 15, 16, 17 ou 18.
[^] # Re: Nombre de Fridos valides
Posté par jch . Évalué à 3 (+2/-0).
C'est une affirmation très forte. Tu peux nous donner une idée de preuve ?
[^] # Re: Nombre de Fridos valides
Posté par LaurentClaessens (site web personnel) . Évalué à 5 (+3/-0).
Dire qu'il y a zéro Frido valide signifie (si j'ai bien compris le concept) qu'il existe zéro démonstrations valides tout court parce que les démonstration avec cycles ne sont pas valides.
Je ne sais pas comment on appelle un système d'axiome dans lequel aucune preuve n'est valide, mais le mot "incohérent" m'a l'air de convenir …
(en mode je parle de ce que je ne connais pas)
[^] # Re: Nombre de Fridos valides
Posté par Liorel . Évalué à 2 (+0/-0).
On peut trouver un cycle sans supposer que tout ZFC est incohérente. Soient A, B, C, D des énoncés, notons < la relation "requiert pour être démontré".
Alors si on a A < B < C < D et B < A, on est :
Dans la mesure où un Frido valide nécessite tous les énoncés contenus dans le Frido de référence, il suffit qu'un seul énoncé nécessite un cycle pour qu'il y ait 0 Frido valide. Ça n'implique pas que ZFC est incohérente, juste un énoncé faux.
Cette réflexion en amène une autre : si on considère l'ensemble des énoncés du Frido muni de la relation "requiert pour être démontré", le Frido est-il un arbre orienté ? Autrement dit, est-il connexe et acyclique ? La propriété d'acyclimse a déjà été discutée, mais le Frido est-il connexe ? Il n'est certainement pas fortement connexe, et très vraisemblablement pas unilatéralement connexe1, mais est-il faiblement connexe ? Et si le Frido est un arbre, je serais curieux de savoir quelle proportion des énoncés sont des feuilles et quelle proportion sont nécessaires à au moins une démonstration.
S'il était unilatéralement connexe, alors il existerait un énoncé dans le Frido permettant de redémontrer tout le Frido sans faire aucun autre postulat. Ça me semble excessivement exigeant. ↩
Ça, ce sont les sources. Le mouton que tu veux est dedans.
[^] # Re: Nombre de Fridos valides
Posté par LaurentClaessens (site web personnel) . Évalué à 3 (+1/-0).
Je propose d'affaiblir la relation
À la place je vais prendre la relation A>B si la démonstration donnée dans le Frido pour A utilise B.
La raison est qu'il y a des paires de résultats A,B pour lesquels il faut démontrer A ou B (au choix) à la dure, et ensuite l'autre est facile. Ex : l'inversion locale et la fonction implicite.
Ainsi, le Frio est connexe parce que tout pointe in fine sur de la théorie des ensembles. Je serais étonné qu'un seul résultat n'utilise pas par exemple (A u B) u C = A u (B u C).
Le Frido a plusieurs "racines" c'est à dire théorèmes non démontrés et pour lesquels je n'ai pas d'intention d'en donner :
Le graphe est orienté (forcément). Il est acyclique (en tout cas c'est l'intention) parce qu'un cycle serait
A<B<A
qui signifierait que la démonstration de B cite A mais que la démonstration de A cite B.
Trouver les feuilles
En théorie, c'est simple : un bon
greptrouve les\label{foobar}qui n'ont aucun\ref{foobar}correspondant.Le cas de la géométrie affine.
Je ne me cache pas de trouver la géométrie affine complètement idiote.
J'ai d'ailleurs un projet dans le Frido est de faire en sorte qu'aucun
\refne pointe vers l'intérieur du chapitre sur les espaces affines.Cela prouverait que l'ensemble du chapitre ne sert à rien.
D'ailleurs je ne comprends même pas comment il serait possible d'écrire un énoncé quelconque qui puisse se démontrer en passant par les espaces affines, mais qui ne puisse pas être démontré juste avec les espaces vectoriels.
Problème de LaTeX/python
Pour étudier ce genre de questions, ça fait longtemps que j'ai en tête d'écrire un script qui détecte la structure
Et d'étudier les
\refdansproof.[^] # Re: Nombre de Fridos valides
Posté par kantien . Évalué à 3 (+1/-0). Dernière modification le 26 septembre 2026 à 18:32.
Le problème de Laurent est plus simple, comme il te l'a expliqué dans le commentaire auquel il te répond.
Comme on est sur un forum d'informatique, je vais faire une analogie avec les stratégies de typage et de définition de variables dans un langage de programmation (le problème est le même, mais n'est pas lié à des problèmes de cohérence de théorie).
Son problème est le même que l'exemple illustré ci-dessous en OCaml :
Ici, je veux utiliser
fooavant de l'avoir introduit dans l'environnement, le compilateur rejette le code. Je dois en intervertir l'ordre :Mais c'est un choix de design, le langage Haskell, par exemple, aurait accepté mon premier exemple.On peut y utiliser une fonction (qui n'est qu'un theorème pour moi) avant même de l'avoir défini (ou de l'avoir prouvé, ce qui est la même chose). Mais un tel choix complique le code du type checker et les erreurs de typage peuvent apparaître après que le celui-ci est effectué un travail qui s'avère inutile. Que ce soit en Haskell ou OCaml, le travail du type checker est le même que celui du noyau d'un assistant de preuves comme Rocq ou Lean : vérifier que les preuves (fonctions) sont formellement correctes.
Maintenant, revenons au problème de Laurent. Il fait de la programmation générique : au lieu de définir directement les fractions, il passe par le corps des fractions sur l'anneau des entiers.Il expose une théorie générale qu'il applique à un cas particulier : c'est de la programmation générique, c'est, par exemple, ce que font Haskell avec les type classes et Rust avec les traits. Mais, il pourrait directement développer la construction sur Z pour définir Q, sans passer par la construction générique : c'est par exemple ce que fait le compilateur Rust en monomorphisant tout usage de Traits, c'est un cas particulier d'inlining. Pourquoi il fait ce choix ? Sans doute par soucis de factorisation en appliquant le principe DRY, mais cela à une incidence sur l'ordre dans lequel il doit introduire ses concepts et ses constructions.
Illustration avec du code OCaml. Je pourrais écrire le code du polynôme
X² + X + 1sur les entiers, ainsi :Mais je me retrouve avec une fonction monomorphe. Si je veux le définir sur un autre anneau, il faut que recommence le travail : c'est rébarbatif. J'expose donc le concept d'anneau et je définis ce polynôme sur un anneau quelconque.
C'est exactement ce que fait Laurent, mais au lieu de définir un polynôme générique en faisant abstraction de l'anneau particulier, il expose la construction du corps des fractions, construction générique dont il se sert pour définir les rationnels à partir de l'anneau des entiers relatifs. Mais il aurait très bien pu se passer de la construction générique, comme pour mon premier polynôme, et faire comme Jean Dieudonné dans Pour l'honneur de l'esprit humain (livre dont je conseille la lecture pour toute personne intéressée par les mathématiques, il en a fait la promotion à l'époque chez Pivot).
Ce que j'ai écrit en OCaml est exactement ce que font Haskell et Rust avec les type classes et les Traits. La différence est qu'à l'instanciation du polynôme, il n'est pas nécessaires de passer explicitement l'anneau comme paramètre : il est déduit automatiquement par le compilateur à partir du type du paramètre. Cela est possible car, dans ses langages, pour une structure algébrique et un type donnés, on ne peut en définir qu'une seule : la structure canonique; il n'y a alors pas d'ambiguïté sur la structure à passer en paramètre. C'est la seule manière raisonnable d'implémenter ce que l'on appelle la surcharge d'opérateur mais, malheureusement, la plupart des langages n'imitent pas Haskell ou Rust en la matière (que l'on ne me parle pas de POO, ici on fait des mathématiques et de la logique avec un minimum de sérieux).
Enfin, tout cela pour dire que le problème de Laurent n'a pas grand chose à voir avec des soucis de cohérence logique, voir de contradiction dans ZFC.
Maintenant, on va vraiment parler de logique mathématique et devenir quelque peu pédant pour faire honneur à Laurent. Je vais éviter de rentrer dans la distinction entre prouvable et vrai, les nuances entre syntaxe et sémantique, ce serait trop pédant. En revanche, sache que ton idée d'ordre est on ne peut plus connue et étudiée dans le domaine de la logique mathématique : c'est l'algèbre de Lindenbaum - Tarski. C'est une relation d'ordre sur les classes d'énoncés logiquement équivalents définit comme tu le souhaites : la classe de A est plus petite que celle de B si on peut prouver B avec A comme hypothèse. J'ai rapidement survolé la page de Wikipédia, elle m'a l'air bien faite. Mais je pourrais développer si certains le souhaite : treillis, algèbre de Heyting (pour la logique intuitionniste), algèbre de Boole (pour la logique classique), topologie et théorème de représentation de Stone, et le lien avec la méthode du forcing pour prouver des énoncés de consistance relative dans ZFC (là il faudrait vraiment distinguer syntaxe et sémantique, prouvable et vrai), catégorie cartésienne fermée (si on n'efface la différence entre les preuves dans la structure d'ordre) et correspondance entre preuves et programmes. Néanmoins je ne sais jusqu'à quel point ces notions sont au programme de l'agrégation (Laurent si tu peux me le dire).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Nombre de Fridos valides
Posté par jch . Évalué à 1 (+0/-0).
D'après ce que j'ai compris, ça voudrait dire qu'il y a un cycle dans les références entre propriétés. Ça voudrait dire que les preuves du Frido ne seraient pas bien fondées, mais ça n'impliquerait pas que les propriétés soient fausses (il se pourrait qu'il existe des preuves bien fondées des mêmes propriétés).
Si ma mémoire est bonne, incohérent, ça veut dire qu'il démontre une propriété et sa négation (et par conséquent qu'il démontre toute propriété).
Pareil :-)
# LaTeX
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Tu as essayé «
unicode=True» comme option au chargement de hyperref ?Personnellement je n'ai jamais eu de soucis d'encodage avec hyperref et avec des macros maison.
En revanche j'ai longtemps eu des soucis avec hyperref et des macros maison pour le traitement de certains caractères dans les URL (notamment # et _). Récemment j'en ai eu marre et je m'y suis penché. Je pense avoir résolu mon soucis avec la déclaration suivante :
(Oui bon là ça fait rien de spécial mais c'est pour montrer ; l'idée étant que la lectrice peut adapter la définition de \mylink@ à son bon gré.)
Adhérer à l'April, ça vous tente ?
[^] # Re: LaTeX
Posté par LaurentClaessens (site web personnel) . Évalué à 2 (+0/-0).
J'avoue ne plus savoir ce que j'ai testé :)
Par contre, je suis un peu lassé de programmer en LaTeX.
LuaTeX fonctionne très bien, je ne vais pas me replonger dans les arcanes de LaTeX pour la beauté du geste. Je laisse ça aux plus jeunes que moi.
À la limite, je suis preneur d'une fonction clef en main. Et encore, il faudrait que le retour de LuaTex à LaTeX m'apporte quelque chose.
[^] # Re: LaTeX
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Adhérer à l'April, ça vous tente ?
[^] # Re: LaTeX
Posté par LaurentClaessens (site web personnel) . Évalué à 2 (+0/-0).
pas au point de me remotiver à toucher à un
\makeatletter. C'est au-dessus de mes forces.[^] # Re: LaTeX
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Je pense qu'il ne te manque que «
unicode=True» comme option au chargement de hyperref.Adhérer à l'April, ça vous tente ?
[^] # Re: LaTeX
Posté par LaurentClaessens (site web personnel) . Évalué à 2 (+0/-0).
Presque.
Exemple minimum :
Compilé avec
pdflatex exemple.tex.Le pdf affiche:
https://fr.wikipedia.org/wiki/Idal_premier(notez le
émanquant)Par contre, quand on clique dessus on arrive bien sur
https://fr.wikipedia.org/wiki/Idéal_premieravec l'accent.Mais mais mais …
Si j'enlève
[unicode=True]c'est exactement la même chose sur cet exemple.[^] # Re: LaTeX
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Je pense qu'il manque ce qui suit à ton exemple pour à minima retrouver le contexte d'encodage du frido :
Adhérer à l'April, ça vous tente ?
[^] # Re: LaTeX
Posté par Pol' uX (site web personnel) . Évalué à 3 (+1/-0).
Non, au temps pour moi. J'ai installé LaTeX pour reproduire ton bug et il est tenace. :)
Adhérer à l'April, ça vous tente ?
# L'IA parlons en
Posté par Funix (site web personnel, Mastodon) . Évalué à 7 (+5/-0).
Tu as fait mention à l'IA mais à la lecture de cet article où Cédric Villani se montre très négatif à son sujet, en tant que mathématicien tu penses aussi que c'est une catastrophe ou une fantastique opportunité pour aller plus loin dans la recherche ?
https://www.funix.org mettez un manchot dans votre PC
[^] # Re: L'IA parlons en
Posté par LaurentClaessens (site web personnel) . Évalué à 9 (+7/-0).
Je ne suis pas mathématicien—en tout cas pas payé pour faire de la recherche.
Il y aurait beaucoup de choses à dire sur l'IA en math.
En vrac.
Il semble y avoir consensus sur le fait que le mécanisme d'évaluation des promotions par
bibliométrie est mort. N'importe qui peut maintenant faire 20 articles corrects par an.
Cet article fait une proposition intéressante : les articles doivent être évalués par les concepts nouveaux qu'ils introduisent, pas sur le théorème central ou la difficulté de la preuve.
Il pourrait y avoir besoin de moins de mathématiciens pour avancer à la même vitesse. Pour moi c'est pas un problème.
Il faudra sérieusement revoir le mécanisme de revue des articles par les pairs, parce qu'on va droit à la surproduction.
À propos de surproduction, introduire de l'IA pour accélérer la partie de la recherche où n'est pas le goulot d'étranglement n'accélère pas la recherche.
De toutes façons, ce sont les humains qui décident ce qui est intéressant.
La partie "historique" de la mathématique, c'est à dire répondre à des questions de physique reste. L'IA ne peut pas prévoir si les ondes gravitationnelles détectées par LISA vont ou non respecter les équations d'Einstein.
Beaucoup de mathématiciens expliquent que l’intérêt d'un grand théorème est plus le cheminement qui mène à la preuve que la réponse. C'est à dire que, en cherchant une preuve, on développe des nouvelles idées. C'est ça qui fait vivre la mathématique.
Ceux du point (8) ont raison.
Le point (9) n'est pas un problème : les mathématiciens devront trouver d'autres motivations pour trouver des nouvelles questions.
Les doctorants aujourd'hui demandent à l'IA et utilisent des théorèmes sans les avoir vérifié dans la littérature.
Certains mathématiciens s'en plaignent et pleurnichent que la recherche documentaire dans les livres est quelque chose que les doctorants devraient savoir faire.
Ah … les points 11 et 12 sont ma marotte.
Jusqu'à il y a quelques années, on pouvait dire «tu dois apprendre à aller voir dans les livres, de toutes façons t'as pas le choix : les mathématiciens ont écrit leurs savoir dans des livres qui ne sont pas disponibles sur internet et dont la photocopie est interdite».
Ce discours était déjà scandaleux depuis des décennies, mais aujourd'hui il devient inaudible. L'IA a eu accès à ces livres et peut en redonner le contenu.
C'est d'ailleurs comme ça que j'ai pu démontrer Cauchy-Lipschitz holomorphe et analytique alors que je n'ai même pas trouvé d'énoncé sur internet. L'IA a certainement lu des livres contenant ces théorèmes.
[^] # Re: L'IA parlons en
Posté par LaurentClaessens (site web personnel) . Évalué à 5 (+3/-0).
J'oubliais un autre point.
Pour l'instant, il semble que les IA n'introduisent pas de nouveaux concepts. Elles arrivent à utiliser de façon optimale les mathématiques qui existent déjà.
Autrement dit, les IA explorent l'enveloppe convexe de la mathématique déjà existante.
À l'heure de l'IA, l'intérêt d'un article doit être de proposer des choses qui sortent de cette enveloppe.
Cela rejoint le point (2).
De même, comme démontrer des choses devient automatique, la plus value humaine à la mathématique est de faire le tri entre les résultats (vrais) qui nous intéressent et ceux qui ne nous intéressent pas.
Aucune IA n'aurait pu prédire que la suite kangourou aurait pu intéresser quelqu'un. Il faut vraiment être humain pour avoir envie d'y réfléchir.
Peut être que l'unité de publication mathématique devient le livre au lieu de l'article. Une publication valable serait «voici un nouvel objet, voici des lemmes pas intéressants mais qui vont servir—et voici le résultat intéressant»
[^] # Re: L'IA parlons en
Posté par bbo . Évalué à 4 (+3/-1). Dernière modification le 23 septembre 2026 à 10:06.
Ça sera même plutôt le contraire car dans un système, optimiser le mauvais élément rend le système moins bon.
Si le problème dans la publication d'articles n'est pas la production des articles mais leur relecture, produire encore plus d'articles va juste ralentir la recherche car il faudra de plus en plus de temps pour qu'un article soit relu par des humain.e.s
Mais je suppose que cela permettra aux technophiles béas de l'Église de la Très Sainte Génération de faire du prosélytisme pour que les LLM assurent tout ou partie des relectures pour "sauver la recherche de l'extinction".
# Typst
Posté par mattpiz . Évalué à 3 (+4/-1).
Je sais pas si vous avez déjà essayé, mais Typst c’est vraiment top comme remplacement de LaTeX. https://github.com/typst/typst
# Lien cassé
Posté par Dafyd . Évalué à 4 (+3/-0).
Bonjour Laurent,
Au 0.6.1 : "Si vous comptez utiliser régulièrement ce logiciel, je vous recommande chaudement de l’installer sur votre ordinateur."
Le lien sur "installer" est cassé.
Sinon, je suis chaque année toujours aussi impressionné par le fait qu'un être humain soit capable de produire un contenu mathématique d'une telle ampleur. Je suis incapable de juger du fond (mes maths datent et se sont arrêtées en Math spé), mais bravo pour la forme, et pour la persévérance.
[^] # Re: Lien cassé
Posté par Dafyd . Évalué à 3 (+2/-0).
Au passage, j'ai bricolé un oneliner en bash un peu dégeu mais qui marche pour tester tous les liens :
Se placer dans le dossier tex des sources et :
Ca donne le code HTTP de réponse pour chaque lien. Tout ce qui n'est pas 200 est cassé.
[^] # Re: Lien cassé
Posté par Dafyd . Évalué à 2 (+1/-0).
Ah et il faut faire pour https:// aussi, j’avais zappé ce matin.
[^] # Re: Lien cassé
Posté par LaurentClaessens (site web personnel) . Évalué à 5 (+3/-0).
Ouep.
Il y a plein de liens cassés partout; c'est un problème récurent. Internet est le royaume de l'éphémère.
La détection de liens cassés n'est pas tellement un problème (ta ligne fait le taf; j'avais fais un truc en python du même acabit il y a longtemps).
La vraie question est : que faire avec les liens cassés ?
Dans le cas présent c'est facile : je supprime, et la lectrice trouvera elle-même sur le site de Sage.
Dans la bibliographie c'est un massacre. Les liens cassés se comptent par dizaines…
Je me suis résigné à ne plus m'en préoccuper : finalement c'est pas si mal que le lecteur se rende compte qu'internet est un gruyère[1].
[1] ou un emmenthal ou un roblochon, je ne sais plus … le fromage avec les trous.
[^] # Re: Lien cassé
Posté par Benoit Sibaud (site web personnel) . Évalué à 5 (+2/-0).
Remplacer par des liens archive.org de l'époque ? https://github.com/akamhy/waybackpy/wiki/CLI-docs peut aider
[^] # Re: Lien cassé
Posté par LaurentClaessens (site web personnel) . Évalué à 2 (+1/-1).
Mwouais.
J'aime pas trop
web.archive.org. Si quelqu'un veut faire disparaître sa page, c'est son droit.Le liens cassés dans le Frido ne me gênent pas tant que ça. C'est juste la nature d'internet.
Envoyer un commentaire
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.