Coq et caractères

Preuve formelle du théorème de Feit et Thompson

Piste verte Le 23 novembre 2012  - Ecrit par  Jérôme Germoni Voir les commentaires (5)

Une équipe du laboratoire commun Inria - Microsoft Research dirigée par Georges Gonthier a annoncé fin septembre la vérification par un ordinateur, plus précisément par l’assistant de preuve Coq, du théorème de Feit et Thompson, un résultat difficile d’algèbre prouvé en 1963 par deux cent cinquante pages ardues. La nouvelle semble susciter plutôt de la perplexité chez certains mathématiciens : qu’apporte une preuve par ordinateur à un résultat dont personne ne doute ? D’autres collègues, plus enthousiastes, saluent le tour de force de faire vérifier à un ordinateur un des fleurons de la pensée humaine.

Lacunes du discours mathématique

Malgré tous les efforts de son auteur, un texte risque d’être entaché d’inexactitudes.

Un exemple tiré de la presse récente

La presse, pourtant exemplaire en matière de précision, est parfois amenée à corriger certaines affirmations hâtives. « En témoigne l’erratum, (la correction) qui a été publié après un article [du New York Times] du 18 octobre et repéré par Rue89. L’article concernait Ahmed Abu Khattala, suspecté dans l’attaque contre le consulat américain de Benghazi. Le premier paragraphe racontait que, alors que les autorités américaines ont promis de le traduire devant la justice, on l’avait vu récemment siroter un jus de fruit dans un hôtel de luxe. » Bruno Duvic continuait ainsi sur France Inter le 22 octobre 2012 : « Erratum ! Ah bon ? On aurait accusé cet homme à tort ? Voici le texte publié par le New York Times. “Une version précédente de cet article décrivait de façon incorrecte la boisson que Ahmed Abu Khattala buvait dans un hôtel de Benghazi, en Libye. Il s’agissait d’une boisson frappée aux fraises et non d’un jus de mangue.” » [1]

L’Éden mathématique serait, par contraste, le lieu des vérités éternelles et inattaquables où de telles imprécisions n’auraient pas cours. Une preuve mathématique devrait partir d’axiomes si naturels et procéder par étapes si élémentaires qu’elle doit devenir évidente pour tout autre mathématicien, ce qui assure un caractère irréfutable au théorème. Beau programme, qui trouve son origine dans les Éléments d’Euclide, et précisé vingt-cinq siècles plus tard, dans les Principa Mathematica d’Alfred Whitehead et Bertrand Russell ou les Éléments de mathématique de Nicolas Bourbaki.

« La mathématique formelle » d’après Bourbaki

Dans le premier chapitre de la Théorie des ensembles des Éléments, Bourbaki présente un texte mathématique comme un « assemblage » de « signes » choisis entre les « signes logiques » ($\Box$, $\tau$, $\wedge$ et $\neg$), les lettres (éventuellement accentuées $A$, $A'$...) et les « signes spécifiques de la théorie » (en théorie des ensembles, $\in$ ou $=$ suffisent), certains signes pouvant être surmontés de traits appelés « liens ». Certains « critères de substitution » permettent de simplifier des assemblages, des règles de construction permettent de former des assemblages, dont certains représentent des « objets », d’autres des « assertions ». Pour définir une théorie, on se donne des « axiomes » et des « schémas » permettant de transformer les termes et de déduire d’autres assemblages.

Mais « l’usage exclusif des assemblages conduirait à des difficultés typographiques et mentales insurmontables. C’est pourquoi les textes courants utilisent des symboles abréviateurs (notamment des mots de la langue ordinaire). » Il faut une cinquantaine de pages à Bourbaki pour justifier les méthodes habituelles de raisonnement et de rédaction d’un texte mathématique.

Mais si on devait détailler la rédaction à ce point, la démonstration du moindre fait significatif deviendrait longue au point d’en être impossible à lire, voire à écrire. Aussi, les textes mathématiques regorgent de raccourcis qui, implicitement, signifient : « il est évident que... » Une preuve est donc écrite pour un public particulier d’élèves, d’étudiants, de chercheurs... avec un niveau de détail adapté à ce public (ou, du moins, qui devrait l’être) : remplacer $1+2+\cdots+n$ par $n(n+1)/2$ est un problème difficile pour un élève de troisième, c’est une évidence pour un mathématicien professionnel. Il reste donc au lecteur des étapes à combler. La formalisation que Bourbaki affirme possible en principe ne semble pas réalisable par un être humain ; de plus, elle obscurcirait plutôt les choses et on n’aurait rien à y gagner.

PNG - 76 ko
Un théorème des Principia Mathematica de Whitehead et Russell et une preuve sans mots : thèse et antithèse

En général, combler les étapes manquantes du discours mathématique se fait sans mal. Sinon, modulo les convenances sociales, le lecteur (élève, mathématicien, relecteur d’une revue...) est en droit de demander des éclaircissements à l’auteur (professeur, chercheur...). Mais il peut arriver qu’une preuve soit longue et ardue et que sa validation le soit aussi : celle de la conjecture de Poincaré par Grigori Perelman a pris environ quatre ans aux experts du sujet.

Erreurs et mathématiques

Par ailleurs, dans les implicites d’une preuve, peuvent se glisser des erreurs. Les articles spécialisés et les livres en sont parsemés : ce sont souvent des fautes mineures, comparables à la confusion entre fraise et mangue, que le lecteur repère et corrige tout de suite. Il peut même ne pas les voir, si sa démarche mentale est assez active pour qu’il suive les grandes lignes de la preuve et en reconstitue les détails lui-même. Mais cela peut être plus sérieux : après l’annonce en 1993 par Andrew Wiles de la démonstration de la dernière étape du dernier théorème de Fermat, les experts ont découvert un argument faux, que Wiles a réussi à corriger avec Richard Taylor en quelques mois.

Les erreurs sont un élément de la vie mathématique. Certaines restent célèbres, telle l’erreur féconde commise par Poincaré pour le prix du roi Oscar [2]. Mais on en trouve de nombreuses autres dans l’histoire mouvementée du 16e problème de Hilbert. Certaines erreurs en mathématiques sont corrigées, d’autres encore ne sont jamais détectées. On en comprend bien l’origine : avant d’avoir été poli par la pensée comme un galet par le ressac, un concept reste fuyant et malcommode, et ce qui paraît « évident » dans la fulgurance de l’intuition peut se révéler faux plus tard.

En tout état de cause, la validité d’une preuve est un acquis social : c’est une communauté qui donne le quitus. En pratique, la plupart des théorèmes ne font aucun doute : ils ont été compris et démontrés tant de fois... Mais cette validation peut être remise en cause. Certaines preuves d’Euclide ont été jugées valables pendant des millénaires, mais des géomètres de la trempe de David Hilbert les ont reprises et complétées. Plus grave, la preuve par Kempe en 1879 du théorème des quatre couleurs a été jugée correcte pendant une dizaine d’années avant qu’une faille majeure n’y soit détectée. Pour un exemple plus récent, le titre d’un article d’Amnon Neeman paru en 2002 est explicite : “A counterexample to a 1961 ’theorem’ in homological algebra” [3].

JPEG - 153.3 ko
Conjecture de Kepler et théorème des quatre couleurs : démontrés ou pas ?

Dans un registre différent, la communauté mathématique s’est déclarée incapable de valider complètement la démonstration de la conjecture de Kepler soumise par Thomas Hales vers 1999 à l’un des journaux les plus prestigieux, Annals of Mathematics. L’article a bien été publié mais avec des réserves : la preuve repose de façon cruciale sur des calculs sur ordinateur à deux reprises [4] Aucune erreur n’est connue dans la preuve mais même son auteur exprime des réserves à son sujet, au point qu’il a lancé un programme sur une vingtaine d’années pour fabriquer une preuve formelle.

En bref, presque tous les mathématiciens sont très confiants dans la robustesse de l’édifice mathématique [5] mais ils savent que des erreurs peuvent s’y glisser.

La question des fondements et le renouveau des mathématiques constructives

La question des fondements des mathématiques a été une des préoccupations majeures au début du XXe siècle. En voici quelques acteurs majeurs : David Hilbert, Alfred North Whitehead, Bertrand Russel, Kurt Gödel... Un peu plus tard, Bourbaki a proposé sa propre formalisation. Un large consensus en ressort : les mathématiques classiques reposent désormais sur la théorie des ensembles, laquelle est décrite par les axiomes de Zermelo-Fraenkel et, souvent, l’axiome du choix.

Néanmoins, cette position n’est pas acceptée de tous : les constructivistes contestent l’existence d’un objet qu’on ne peut pas construire ; cela les conduit en particulier à rejeter une preuve par l’absurde ; ils estiment que les axiomes de la théorie des ensembles engendrent des objets « trop gros » pour notre univers. Dans ce point de vue, une preuve, c’est essentiellement un algorithme (voir ci-dessous l’exemple du PGCD). Aussi, la montée en puissance de l’informatique a sonné le renouveau du constructivisme en mathématiques.

Dans cette mouvance, on peut citer Thierry Coquand. Le nom de l’assistant de preuve Coq est une double référence à son nom et au calcul des constructions, abrégé en CoC en anglais, dont il est le fondateur et un expert.

Vladimir Voevodsky, lauréat de la médaille Fields en 2002 pour des travaux classiques (non constructivistes), travaille depuis quelques années à clarifier les fondements des mathématiques. Il organise par exemple une année spéciale à l’Institute for Advanced Study de Princeton, avec Thierry Coquand et Steve Awodey. Pour reprendre les mots d’Assia Mahboubi, le but est de « comprendre comment une meilleure description des fondements des mathématiques peut aider à déterminer le bon langage et les bonnes définitions pour des objets les plus fondamentaux (catégories, ensembles, structures), qui induiront l’intuition la plus juste, et la plus complète de ces objets, minimisant les constructions bancales, ou trop techniques, qui incitent à l’erreur. »

Une preuve inattaquable : la preuve formelle ?

On peut chercher à améliorer la situation grâce aux assistants de preuve. Commençons par une idée banale pour un informaticien : on peut prouver mathématiquement la validité de certains algorithmes.

Un exemple de preuve (non formelle) de validité d’un algorithme

Montrons que l’algorithme d’Euclide donne, étant donnés deux entiers naturels $a$ et $b$, leur PGCD, c’est-à-dire un entier naturel $d$ qui les divise tous les deux et tel que tout autre diviseur commun à $a$ et $b$ est un diviseur de $d$.

L’algorithme se termine. En effet, à chaque passage dans la boucle, la valeur de la variable $y$ diminue strictement : il y aura donc au plus $b$ passages dans la boucle.

Pour prouver que l’algorithme est correct, on met en évidence un invariant de boucle, c’est-à-dire une assertion qui est vraie au démarrage de l’algorithme et qui reste vraie après chaque passage dans la boucle : elle sera donc vraie à la fin de l’exécution.

Pour deux entiers $a$ et $b$, on note $D(a,b)$ l’ensemble de leurs diviseurs communs. L’assertion clé est :

$D(a,b)=D(x,y)$.

Montrons que c’est bien un invariant de boucle :

  • Avant le premier passage dans la boucle, on a : $x=a$ et $y=b$, si bien que l’égalité est évidente.
  • Supposons qu’au début d’un passage dans la boucle, on ait : $D(a,b)=D(x,y)$. À la fin de la boucle, on a remplacé $x$ par $y$ et $y$ par $x-qy$ (où $q$ est le quotient de $x$ par $y$). Il suffit donc de montrer que $D(x,y)=D(y,x-qy)$ : si un entier $d$ divise $x$ et $y$, il divise aussi $y$ et $x-qy$ (si $x=dx'$ et $y=dy'$, alors $x-qy=d(x'-qy')$) ; inversement, s’il divise $y$ et $x-qy$, il divise aussi $x=(x-qy)+qy$ : c’est gagné.

En sortie de boucle, la variable $y$ vaut $0$ ; notons $d$ la valeur de la variable $x$ que renvoie l’algorithme. On a, d’après ce qui précède : $D(a,b)=D(d,0)$. Or, comme tout entier divise $0$, les diviseurs communs à $d$ et $0$ sont les diviseurs de $d$, parmi lesquels $d$ est le plus grand (au sens de la divisibilité). Par suite, l’entier $d$ satisfait aux spécifications.

Mais il y a mieux ! En effet, ce qui précède montre qu’il existe un PGCD et qu’il est unique (c’est loin d’être évident a priori) ; de plus, on a un moyen de le calculer. On voit, dans cet exemple, comment un algorithme et une preuve de validité de l’algorithme prouvent un théorème (l’existence et l’unicité du PGCD).

JPEG - 25 ko
Coq au secours d’Euclide

Un assistant de preuve est un logiciel spécialement dédié à la validation de preuves de théorèmes. On met ainsi en œuvre le programme lancé par Euclide : réduire chaque étape de la preuve à une évidence élémentaire, que même un ordinateur peut vérifier automatiquement (sans recours à l’intuition du lecteur ou à sa culture mathématique, en particulier). Comme le décrit Georges Gonthier, « l’idée est d’écrire un code qui décrit non seulement ce que la machine doit faire, mais aussi pourquoi elle doit le faire — une preuve formelle de correction. La validité de la preuve est un fait mathématique objectif qui peut être vérifiée par un programme différent. » [6] L’informaticien traduit la preuve dans un langage que peut intégrer l’assistant de preuve, ici le langage Coq, ce qui donne une preuve très longue ; s’y ajoute un certificat de correction de la preuve, produit par l’assistant de preuve, qui écarte la possibilité d’erreurs de calcul ou de raisonnement. On obtient ainsi une preuve formelle. La preuve se trouve ainsi beaucoup plus détaillée que quand elle était écrite par un humain et l’assistant de preuve procède à un examen beaucoup plus approfondi qu’une équipe humaine.

De l’algorithme d’Euclide à la description d’une preuve formelle

En extrapolant l’exemple de l’algorithme d’Euclide, on peut imaginer ce qu’est une preuve formelle :

  • le rôle de l’algorithme est joué par formalisation de la preuve elle-même : écrite initialement par un humain (dans l’exemple du jour, Feit et Thompson en 1963), elle est traduite par un humain (Georges Gonthier et son équipe) en langage compréhensible par l’ordinateur (le langage de Coq) ;
  • l’assistant de preuve (Coq) vérifie et certifie la validité du code ainsi écrit. [7]

L’algorithme d’Euclide et le PGCD vus par Coq

L’algorithme d’Euclide et la notion de PGCD sont des notions si basiques qu’elles font, évidemment, partie de la distribution standard du logiciel Coq. On les trouve dans cette bibliothèque d’arithmétique élémentaire, dont ce bloc dépliant est une sorte de fiche de lecture rédigée par un béotien. [8]

La page commence par la définition de la divisibilité : le critère pour pouvoir affirmer qu’un entier a divise un autre entier b, c’est de pouvoir trouver un entier q tel que b=q*a. Puis est introduite une notation infixée et viennent un grand nombre de résultats (des Lemmas), chacun suivi de preuves. Le premier de ces lemmas exprime qu’un nombre est toujours divisible par lui-même : pour le voir, il suffit de prendre q=1 dans la définition et appliquer une des règles de calcul pour simplifier 1*a en a (ring). Facile, non ?

Non, pas si facile : que veut dire la ligne qui commence par Hint ? Passons. Les deux lemmes suivants, Zmult_divide_compat_l et Zmult_divide_compat_r, expriment tous deux que si a divise b, alors ac divise bc, et ce quels que soient les entiers a, b et c ; ces lemmes coïncident à l’ordre des facteurs près (l pour « gauche », r pour « droit »). La preuve du premier est une récurrence sur c ; la preuve du second se ramène au premier en réécrivant, dans la conclusion souhaitée, a * c à la place de c * a et idem pour b ; on conclut alors trivialement...

Et ainsi de suite : on voit défiler un grand nombre de propriétés plus ou moins immédiatement identifiables et des preuves, qui utilisent les propriétés précédentes. Pour le non-spécialiste qu’est l’auteur, il est frappant de voir combien la syntaxe est presque familière. Presque, seulement...

La définition du PGCD qui suit se paraphrase ainsi : on dit qu’un entier d est un PGCD de a et b s’il est un multiple de tout entier x qui divise a et b. « On prouvera son unicité plus loin », promet un commentaire dans un cadre bleu. Viennent une série de « propriétés triviales », par exemple la dernière : la valeur absolue d’un entier a est un PGCD de a et 0.

Puis l’algorithme d’Euclide. Sans aller dans les détails, on observe deux points clés : d’une part, les lemmes Zis_gcd_for_euclid et Zis_gcd_for_euclid2 permettent de passer de a et b à b et a-q*b ou à b et b*q+r ; le lemme euclid_rec fournit l’invariant de boucle évoqué dans le bloc dépliant ci-dessus à l’assistant de preuve. La lecture de cette partie est moins facile à interpréter que ce qui précède, mais l’exécution apporte quelques éclaircissements. Essayez !

La formalisation complète d’une preuve est, on l’a dit, un travail quasiment insurmontable pour un être humain : c’est ce qui explique que le processus prenne six ans pour une équipe entière pour un théorème de la difficulté de celui de Feit-Thompson. Mais, par les progrès de l’informatique et du matériel, sa vérification intégrale est devenue accessible à un ordinateur, ce qui donne une motivation pour un travail titanesque. La preuve formelle est un champ de recherche qui se développe en informatique depuis plus de quarante ans. Les experts font généralement remonter le domaine au système Automath élaboré en 1967 par le visionnaire Nicolaas de Bruijn, disparu cette année à 93 ans. Mais depuis, de nombreux théorèmes classiques ont reçu une preuve formelle [9].

La formalisation et la certification de preuves mathématiques s’inscrit dans une branche plus large de l’informatique, la certification de systèmes divers : processeurs, logiciels, matériels, protocoles [10]. Longtemps, la seule façon de s’assurer que quelque chose allait fonctionner conformément aux spécifications, c’était de la tester. L’analogue mathématique serait la vérification d’un énoncé sur un grand nombre d’exemples [11]. La certification par un système indépendant apporte un degré de confiance supplémentaire, de nature différente : l’analogue mathématique, c’est une preuve de l’énoncé. La certification est particulièrement cherchée pour les systèmes dits critiques, dont le dysfonctionnement aurait des conséquences plus graves que la confusion entre deux boissons sucrées : l’explosion de la première fusée Ariane 5 est due à une erreur « mineure » d’un logiciel [12] ; comme passager, on souhaite que les calculateurs d’un avion présentent les meilleures garanties de confiance, etc. Un autre exemple célèbre où la certification a été utile, mais un peu tardive, est le bug de la division du Pentium, qui a conduit Intel à rappeler à grands frais une génération de processeurs en 1994 et à investir dans la certification : depuis lors, Intel fait prouver formellement ses algorithmes arithmétiques (travaux de John Harrison entre autres). L’avantage du domaine mathématique pour ces questions, c’est que l’on n’a pas à affronter l’imperfection du réel.

Vérifier la preuve, pas trouver la preuve

Attention : il faut distinguer la démarche de certification de preuve que l’on vient de décrire de la recherche d’une preuve qu’effectuerait l’ordinateur plus ou moins seul. Ici, les ambitions sont moindres : on cherche à valider une preuve existante, à donner « la preuve de la preuve » [13].

Bien sûr, il serait beaucoup plus ambitieux d’espérer programmer l’ordinateur pour qu’il démontre lui-même le théorème à partir de son énoncé. David Hilbert rêvait, dès 1928, d’un algorithme universel pour décider de la véracité d’une assertion mathématique. Mais en 1936, Alonzo Church et Alan Turing ont démontré indépendamment « qu’un tel algorithme ne pouvait exister. Avant même la construction des ordinateurs, le théorème d’indécidabilité de la démontrabilité fixait donc l’existence d’une limite intrinsèque à leur utilité en mathématiques. » [14] En revanche, valider ou infirmer la preuve d’une assertion mathématique est un problème décidable, c’est-à-dire qu’un ordinateur peut le résoudre (en principe).

Pour reprendre une image que l’on trouve déjà chez Bourbaki (loc. cit.), quiconque connaît les règles des échecs peut vérifier si une partie les respecte ; mais ça ne suffit pas, loin de là, pour être un bon joueur. Un ordinateur programmé pour démontrer des théorèmes, qui ferait des déductions dans un ordre méthodique (par ordre lexicographique des preuves possibles ?) ou au hasard, aurait bien peu de chances de démontrer le théorème des quatre couleurs ! Encore moins qu’un logiciel qui essaierait de retrouver les quelque 260000 caractères de Cyrano de Bergerac en commençant par « aaaa... » ou en les choisissant au hasard.

Et pourtant : l’informatique est un recours inévitable...

Gilles Dowek [15] renverse cet état de fait apparemment négatif pour justifier que les mathématiciens ont besoin des ordinateurs s’ils ne veulent pas se cantonner dans des « preuves courtes ». En effet, décider si toutes les propositions démontrables en moins de dix mille pages sont vraies ou fausses est un problème décidable (il suffit d’énumérer toutes les preuves possibles, les valider ou les réfuter : c’est hors de portée d’un ordinateur en pratique, mais ça n’a aucune importance ici). Il existe donc des propositions démontrables dont la preuve la plus courte est « longue » (peut-être que le théorème des quatre couleurs est de ce type) : pour cette catégorie, l’ordinateur peut aider l’être humain en prenant en charge des portions importantes de la preuve.

Peut-être peut-on objecter que le pouvoir sémantique des mathématiques augmente et que les preuves tendent à devenir plus courtes lorsque leurs concepts deviennent plus puissants. Ou estimer qu’il n’y aura plus de source d’énergie pour faire fonctionner un ordinateur avant que la panoplie des propositions à preuve courte ne soit épuisée. À ce moment-là, l’hypothèse de Riemann sera peut-être une préoccupation subalterne.

Validation de la validation de la preuve...

Bien. Mais qui valide l’ordinateur qui certifie la preuve ? Qu’est-ce qui prouve que l’ordinateur fait mieux qu’attendre un moment (pour la crédibilité) et tirer au sort pour répondre « oui, la preuve est correcte » ou « non » ? D’après Thomas Hales, il y aurait dans tout programme un bug toutes les 500 lignes de code. [16]

Ce qui fonde la confiance dans une preuve formelle, c’est que l’ensemble de l’assistant de preuve est contrôlé par une toute petite partie, qu’on appellera le noyau du logiciel. La taille du noyau est suffisamment petite (500 lignes environ) pour pouvoir être scrutée par un humain ; de plus, il a été (at)testé sur un grand nombre de situations variées. Même s’il n’est pas capable de se certifier lui-même (théorème d’incomplétude de Gödel oblige), le noyau est capable de certifier le reste de l’assistant de preuve.

Il y a un deuxième étage de validation du système : en effet, un assistant de preuve est écrit dans un langage « de haut niveau », c’est-à-dire très éloigné de l’assembleur qu’utilise le processeur. Il faut donc le compiler, et il est connu qu’il n’existe pas de compilateur parfait. Néanmoins, Xavier Leroy travaille avec d’autres et avec succès à la certification de compilateurs, ce qui permet d’espérer pour bientôt de garantir cet aspect.

Résumé des épisodes précédents

Une preuve formelle est une formalisation d’une preuve, c’est-à-dire une traduction purement symbolique en langage informatique d’une preuve écrite par un être humain, et un certificat de validité de cette preuve fournie par un logiciel spécialisé appelé assistant de preuve, qui vérifie que toutes les étapes de la démonstration sont correctes et qu’elle démontre bien ce qu’elle affirme démontrer. La confiance dans l’assistant de preuve vient d’un examen et de tests approfondis du noyau et de la validation du reste par ledit noyau. Tout cela donne une confiance nouvelle dans la preuve.

Au bilan, une preuve formelle diminue énormément la possibilité d’erreurs mais elle ne permet pas d’atteindre une certitude philosophique. [17]

Après ces longues généralités sur la preuve formelle, venons-en au théorème qui fait l’objet de l’annonce.

JPEG - 97.5 ko
John Griggs Thompson et Walter Feit

 

Théorème de Feit-Thompson

Énoncé comme une conjecture par William Burnside en 1911, le théorème de Feit-Thompson s’exprime en très peu de mots.

Tout groupe fini dont le nombre d’éléments est impair est résoluble.

De façon équivalente : tout groupe simple ayant un nombre impair d’éléments est cyclique. La théorie des groupes est la formalisation mathématique de l’idée de symétries. Alexandre Grothendieck « n’hésite pas à parler de l’invention du zéro et de l’idée de groupe comme deux des plus grandes inventions mathématiques de tous les temps » [18]. Le concept de groupe traduit l’idée de symétrie, de transformation. Un groupe fini est donc constitué d’un nombre fini de « transformations ».

PNG - 13.7 ko
Icosaèdre régulier et un plan de symétrie

Définition d’un groupe

Appelons transformation d’un système ou ensemble $X$ une application bijective $g$ de $X$ dans lui-même : cela signifie qu’à tout point de $X$, on sait associer un (autre) point de $X$, et qu’il existe une « transformation inverse » $g^{-1}$, telle qu’en appliquant successivement $g$ et $g^{-1}$ (dans les deux ordres possibles), on envoie tout élément de $X$ sur lui-même.

Un groupe est alors un ensemble (non vide) de transformations d’un système satisfaisant aux conditions suivantes :

  • il contient l’inverse de chaque transformation qu’il contient ;
  • il contient la composée de deux transformations quelconques qu’il contient.

C’est la présentation classique (d’avant Sophus Lie) préférée par Vladimir Arnold à la définition abstraite. Pour ceux qui le connaissent, le théorème de Cayley garantit que cette définition est équivalente à la définition axiomatique habituelle (au moins si on travaille à isomorphisme près).

Voici un exemple : fixons un entier $n$ et soit $\alpha$ l’angle $360^\circ/n$. Les transformations consistant à tourner autour d’un point fixe d’un angle multiple de $\alpha$ forment un groupe ayant $n$ éléments, appelé groupe cyclique d’ordre $n$.

Parmi les groupes, les plus simples sont les groupes dits commutatifs. Cela signifie que l’ordre des transformations n’importe pas : si je me déplace de 3 mètres vers le sud puis de 5 mètres vers l’est, je me retrouve au même endroit que si je fais les déplacements dans l’ordre inverse. Mais la plupart des groupes ne sont pas commutatifs. Si, d’une position donnée, j’avance droit devant moi sur 5 mètres avant de tourner d’un quart de tour, je ne me retrouve pas au même endroit que si je commence par tourner, puis que j’avance. Cela illustre le fait que le groupe des déplacements du plan n’est pas commutatif.

Voici une idée simple (et discutable) : un groupe commutatif, c’est facile à étudier. Les groupes résolubles sont, en un certain sens, « presque commutatifs ». Les groupes simples sont, eux, aussi éloignés que possible de la commutativité [19]. Ainsi, les groupes simples sont compliqués... Ce sont plutôt eux qui intéressent les experts, même larsqueeeeeeeeeg/wiki/Vladimir_Arnold" cedia.org/wisi, ct pni élol0u' rel='eexpliquete' rel='footnote' title='Il y footnote' title='Par exemple : t8217oit que si je fdl cla'spip_cnhXavier Leroy tr » sp;noediv>

Vladimir ArnoldJean-Peve e Sve e Intelrantiimre d’un id='n' clfdlcan enphyseuve dau' clfdlcpni ér exempn. Mogramme (x,y)$. À »Vsavez8217;tivisme léments8217;ést cyclique. La Uneant mia.org/wisi, ct pni élol0u' rel=';espérer pou/p>

Et pourtant : G/i> sont, en un ce,nt compliqués...( id='nhhard;un nnaî='blocs_destination blocs_invisible blocs_slide'>

Appelons transformadonc const$G (au sa doe cimples sontlgorithmess diviss(...)' is dits c='spip_, Intel faslectur lbrints. Esure différ $X$ signnnaistaxe thématique, ciithme et banale poEt mpo cetorg/wisi, ct pni de core elle-même&n :>

    _0=1$x=v>_r= l, dits X$ su$k\ge1$x=v>_{k ordriseurs cn_k les dp_k=n_k/>_{k ordrre. Prm résAouver t8217oitmess diviss(...)' is dp_kdrre.le aflangage e depuisse. Mais la pli un 7;entique tout dits $n=6$la'spipe dceal'>Vl$ (dan>_0=1$les dn_2=6$ suffit pas,  (.ue lRdn_1=2$,énergrcissem dp_1=2$les dp_2=3$s, qule afdn_1=3$,énergrcissem dp_1=3$les dp_2=2$$X$ signDur peut,nt ntiers natuoit c constituédG x=(x-bsp;transfot dépduee du-ments te (G_k)_{0\rg/k\rg/r} lpplien un$G_0=g{1\} ,n$G_r=Gxiste dits X$ su$k\ge1$x=vG_{k ordrre.uche de sinodiquvG_k les dS_k=G_k/G_{k ordrre.qués.sAouver t8t dépduont compliqués...dS_kdrre.le aflangage e depuisse. Mais la pli un 7groupe

11-à-dire très éloigné de siithmen uts les e (lsst cycliqercheParmi les groupes, lle< pour sont pmplacsmecrit.18].2' >2temps, la seu,aitée, estribles Hales, sp;:rel=ransnverse. Maisnn sera pe,=ransnverstée, théorie des groupes est la queue (d’isatis_blocs'>

Et pourtant : Qs (va sur i articdQu’est-ce q: queue (d’iient rano de Be='blocs_destination blocs_invisible blocs_slide'>

Appelons transformaenttème satisfaisdiscutab217;élqui se s Hales, s$g$ de $srre. Pcours à l& en mère pour poong> estl e dare eifférenil suf’ensembllelass='spip_ un ensem7;entique tout dits oupes ra estd décpac, je coren clad’Eucicatiol e daéreexplyrand n, sp;:relrpduont compliref="hst suousri217;esiloignd L&# sont lndre us#821 7groupe est queue (d’ateurs s>

est rano de Bateurs s&tialementa preuve lui-mêmee lémenla'spipoint ’él,elr.wikipedia.org/wiki/th%C3%A9orie_des_grTanoe_(Eucpes" 8él)rel='external'>Xavier Leroy trtanoeétiqumps#8ousri21nsnverstdqueue (d’upe tà cquamen etu des dstupque $g$ et 8217 pour pouvoirano de Boirano drIl fatdqueue (d’re qu’un ordinateus, cRte' relilosophdqueue (d’ (s).

Voici un edre l7;oralsinof;: uewisi, ct pni élol0u' rel=';i mêm_cnh

Nmreux teeeg/winbsp;:ss="spip">

Tout groupe fini dont le nombre d’éléments est impair est résportance ie de

De façon équivaleCrouge>Lemmaion dRe le gr#8217 type de a s est la queue (d’iommutatif,e he est mvrammecode me de la affou mncret un upes é d unM1omme le é d unnbsp;» tip_i>groupes simpl ceons-en quner hste preuve nbsp;vaux de John Halus grano de Bergemo queue (d’iiee lémen (wikipedia.org/wiki/th%C3%A9orie_des_grEos no_Eucpes" 9brintsrel='external'>Xavier Leroy truve nbsp;de de Göde accesip_nor c;ut pquest m Churchla preuvep;: quede sit;unp plerirano drIlée de$p$

18].21'>21p>Bien sûr, il serorème de Feit-Un nt fixénorc : ilthématiqus='spratiqion adi> d’un énoncproduit par lRit. est la queue (d’i. Aposa Mahboubnt meents erivaoj#8, dans st-ce q: nbsp;» Aurmatbut, quelquey;i mêm Pcours à l&dent à qiviss(nbsp;:l sont lboo étns CoqXavier Leroy trLs/L3 Aa> ysiliref (VoiOdd Or d&Tec" em='blocoduphiqH.ans d&tionG. Glaub c_re(Caiviidge doseursity...Xavier Leroy trChrano d&Tec" yiref TVoiOdd Or d&Tec" em='blocoduphiqT. Pe djouvie(Caiviidge doseursity... est une formalit.4Feit-Thompson s’exprime en embllel validatiouge>Lemmai#8217;idée demart $g$ lus courte est que lfallu qeqphique qu̵upe veulemmaut7; basiq’ancialiste que (il suffi st de ce type)&nbrecte 󈫘 un pirammesophiquepour cque $gce,en un es17;ané) et t ;rong>Demia.or>

Apeus, c#8217;un aquede machinet-ce q;ee ou infirmer/ersnouvefronter ur. Il f enprincipe)Lemma,retrouv d̵arge d17;. Au touteaérlapnais uewisi, ct pni élol0u' rel=',dte 󈫋 nen quner hsteci). fier théorie des groupeavant tique%29pduont complir has ux, aussi17;aA posthme etllel ;anAposa Mahboubnt nbsp;» (eificationrnie ivaoj#8iciel ssiquesn anglais ; lst suous les temps&n17;un artic s󊌹il etu des d reste pnbsp;&#du plae poursvation i(lun humest pnPour naisrofde ss presque lRit.

Et pourtant : Cvant tique%29pduont complir has ux, aus (10 ss2 Cport ou circulessus à lR/a>]='blocs_destination blocs_invisible blocs_slide'>

Appelons transformaLuewisi, ct pni avant tique%29pduont complir has ux, aus, qus='sisionnai83ux que si isons pour les

bre de $5$llets à ouat)tesnt la compdiv classi;transfomg snsfoLiithi.e.ddiv classi suousri217 que, ci>loon. Maisuousri217;upart out uede sit;unp p;trasnt la compdivaisuvingt-ruipnbsp;», compliqsfraxicogexemple la dernhref="http

Résumé des épisodes="hte rueuve formeple (esements. rtie essrdinateur, pss="spip">
  • il contient l’wikipedia.org/wiwww.msr-class=class='spPaoj#cts/ous -ransf. Ous/f7;extrime enrel='external'>Xavier Leroy trAus='sprode Fi7malisaduit par17;un énoncéne preuve sais uede l&u aura pIlasse de gnt&nbs (vaoj#8i

    P\alpts commutatiwikipedia.org/wiessecati.micsonoft.ne /en-us/news/f7bsp;:s/gipe) enpe AM-101112.aspxrel='external'>Xavier Leroy trTec" emthe AM Giqu& Acsayem='bl sais uede l&u&#Micsonoft Rssecati contient la compCon-ri2 Vroy/niommutatiwikipedia.org/wiwww.lemans ='spsFi7;nat/Rittaud/2012/11/01/un-avant Xavier Leroy trU7;avant iD17;hiv>ommutatiwikipedia.org/wi qui soc. c. rec/jcmsi qu_63417/du-u ie-a-la-reesipeassi-devenirrel='external'>Xavier Leroy trDu, d&# axiomateueiqu;&#du pldevenir='bl saisIqui soc. c (juin 2012, qutme de deux&e&n&ibsp;(vaoj#8i17;exprime en) contient la compwikipedia.org/wiki/Alexandre_Grothendievient d&Pentdeveniaire' rel='external'>Alexandre Grothendievient d’un e='bl saisWlexandre_fr contient la compwikipedia.org/wiwww.la17;une pr='spfoutrnt/ 93s&nb/Rittaud?id=30903rel='external'>Xavier Leroy trLesp;(...)' id='e&nR7;une preubl nnbsp6;46d(un ceents 2011),omme le hée et hors dli> il contient l’nbsp;» Le de Gödune preuve te uve.

    ont bcogexemple la den assistan hutve daertiGreuvrdaBolrysnt la compcit.' id='nht-ce q: nbsp;» Le de Göd l’informatique. Lee de Gödune preuvexemple la dernt la compns sa version&nommutatiwikipedia.org/wiwww.la17;une pr='spfoutrnt/17;une pr/Rittaud?id=4026rel='external'>Xavier Leroy tr »A confirdte ̻rison ent aura pIe plDinursatis_b la compPnesquepoun grss%29pduonte c nbsp;» vramxemple la dern niveau a preuve laxemple la dern niveau  eobc laxemple la dern niveau  elaeus,ucouxemple la dern niveau 7;un av laxemple la dern niveau coh217;anxemple la dern niveau 7;ordiifxemple la dern niveau a d’i>groupes sim..o&nbsntt nl/fr.wikipediaImutativitout' rel='external'in'> clasittaudsationt c;ut différ , le thématiqcne pagn’est la préP17;é de F

    Np>P\alpts ss="spip">

  • il contient l’wikipedia.org/wiwww.ams_Grotnloc. c/200811/rel='external'>Xavier Leroy trD(...)'f17;est l='bl sais ar lRie formalit possibl/i> loc. cit. (Voilmee can Mt(Vont beal Sint tyrmatiovol. 55, numb)'f11 (2006) (p17;é de F P\alpts ss="sp;ssiblRittaud7;s. Si,acupation eue (rxbrsen enab natusp hors dli> il contient l’aurait dans ommutatiwikipedia.org/wiwww.ams_Grotnloc. c/200811/tx081101370p.pdfrel='external'>Xavier Leroy tres of the AM='bloc la 8217cson équipe) enommutatiwikipedia.org/wiwww.ams_Grotnloc. c/200811/tx081101382p.pdfrel='external'>Xavier Leroy tres of the AMformellTVoiFnt-Colod&Tec" em='bloc la compJautres). L&#ommutatiwikipedia.org/wiwww.ams_Grotnloc. c/200811/tx081101395p.pdfrel='external'>Xavier Leroy tres of the AMformellTVo" yitionPano ice='bloc la compFreeksWlndrjkommutatiwikipedia.org/wiwww.ams_Grotnloc. c/200811/tx081101408p.pdfrel='external'>Xavier Leroy tres of the AMformellGete de StRited='bloc la la nt la la nt_doc estination "utat-nt&nbsum" réguliePtat-nt&nbsum :ateurs s&# ilthématiqant d de deuds femeent deCon-ri2 Bte' fé, Damve dGiv>t,dte&ersnouveesilerirtions» pseudn comgre u,nAposa Mahboubnt Jean-Michel Mulu qu&OliailleReboux,peuc Sdinau1argeriRom esd&Tei&nbsntqcp>Uneane $srladimir_Arnolo ddre u artionnementhématiqittaud t8t bnt d&i une preuba pree F énorount_doc Aittaud er a foura hwikipedia_Ghys-Etlié _out' r>Étlié Ghys='bl estination "empls"c eh2> loueuve2c estinspan>b1sformaote_ref"> [1p>BieArgearsymé id='nh)&n lesd (Voibe idtrouthat Ahmsd Abu Khattatewa pfrink de at (Voihmplns stewa paoateawbolrytionpenlaemptc_rgo jui21&#which iblwhat Voihadequeeted.taidl class='spistinspan>b2sformaote_ref"> [2p>BieXavier Leroy trl#8o de confte de ceirpduone permetcomPdiaca1_nor b3sformaote_ref"> [3p>Bie

    Au bilastigiisseiervu.Iiques deue Mt(Vont beaei est Lformation inverisi, ct ples choisissanemenNere u nouvell toutef-e :e tra il sRnbsp;:len en="lementcomgsi,t> 4p>Bie

  • <, mais çs est ut $n$/p> touts;espérer pte17;u’esinie eseen/diu’ d gve forme ڰan cet usnouate>

    De f='spistinspan>b5sformaote_ref"> [5p>Bie18;8217;tis nouvelsur 5 mèr bientnvIlngeq [6p>BieDe f='spistinspan>b7sformaote_ref"> [7p>Bie

    <, mais simtoution adi>rtie les res transform;utide la re.le afnditionstrapotan hrmationbouclusetisistanst unnta preuvee islnge

    De f='spistinspan>b8sformaote_ref"> [8p>BieXavier Leroy trbesoubl contiesont gnt&nbs&nbsmutatif.

    Vrmalit sont vale5 est id='nhXavier Leroy trbesoublt m Chur rechercp17;éir: il étion est équvale5 est-ce q;ee ft de17;il nin;teursifpleri7pes - clfrathmoin;teursio entièrroie eson eCoq.ee objeue217;àode cltièrompl’e de Gödtouoy/s ( du noyau.

    De f='spistinspan>b9sformaote_ref"> [9p>BieAlexandre GrothendieUnealt titsinofedPcours or théorie des groupes ct pni st diviss(...)' isor De f='spistinspan>b10sformaote_ref"> [10p>BieDe f='spistinspan>b11sformaote_ref"> [11p>Bieins"htde deux&$10^{12rdrre.qgrandesns que diviss(...)' is nouvelle dquepour dans la prsnverstwikipedia.org/wiki/th%C3%A9orie_des_graef="http:PentGoldbaghaire' rel='external'>théorie des groupeaef="http:/u&#Goldbaghor 12p>Bie

    Vrfallu qtinguer la mutatif.sujours dentt&tents. jtiquevénérlhématiqcci>)&n, cRtnse l,nt âcnntaluontt thh3> i 2sp;(vaoil suf.er ou infirmerlesé appeli mêm_cnhbugsi él#821fulfo821Anbade 4t-ce q: r fairee perm8ubalnt mêm: quee7;assisreca#8#821rnce drs nLmérints. Est unq’anesfait que le groupa8q’acrapossibitée,s la prn$.

    De f='spistinspan>b13sformaote_ref"> [13p>BieXavier Leroy trsittaudsatio ttBo sa version&nres possa# id='nhb14sformaote_ref"> [14p>Biethéorie des groupes ct pnie de Gödne pre odmplerGödeloublt dnér1931,retroip_cnh [15p>Bieb16sformaote_ref"> [16p>Bie

    au). bout ditst d-ilt m Chuetroimbe o#82l, /i>bugsi é de gmate pan cla toutntiiatassiirammerchmoyié s possa# l&e 5 est id='nh.)_blocsf='spistinspan>b17sformaote_ref"> [17p>Bie.inp;trreuatio diminue io d la... sont uesqungnge ..; basiquesRitede cs;rong>Dionnemc deslli las

    De f='spistinspan>b18sformaote_ref"> [18p>BieXavier Leroy tr, article publié oublt l’occasion du bicee. Mais aire (...)' id='nhnie de Gwikipedia.org/wiki/th%C3%A9orie_des_grpes"89 pnb;tr_Ge pubaire' rel='external'>théorie des groupeÉ pnb;traGe pubsatis_blocsf='spistinspan>b19sformaote_ref"> [19p>Bie .etsi é#8217;une posPits oupiv>ro épeutransform;utide lat  (.Etmart s res tu circul classix be eat yante du-ments dre.uche de sit-ce q;ecul classit, en un cle de deurmation inveieux d&#les choisissanuee du-ments teuche de si ss="sp;sbicee. Mais psform,ecul classibre impmutatif.< ce de deuimêmeirmalmia.oci). dl class='spistinspan>b20sformaote_ref"> [20p>Bieoupes rathém si,t> De f='spistinspan>b21sformaote_ref"> [21p>Biewikipedia# le ger"cPle ger clasittaudsatiuve2c e> il contieha eac elic eikipediang>lto:?sub="ht=Coq.ent rano de Be&body=Coq.ent rano de Be - Imort ouont bcoge : .org/wi mort .rong.cnrsc'spCoq-et-crano dt .ut' rel='ext"link-dantno "lt : in"Envoyer clasittaud &a> tve;eculns ">nnannannannawikipediaurtant ac eh3nCréela sn trou:uve f e'blocs_destination "locs_invisible blocs_slide'>

    Appelons tranac eikipediaIMG/nttè1369.png">Imorteux&e&nundsatio- Lesé ooip_cnhCef="http:/u&#Kepntionamhe plretrouve mpialmia.onueephde Be ln o17;énnsmmutativit, Intel famment &#i ouats tingue?satio- WlexandreP\alpts e formelleL..)'ce Cre="sp eComrrec
    Tisi, ct pni st de ce type)&nbpasse- WlexmndrePComrrec formelleDe pourasion c
    Ceq ibiliatiqueur faireEucl thpasse- WlexmndrePComrrec formelleL..)'ce Cre="sp eComrrec
    Cef="http:/u&#Kepntioentdisi, ct pni st de ce type)&nbommutatifamment &#s ouats tingue?satio- WlexmndrePComrrec formelleL..)'ce Cre="sp eComrrec de e pourasion c
    JautrGriggstu' rel=';lanWx/divi17;esatio- Oberwolde h formelleL..)'ce Cre="sp eComrrec
    Idasaèdon euege et;lan éplale ttsref="httsatio- Imorteeueique&#i certiwikipedia.org/wiwww.sortrong.ie_drel='external'>Xavier Leroy
    trSortsati
    nna il contiforum"c eliispa"forum6271"il contiforum-fil"c eliispa"forum6271"il conti;ut dif"c estinl='ext"coutrnt"c estinl='ext"head"c eh3>Coq.ent rano de Beuve f tre>ud 23 noveents 2012 ux&08:29,te paBsi,tve danonymeocs_d ef='sp estinl='ext"meLsort"c ep>>>>émomiementbasiqt d exem.oculnrgumia.ofaux,pes tWi qs ,eeue possiri7;eigeqcertiRo1928 Taylod&res;ytents. moiy$X$ signHeuu..cutatif.

    _Richard_ Taylod&n&#ommuta?e/pc eikipediaCoq-et-crano dt .ut' ?id_forum=6271#;ut difu)"ll='ext"answu)">Rp;ouidr#8i>loo meLsortCoq.ent rano de Beuve f tre>ud 23 noveents 2012 ux&09:28,te paJ"htt co Gerpreiocs_d ef='sp estinl='ext"meLsort"c ep>Ahem ..;Eble7;un , jt de $Xaut usasi iqercheD eikipediaCoq-et-crano dt .ut' ?id_forum=6272#;ut difu)"ll='ext"answu)">Rp;ouidr#8i>loo meLsortCoq.ent rano de Beuve f tre>ud 22 un ceents 2012 ux&13:24,te paPide;:éncanneocs_d ef='sp estinl='ext"meLsort"c ep>À='se os ersp> Lmia.omnh

    Tout groupe fini doL’dune preFi7; rphidui courte est u circulqungngepes tetreade accratnt&vient d’un e, e (e#elqungngepCoq,d21n à nouvelle te est s’nguenna

    De façon équiv i do1uxLab correctes et euve n à l&djer mutatif.

    norct mia.o17ngue.eComrtllel ;anAposa Mahboubnt i’exc95%du ss=")Lemma18deellel,edCe soquepousest ut $n$deellel. Dec succès t&nbs>Np>PCoq,dla mutatif.

    besoint surnceerdde la démooupipe18deellel,elesé appeleammethmo qtsp;nombre,eltroi pos. Comrtludiqurg sistanucp17;eiont besoi (e>

    17!)> la pui peune preFi7;i17 signJe.voudt usaaje lars;ytents. ès à fot différ i17 signAt doim correctes et ep>PCoq,dmutatif.

    norct mia.oobsctp:/( deluds roie certicPrincipsa Me(Vont beaa$X$ signB. Qst> ont besoin17!p">Rép>C. Ix-bsp;trai strait des drn i mutatif.. Si,u8un humfamment &#s es te pamachine, ès à l&djee ipe)umachine ssiuep>P/p exempont correctes et t m Chulusnfbasiquunbsp;: ssmz est pnbsoér;lan/p> clasittaudsatiotutatif.AnsodimChamb)'t-Loie relatrai stpoc eloppepe cy Lem"htde dhu/p> Xa"ier L"roy ">e tMans satiotu 14 avril. (liste ér sdiqucb naepe c,aé sode cli aune prr &la éon inve son équipe) en de l:lemans ='sntier ora éoecoe sitcoteud’une proe.onueeuivrs pelqi7;i)e/pc eikipediaCoq-et-crano dt .ut' ?id_forum=8258#;ut difu)"ll='ext"answu)">Rp;ouidr#8i>loo meLsortCefnbspcpra> | wikipediarnal.php?port=>)&n lea Ss&amp;qung='snamp;mode=6forum">s’dserchepra> | wikipediarnal.php?port=rnal'e is&qung='s">cot de e ise oion du ?pra>

    De ffieldsen> ip_docp ef='sp estination "açon-relatrd"ispa"suggt que l"c eh2>wikipedia#suggt que l"cAittaud7;saggérésitsvo7;avmz aimrm clasittaud,evoe (esements. suggt que l ointnt bcogerlaittièt unvo7;inrts, mêr/:e/pc la elic estination " mort"c eikipediaUn- la... son-tiè-eureles -lt .ut' rel='ext"hors-pp;tr" eimg src='es/L3/irtio-gd2/44/03232d89d531c8112bc7f0cdde50f3.jpg?1481145452' width='320viheight='180vi/ efap ef='sp estination ", mume"c estinl='ext"t : i">wikipediaUn- la... son-tiè-eureles -lt .ut' rrU7;v><, mais tièrrtie les rcp>venir rong>ont bcogeud wikipediaUn- la... son-tiè-eureles -lt .ut' rr27 aoûta2i14='blocod estination "oinhor"c eikipedia_Aposa-Mahboubn_out' r>Aposa Mahboubnnna< ces e ér 'sittaudps ces lfap ef='sp e/lic elic estination " mort"c eikipediaUn-n='sppt-mt(Vont bwikipediaUn-n='sppt-mt(Vont bud wikipediaUn-n='sppt-mt(Vont bBiocod estination "oinhor"c eikipedia_Ehrhardt-Caroli _out' r>Caroli Ehrhardt Prong>ont bcoge. Onsimtoucpossira e (ehsteo17;iermet aiurte rus, queXIXe s poc/p,irnie iesilerao qtspnute pana.. nna< ces e ér 'sittaudps ces lfap ef='sp e/lic elic estination " mort"c eikipediaLa-euretf-et-la-machine.ut' rel='ext"" eimg src='es/L3/irtio-gd2/79/01e7e850f736866a3663f2ffad956f.png?1481148498' width='320viheight='180vi/ efap ef='sp estination ", mume"c estinl='ext"t : i">wikipediaLa-euretf-et-la-machine.ut' r Lasrtie nhBiocod estination "oinhor"c eikipedia_Wert d-Benjamin_out' r>BenjaminnWert dnna< ces e ér 'sittaudps ces lfap ef='sp e/lic e la ef='sp ef='sp estination "açon-right açon-oinhor"c eh2>L'qant duve2c estic estinl='ext" mort"cwikipedia_Gerprei-Jee da_out' r>eimg l='external'é oornal'é os'ix/dt"" src="es/L3/irtio-v claties/L90xH61/ointn659-1cd2c.jpg?1501003657" width='90viheight='61vi/ estinl continame"cJ"htt co Gerpreioc='sp stinl='ext"bior>ep>Maîtreée dans"hte ruece q7 illustidi id='nhbp> nir='bl ie de Gwi>Imort ouont bcogetaidl cl f='sp efap ef='sp ef='sp estination "açon-right açon-onchors"c ehumé des to-;ut difsa>wikipedia#;ut différ "cVaxe ti>c;ut différ ,(5) ef='sp estination "açon-right açon- mort"c &nbs%dan">nna eikl='ext"reemo eaiipediaQements.-te c-hst-lt -s gurt -sdiq-parolt -II.ut' rrU7;sittaud au hasardote_ref">&nbs%dan">nna yasssiblRittaud7;sion dus !lfap ef='sp e/='sp estination "açon-right açon-o enda"> eh2> eikl='ext"reemo eaiipediarnal.php?port=a enda">Aie esipésnu&nbs%dan">nna ela elic eikipedia+Sleree-mt(Vont b estination " mort"c eiel='ext"flue%dan-evrnt"cocod ec='sp estination ", mume"c estination "datr" 25lepteents 2017ec='sp estination "t : i">Slerbreeous17;idée ded='Lyo daertiCon-ri2 Vroy/ni (3/10)ec='sp ec='sp efap eflic elic eikipedia+Fit.' -ou-feouts-mt(Vont b estination " mort"c eiel='ext"flue%dan-evrnt"cocod ec='sp estination ", mume"c estination "datr" 23lepteents 2017ec='sp estination "t : i">Fit.' ouafeouts,brong>ont bcoge et dune preuve (29-30/9 et 16/10)ec='sp ec='sp efap eflic elic eikipedia+SFi7;nat-17;une pr-et-sint te-Pare -29-30-9+out' r> estination " mort"c eiel='ext"flue%dan-evrnt"cocod ec='sp estination ", mume"c estination "datr" 23lepteents 2017ec='sp estination "t : i">SFi7;nat,217;une proe.osint_cnh estination " mort"c eiel='ext"flue%dan-evrnt"cocod ec='sp estination ", mume"c estination "datr" 15lepteents 2017ec='sp estination "t : i">Mong>ont bcogeen enjtiqn;il etute trimodi (16-17/9)ec='sp ec='sp efap eflic elic eikipedia+Stephadi-Muoy/s-possi-au-Colle e-de-Fr exe+out' r> estination " mort"c eiel='ext"flue%dan-evrnt"cocod ec='sp estination ", mume"c estination "datr" 11lepteents 2017ec='sp estination "t : i">Snh estination " mort"c eiel='ext"flue%dan-evrnt"cocod ec='sp estination ", mume"c estination "datr" 8lepteents 2017ec='sp estination "t : i">Lap;trplers tquatiepduonprvort pdiffgonn eommuta?e/='sp ec='sp efap eflic e la ef='sp e/='sp ebrll='ext"cf cf-r exer"c stinl='ext"bçon-right açon-euivrsac eh2>Suivrs IDMefe2c estinl='ext"bçon-newsletfer"c estinl='ext" mort"c eiel='ext"flue%dan-plale"cocod ec='sp eune ispa"/dgisser_newsletfer" eeethod "utat"c elabele f="newsletfer_eng>l">Newsletfer IDMeflabelc einput type "text" name="newsletfer_eng>l"ispa"newsletfer_eng>l"iplaceholdef="Ad, mê e-mti r> ebuttann/ype "submit">nnaniel='ext"flue%dan-dantno ">nnannannannanna c elic eh3 En eg/mape ce/e f enavf e> c eliceikipediarnal.php?port=Rittaud7-17;difsa>Aittaud7;ré;difssatiuvlic eliceikipedia-La-tribunrassi-mt(Vont belis-out' r>Tribunrsatiuvlic eliceikipediarnal.php?port=a enda">A endasatiuvlic eliceikipedia-Defis-du-Cal l&#es -mt(Vont bDéfisnuDébit lu 18p>Biuvlic eliceikipedia-Rrvu<-de-re d -out' r>Rrvu<#8217;ud satiuvlic eliceikipediarnal.php?port=lexurs a>Lexurs satiuvlic la navf eflic elic eh3 D’anestrong>ont bcogete f enavf e> c eliceikipedia-Mt(Vont bMong>ont bcoge, uve.res ssatiuvlic eliceikipedia-En-eoe.E9p brt d̵qhématioucol satiuvlic eliceikipedia-Mt(Vont bMong>ont bcogeaade conssatiuvlic eliceikipedia-L-IHP-mtisan-d-hissleres-out' r>Le de GIHPt m Chofo ni de &hissleressatiuvlic eliceikipedia-L-IHP-unramtisan-de-sFi7;na-tiè- yas-out' r>Le de GIHPt u dem Chofo esFi7;na tièr yassatiuvlic eliceikipedia-Trimesssis-IHP-out' r>Trimesssis IHPsatiuvlic eliceikipedia-Mans -de-la-17;une pr-out' r>Mans plers tr7;une preutiuvlic eliceikipedia-Aittaud7-mt(Vont bÉthneplers tr7;une preutiuvlic eliceikipedia-Oes c-du-moiy-out' r>Oes c lu mpubsatiuvlic eliceikipedia-Cafrassi-mt(Vy-out' r>Caffou tstrongssatiuvlic eliceikipedia-Lrs-ref="http:s-du-trimesssi-out' r>Li>c;uf="http:set.Hisslereouont bcogettiuvlic eliceikipedia-Imort -et-vis esis de $-out' r>Imort o c vis esis de $ttiuvlic eliceikipedia-Rsis&#rct -pddagogbRsis&#rct pédagogbCour#es ou > il conticolums-3"> eliceikipedia+-Aunt f-de-Ge pub-+out' r>Aunt fd re e pubsatiuvlic eliceikipedia+-Bo sit-Mtns lbrot-et-l' -oes co-fano alb-+out' r>Bo sa veMtns lbrotent coes co fano albsatiuvlic eliceikipedia+-B anglaieB anglais ; l o c p7;unodbont bcogettiuvlic eliceikipedia+-Ca nets-de-re la-de-la-MMI-+out' r>Ca nets̵e laalers tMMIttiuvlic eliceikipedia+-Ca ti> tphie-+out' r>Ca ti> tphiettiuvlic eliceikipedia+-Fau-il-avler-peur-ssi-mt(Vy-+out' r>Fau-il avleri,acrouHenri P7incaséttiuvlic eliceikipedia+-JacJacJeanelesRans D’Alemb)'t ttiuvlic eliceikipedia+-Joseph-Louub-La> tnge-+out' r>Joseph-Louub La> tngettiuvlic eliceikipedia+-Lrs- diviss-...)' is-jumeaux-+out' r>LArref="http:/u&st diviss(...)' is jumeauxttiuvlic eliceikipedia+-Lr-mans -ess-mt(Vont bLi mans ;il nrong>ont bcogttiuvlic eliceikipedia+-Lrs-5-min la -Lrbesga -+out' r>Lis 5 min la Lrbesga ttiuvlic eliceikipedia+-Lrs-s gurt -sdiq-parolt -+out' r>Lis s gurt use entarolt ttiuvlic eliceikipedia+-Lrs-iiferviews-du-CIRM-+out' r>Lis iiferviewset.Mong>ont bcogealers t&laleuve Tde;: (2013)ttiuvlic eliceikipedia+-mt(Vont bMong>ont bcoge et a ts plastbMong>ont bcoge et Inde griettiuvlic eliceikipedia+-Mt(Vont bMong>ont bcoge et qungngesttiuvlic eliceikipedia+-Mt(Vont bMong>ont bcoge et qifarerasp;:ttiuvlic eliceikipedia+-Mikhail-Gromov-geomet;:-+out' r>Mikhaïl Gromov,m si,t>t;:ttiuvlic eliceikipedia+-Nicolas-Bt fbaki-+out' r>Nicolas Bt fbakittiuvlic eliceikipedia+-Parlez-vo7;-mt(Vy-+out' r>Parlez-vo7;trongs&ingue?satiuvlic eliceikipedia+-R7;di’uy-+out' r>R7;di’uysatiuvlic eliceikipedia+-T21nsuve.-optimal-+out' r>T21nsuve. optimal ttiuvlic la lic elic eh3 Qsiloouts-n?e/e f enavf e> c eliceikipediaPrt diffde $-de-Imort -ssi-Mt(Vont bPrésdiffde $satiuvlic eliceikipediaNot;:-eFoncs defdpe cet.Not;: aie esipésatiuvlic eliceikipediaSila -Ple id='nhs-de ls-amis.ut' rrPle id='nhssatiuvlic eliceikipediang>lto:dantno @ mort .rong.cnrsc'sr>Contno satiuvlic la navf eflic la ef='sp ef='sp efsecs dep Créela set m)&n uy légvee satiuvlic liceikipediaSila -Ple id='nhs-de ls-amis.ut' rrSila web utiee satiuvlic liceikipediang>lto:dantno @ mort .rong.cnrsc'sr>menu contno satiuvlic la navf f='sp stinl='ext"cal-right"n f='sp ef='sp efr exer> ent&nbs type "text/urtant&nbs" src="ssemeaties/js/ tran .rin.jcogry.js">nnnt&nbs> ent&nbs type "text/urtant&nbs" src="ssemeaties-ce gom/vendor/cookiesplease/cookiesplease.rin.js">nnnt&nbs> ent&nbs type "text/urtant&nbs" src="ssemeaties-ce gom/js/app.rin.js">nnnt&nbs> ent&nbs type "text/urtant&nbs"p var _paq = _paq || []; _paq.push(['trackPortView']); _paq.push(['id=bleLinkTracking']); _paq.push(['setTrackerUrl', '/piwik/piwik.php']); _paq.push(['setSilaId', 1]); (funcs de() { var d=docLmia.,m =d.cre="eEalmia.('nt&nbs'), s=d.getEalmia.sByTagName('nt&nbs')[0]; g.type 'text/urtant&nbs'; g.defer=true; g.async=true; g.src='/piwik/piwik.js'; s.taria.Node.intideBefore(g,s); })(); nnnt&nbs>